Archive for May, 2005


Tuesday, May 24th, 2005

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…


Wednesday, May 18th, 2005

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

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.


Tuesday, May 17th, 2005

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.

OTT by reflecting telescopes

Monday, May 16th, 2005

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


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

We inhabit telescopes with substitutions, given G |- D Tel