Epilogue

Just for reference, I have created an Epigram page under wikipedia, see Epigram programming language

You are welcome to improve on what I have written…

Further to recent remarks, I have now implemented a toy elaborator for Hutton’s Razor (the language of integers with addition). You can find it here. Seems to work. The elaborator itself is
tiny.

hutton :: [Value] → Blah
hutton _ =
  Conc (MNode PLUS ["x", "y"] $
    Bind ("x", Call hutton []) $ λx →
    Bind ("y", Call hutton []) $ λy →
    Solve (plus x y)) $
  Conc (MNum $ λi → Solve (VC i Nothing)) $
  Error "unrecognized input"


More chat about this later.

The Epigram project woke up again today after a period in which several papers were written on or around the subject of programming (in) Epigram.

It’s Conor’s task for the time being to create a programming language for describing how elaboration problems get solved (or suspended) he has applied Hutton’s razor and is developing Haskell combinators that do the stuff. The curious might find information relating to this in their cvs. This will hopefully lead to a very good idea about what the interface between the UI and the elaborator should be, once that is sorted a lot of doors will fly open around here.

Peter is going to look in to the ST monad library to see if he can’t help Conor make navigating the proof state with updates a lot more efficent.

Starting point: TT with some proper dependency, e.g.

b : Bool
————–
T b : *

T false = Null
T true = One

we assume at least Pi, Sigma, Empty, Null, One, Bool. We also use Prop <= *,
for propositional types.

We introduce telescopes G |- D Tel , e.g.

-----------
G |- () Tel

G |- D Tel G.D |- S : *
-----------------------------
G |- D.S Tel

where

G.() = G
G.(D.S) = (G.D).S

We inhabit telescopes with substitutions, given G |- D Tel
(more…)