Epigram meeting

March 7th, 2006 by James C

The Epigram meeting went underground today due to the AUT strike. Despite a surprise picketter having taken up temporary residence on Conor’s downstairs sofa we weathered the shouts of “Scab!” and made it safely to Conor’s study.

Topics of discussion:

  1. Further consideration of the advice provided to us by team gtk2hs on Friday.
  2. Edwin is here and keen to build on his experiment of circumventing ghc’s typechecker to utilise the STG Machine for compiling Epigram programs. Expect further news on this later in the week.

This Week

February 21st, 2006 by Conor

Three things on the slate this week

  • Datatypes for OTT: the current implementation loses canonicity if you use the notion of datatype from the pre-OTT days, so we need to bring this up to date. Peter Morris and I have a plan bearing a certain resemblance to what’s going on in the Indexed Containers paper; we also have a longer term plan, with an even stronger resemblance to the same, but that’s another story.
  • Hierarchical proof state for Ecce: my Oleg theory of holes has the annoying problem that objects only have private subobjects (within so-called ‘guesses’); subobjects which need to be visible get λ-lifted and exported to the global context, resulting in a flattening of the elaboration tree, a loss of sharing, you name it. Just do a proof-state dump in Epigram 1 (META-RET, then look in *Epigram-bin*) if you don’t know what I’m talking about. So the plan is to do away with guesses in favour of hierarchically stored but fully λ-lifted holes and definitions. With a twist: we use a relative mode of naming, omitting the parameters held in common between reference and referent. So although these things are globally global, locally they look local. Oh, wait and see…
  • Dummy elaborator for high-level source code. Joel has refactored the grammar and the parser; Peter has refactored the scoper; we just need to reassemble the pieces we had before and we have a basis to build a real UI. We might have the beginnings of a non-dummy elaborator soon enough too.

WTFM…

February 15th, 2006 by Conor

…is the new injunction which we shall doubtless take as seriously as we take anything. With that in mind, I have begun to exploit the page facility of this blog to produce some user documentation for Ecce, so that the intrepid might have fun and games of one sort or another. I, er, encourage my fellow developers to keep this stuff accurate, warts and all.

GHC back end?

February 8th, 2006 by Edwin Brady

I’ve been thinking for a while that it ought to be possible to get Epigram to write out haskell code for ghc to compile, suitably annotated with unsafeCoerce# so as to get past the type checker. I finally got around to experimenting with this the other day; you can see some of the results here (generated from this).

This code is (mostly, apart from the Haskell interface glue at the top) generated by a tool I’m working on for a completely different reason from my usual noddy test functions: factorial, variadic adder and vector sum. I’ve tested it on some more complex code, but this example (factorial in particular) gives some idea of how fast it goes (about 1 second to compute 9! on my machine). Perhaps if I get a moment later this week I’ll try to make a more interesting program.

Read the rest of this entry »

Next stop, a wee theorem prover…

February 6th, 2006 by Conor

Needed to do a bit of hacking at the weekend, so I just sorted out the naming mechanism to allow and generate the x^n notation. Try typechecking lam X : * => lam X : X => X and lam X : * => lam X : X => X^1.

Next mission, a very simple interactive editor for proof states, given by (Cursor (Key UId Reference)) for now, but we’ll go tree-structured later. In the first instance, this should just have holes and lets, with refinement and undo as the basic operations. This requires the ability to propagate an update. Before long, though, we’ll want to have parametrised things, and a hierarchical structure. We should be able to knock up a serviceable toy in fairly short order.

Towards Observational Equality

January 26th, 2006 by Conor

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.

Towards Proof-Irrelevant Equality

January 25th, 2006 by Conor

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.

Minutes

