• Thorsten should type:
    1. darcs get http://sneezy.cs.nott.ac.uk/darcs/term
    2. cd term
    3. chmod +x Setup.hs
    4. ./Setup.hs configure --prefix=$HOME
    5. ./Setup.hs build
    6. ./Setup.hs install --user
    7. (and providing $HOME/bin is in your path:) epigram
  • The next job in term is to build equality in these steps:
    1. Propositional equality
      coersions between equal types (and the proof that these are coherant)
      $\AR{\Rule{\va\hab\vA\quad\vq\hab\vA=\vB}{\va\ [\vq\rangle\hab\vB}\smallskip\\
\Rule{\va\hab\vA\quad\vq\hab\vA=\vB}{\va\ [\![\vq\rangle\hab\va\ [\vq\rangle=\va}}$
      and the structural rule for application
      $\Rule{\vp\hab\vf=\vg\quad\vq\hab\vs=\vt}{\vp\,^=\vq\hab(\vf\ \vs)=(\vg\ \vt)}$
    2. Proof-irrelevance for equality, to do this right we need to decide equality during evaluation (if we do not have a proof of an equation but it’s homogeneous, then we win anyway). The upshot is Equality.lhs and eval from Term.lhs need to be in the same file.
    3. Observational equavalence, at some point (sooner rather than later) we’ll include the structural rule for $\lambda$:
\left(\Rule{\VV{x_0}\hab\VV{S_0}\quad\VV{x_1}\hab\VV{S_1}\quad\vx\hab\VV{x_0}=\VV{x_1}} {\VV{t\;x_0\;x_1\;x}\hab\VV{t_0\ x_0}=\VV{t_1\ x_1}}\right)}}{\lambda^=\vS\ \vt\hab(\lambda\VV{x_0}\hab\VV{S_0}\Rightarrow\VV{t_0\;x_0})=(\lambda\VV{x_1}\hab\VV{S_1}\Rightarrow\VV{t_1\;x_1})}$
      Thorsten pointed out that is rule can be derived from substution of equals for equals plus the more primitive:
      Having this gives OTT a simpler core, but Conor prefers the first version because it is easier to program with.

Leave a Reply