Epilogue

OK, I think I have a plan. I’m gonna

• hack in Bool and W directly, leaving ‘data’ alone for the moment
• add the relevant extra eliminators for equations (dom, cod, sym)
• make coe go into functions, pairs and trees
• add a constructor for extensionality

If that works out, it’s time to rethink data, then remove Bool and W. I’ll keep youse posted.

I’m following a plan to get us to stage 2 of the equality story: proof irrelevance. I’ll update this post as I go, but so far I’ve

• split Term into syntactic stuff (still Term) and semantic stuff (new file Value)
• lumped the contents of Equality into Value and removed Equality
• threaded a freshroot through eval and everything which calls it (no fun at all)
• added source and target to coe and coh
• made the computational behaviour of coe and coh compare source with target if the proof isn’t already refl
• made normal proofs of equations equal
• made spine comparison of coe just compare sources and targets, rather than (irrelevant) proofs
• did some very basic testing
• pushed the changes
• gone in search of a drink

I’m trying to keep Epitome sane as I go.

Meeting:

• 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)
     
     and the structural rule for application
     
  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 :
     
     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.

I just had the following interaction with the version I just pushed:

*ParseEvalCheckRender> parseit synthit
input:
Nat => => data X : * where <z> : X ; <s> : all x : X => X
two => => <s <s <z>>> : Nat
plus => => lam m => lam n => m elim{Nat} (lam x => Nat)
% n
% (lam x => lam xh => <s xh>) :
% all m : Nat => all n : Nat => Nat
---
plus two two
STOP

<s <s <s <s <z>>>>>
data X : * where <z> : X ; <s> : all x : X => X


Some sort of progress, I think.

1. UI. Some interest from Nick Thomas. Joel is planning an experiment with gtk2hs.
2. Using darcs is working very well. Discussed structure our darcs repos.
3. Status of Epigram 2. We have been hacking the core recently. The afore mentioned ‘Up’ and ‘Down’ terms are in with the supporting parser, (not very) pretty printer,type checker equality checker. Peter has been implementing datatypes. Next is the equality type, and then on to wrapping it in a representation of holes.
4. Thorsten discussed injectivity of type constructors.
5. Move to the board to discuss 3 further. Specifically Conor proposes a short path to making something go. Two main areas: a) Finishing Core and moving on to theorem prover. b) Concrete syntax, comms protocol.

6. Division of work. Joel and Wouter to look at concrete syntax and comms. James and Peter to look at core and theorem proving.
7. The advantages of supporting observational type theory sooner rather than later will afford us simplifications in the implementation. (Thorsten to go into more detail about this on the blog).

I’ve just completed the upgrade of the blog software to Wordpress 2.0, fun. The shouldn’t be too much new stuff to get used to, the admin pages look different but are fairly similar in content.

You may notice that I’ve swapped darcs activity in for cvs, this time round it doesn’t use the hack of commenting on a dummy post and uses rss instead, try clicking on on of the patches to find out why.

If you find any bugs, leave a comment and I’ll fix.