January 17th, 2006 by pwm

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
      $\Rule{\va\hab\vA\quad\vb\hab\vB}{\va=\vb\hab\Type}\;\;\Axiom{\DC{refl}\hab\va=\va}$
      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$:
      $\Rule{\AR{\VV{t_0}\hab\forall\VV{x_0}\hab\VV{S_0}\Rightarrow\VV{T_0}\\
\VV{t_1}\hab\forall\VV{x_1}\hab\VV{S_1}\Rightarrow\VV{T_1}\\
\vS\hab\VV{S_0}=\VV{S_1}\\
\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:
      $\Rule{\VV{t_0},\VV{t_1}\hab\forall\VV{x}\hab\VV{S}\Rightarrow\VV{T}\quad\vf\hab\forall\vx\hab\vS\Rightarrow\VV{t_0\;x_0}=\VV{t_0\;x_0}}{\lambda^=\vf\hab(\lambda\VV{x}\hab\VV{S}\Rightarrow\VV{t_0\;x})=(\lambda\VV{x}\hab\VV{S}\Rightarrow\VV{t_1\;x})}$
      Having this gives OTT a simpler core, but Conor prefers the first version because it is easier to program with.

2+2=4

January 15th, 2006 by Conor

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.

First meeting of the year

January 10th, 2006 by James C

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.
DSC00017.JPG
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).

2.0

January 7th, 2006 by pwm

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.

Backstage

December 11th, 2005 by pwm

Although it might seem all quiet on the Epigram front, in actual fact there is somewhat of a blitz going on at HQ and I thought I’d let you in on some of what has been going on.

As you can see in the last post Conor changed his mind slightly on what Terms where going to be, in those pictures, Up terms are those you can sythesize a type for (and are now called Synth), Down terms are terms you have to push the type into and check (and are now called Check).

Since changing to this representation would break a lot of what is already there we took our experiment ‘offline’ and Conor, James, Wouter and I set to work on implementing all the kit we needed for the new underlying terms (and values). When I say offline, I really mean we created ourselves a Darcs project as it seemed the perfect experiment of our plan to move wholesale to darcs. The results of the tinkering and the experiment can be grabbed by entering ‘darcs get http://sneezy.cs.nott.ac.uk/darcs/term’. It’s not finished, but a few days work bore many fruits.

Next up, holes and Datatypes.

Local types for local people

December 2nd, 2005 by Conor

More to say about this anon, but here are some boards, before I clean them to write some more.






Moping, hoping, scoping, coping

November 29th, 2005 by Conor

Just a thought, which I decided to scribble down before I forgot it.

Key policy: Epigram is a declare-before-use language, temporally as well as spatially. When you say x, you get the most local existing x at that time, or you get a new x generated as locally as possible. In a declaration, spare names go into the generalisation prefix; in a rhs, spare names go into the where clause, one way or another. Naming is a surrogate for pointing, so once the bond of reference is created, it must not be broken by ill-propagated renamings, capturings, or whatever. It’s this policy which enables scope resolution at any point in time: there should never be any issue about the referent of an identifier.

Now, we go backwards as well as forwards, this time around, so what happens when you delete information. Well, there are at least two sorts of undo: devaluation (removing (parts of) the value of a symbol) and degeneration (removing the symbol altogether). Now, you propagate a devaluation by rechecking and devaluing everything which depends on a devalued symbol. Degeneration is much scarier. But I remember now, there’s a funny thing. If you set things up right, you don’t need degeneration, exactly…

Imagine we have only let (the sooner we turn data into sugar for let, the better). You can devalue a let, replacing the top rhs by a shed. Now, key editing move: you can commute one let past another by turning

let f blah ; let g waffle

into

let g waffle ; let f blah

if waffle does not depend on f, or

let g waffle where f blah ; let f blah

otherwise. Degeneration is thus the repetition of this refactoring until the global f falls off the end!

(For data as it is now, you need to generate a bunch of lets for the type, its constructors and its various gadgets.)

In terms of what happens to typedness, we should try to ensure that devaluation cannot increase the amount of brown. Intuitively, removing information cannot increase the amount of stuff which is definitely wrong. Of course, we should expect yellow all over the shop.

I mention this largely because this is pretty fundamental stuff, in terms of the propagation of updates around the system. It’s rooted in the proof engine, below the elaboration layer, so the time to figure it out is now.

Minutes

November 15th, 2005 by James C

Points from today’s meeting:

  • darcs is being tested but we’ll hold off using it for epigram for a week or so.
  • Still waiting for
  • Epigram now has a independent type checker for terms and the parser is connected so that it can be tested out. Consumers of this service to follow. Thorsten questioned whether it was sensible to test it via the parser or whether we should generate terms using quickcheck to test it.
  • Wouter has written some haskell to handle expanding includes in Epigram 1. This hasn’t been been hooked up yet
    as it requires some elisping.
  • Whilst on the subject of elisp we considered whether it might be feasible to move to GNU Emacs for Epigram 1 as the carbon version for OS X is quite nice.

R’n'B

November 10th, 2005 by Conor


Turning into code at a whiteboard near you…well, near me, anyway…

Minutes 08-11

November 8th, 2005 by Wouter

There were a few concrete points that did come out of today’s meeting.

Wouter should write a few bits of Haskell to fix Thorsten’s problems using include.

We also need several mailing lists:

  • Epigram general e-mail address - epigram-help at epig etc
  • Epigram developers - epigram-dev at cs dot nott etc
  • Epigram nottingham crew - epigram-notts at cs dot nott etc
  • General epigram discussion - epigram at durham etc

All with suitable links on e-pig if it’s relevant.

Conor also showed that lambda abstracting neutral terms requires more work than you might think at first.

An editor is born…

October 25th, 2005 by Wouter

After hooking Conor’s dummy elaborator to the bits of my crummy editor, the result is the very first preview of Epigram 2 in action.

The editor doesn’t do much and the elaborator says everything type checks, but it’s a start.

Try:

> cvs update -d
> cd current/src/
> make
> echo 'lam X : * => X' > Lam.epi
> ./epigram Lam.epi

You should see a poorly pretty printed version of the original, with highlighted identifiers on a grey background. Try giving the following commands to the editor:

> down
> right
> left
> up

You should see the focus change as you navigate the abstract syntax tree.

To quit the editor, just type quit.

There’s not much else you can do at the moment. Next on the todo list are better pretty printing and actually being able to request elaboration after filling in a shed.

brainshitting reviewed

October 25th, 2005 by txa

Last week we went through the brainshitting list we produced in Durham early this year to see where we are and where we should go. A bit delayed here is the commented list:

Read the rest of this entry »

Container Syntax

October 24th, 2005 by Conor

container syntaxcontainer semantics

Hank dropped by. I scribbled this.