Epilogue

Peter and I started writing the Scoper earlier. See Scoper.lhs. In particular, check out the definition of Concrete, which is about as simple as it’s likely to get. We’ve suspended any funny ideas about imperative data structures for concrete syntax, but we are using imperative refs for ‘acts of naming’, allowing change of the associated string.

Given some feverish after-dinner hacking with Wouter, we now have scoping for a good chunk of CTerm, including all of CPat, and it seems to be doing the right thing. Our mechanism for accumulating ‘shadows’ is in place, but we haven’t yet implemented anything which might discharge a shadow, so it’s hard to see the point just now.

Read the rest of this entry »

The Epigram meeting today resulted in quite a few action points:

• Thorsten should write something for the e-pig website. Conor should then rewrite it.
• Wouter should incorporate the feedback on the library
• Peter has had his types paper accepted! He will work on putting some well-documented examples on the website.
• Conor has some photographs that might be suitable for the e-pig website. He had some productive chats with Edwin about lightning and Term.lhs. Incidentally, his paper has also been accepted. He’s been hacking on the Parser and PrettyPrinter in Scotland.
• James is working to reach the TFP deadline and has been playing around with normalization by evaluation.
• Joel has handed in his thesis. He now has time to look at some examples. Thorsten suggests having a look at Tarmo’s compiler and implementing it in Epigram.
• Finally, we should maybe organise a Hack Fest to get some work started towards a command-line interface and Epigram 2 development in general.

Next week we should discuss a selection of examples, which Peter can then beautify for the website.

It’s not entirely sustainable to claim that Epigram’s underlying theory is exactly Luo’s UTT, what with funny η-rules popping out of the woodwork. Perhaps we need a new name. Being naturally hostile to acronyms, but enjoying suggestive combinations of sounds, I propose ‘Grut’.

I just put the sources for the tutorial under cvs (papers/tutorial) so we can modify it, and so that we can raid it easily for spare parts. It might be a good move to take this as the master copy for the website version of the thing.

Did some cooking with Edwin yesterday, and we came up with an ExTT-like way of separating phases. The idea is to annotate context entries and the typing judgment with a level number (low numbers are more dynamic), with

That is, higher level stuff can only be used for higher level things. We require of our design that the following be admissible

So, contextuals and star (this stratification is orthogonal to stratification for consistency):

Next, the slight generalisation of ExTT to have a funny λ
Read the rest of this entry »

Following Wouter’s fp lunch chat about patches and bit of a kickaround with Lucas Dixon, I’ve started wondering whether there’s a sensible notion of patch which should accompany the editing of a module–if I edit module A, eg by renaming something, can we generate a patch not for A, but for every module importing it, propagating the change? If we timestamped every module import on compilation, we could figure out which patches to apply on recompilation. Is revision control (darcs?) another ingredient of a good Epigram system? Somehow, it’s already a part of what we do ‘in the small’.

I’ve written a small step-by-step tutorial on how to play with MPgram. You can go to this tutorial either from MPgram page or just directly: http://www.jetbrains.net/confluence/display/MPS/MPgram+tutorial

At the moment, I’m developing an editor for Epigram using a tool called MPS. Since MPS has had EAP recently – hence it’s available for download already, I’ve made a page to make my editor available for everyone to play with.
http://www.jetbrains.net/confluence/display/MPS/Epigram

First up, have a butcher’s at TypedLambda.epi. If you look hard enough, you’ll see that all sorts of implicit syntax is holding this thing together. Not only implicit argument synthesis, but implicit argument abstraction—the sort of thing which shows up with rank-n polymorphism. Getting this to behave at all sensibly was quite a big deal at the time and it’s still a bit garbled, to be honest. So let me try to make a clearer plan for version 2.

Epigram has implicit quantifiers, ∀_ and ∃_, which are distinct from their explicit counterparts. (In Lego, the implicit and explicit ∀ were identified, and this inevitably resulted in lots of little mishaps.) Epigram provides both implicit and explicit means to use and to construct elements of implicitly quantified types.

In the underlying type theory, everything is explicit. Use: the postfix _ inhibits implicit usage and instead converts its operand to an explicit function or pair.
Read the rest of this entry »

I can imagine uses for this where clause in programs other than just explicitly shadowing pattern variables which would otherwise be captured. Not only might we consider definitions in there, like Haskell, we might also consider other bits and pieces. Recall the thorny issue of

[Unparseable or potentially dangerous latex formula. Error 3 : 547x32]

This is a reasonable definition, but it doesn’t make a very good view. What happens? You get a nice case when they’re equal, but when they’re not, the context acquires a proof of difference but you don’t. We could now have

Clearly, such an appeal to the context must be unambiguous, and here it is, because even if we had two proofs of the inequality, they’d be definitionally equal. This brings me back to wondering about a proof language for Epigram, where we invoke a proof (with an irrelevant value) by the proposition it proves, rather than by name. Propositional hypotheses could then be anonymous, and where clauses might be the way to make them explicit.

I think there’s an opportunity to do something very nice here, but I can’t tell what it is yet. I think we should think it out a bit more.

A bit more. Where clauses would give us an opportunity to define previously unheard of symbols showing up in right hand sides. Interactively, one might invoke an undefined function: the system could respond by opening a where clause with a template for its definition. Moreover, if the invocation constitutes a Miller pattern, the type of the local function can be plausibly inferred. As a piece of programming language syntax, this makes some sort of sense, but the question is what to call the local function globally, when it shows up in the normal form of a computation on open terms. I have some ideas about that, but their distinctly underdone.

Arising from today’s headbanging session, we have another round of proposed concrete syntax evolution. Here’s the loose context-free approximation.

(Grammar grammar: angle brackets are the meta-brackets here; ? means ‘0 or 1’; * means ‘0 or more’; + means ‘1 or more’; ,* means ‘0 or more, comma-separated’ and similarly for + and for other separators.)

Expressions

Read the rest of this entry »

I’ve bundled together the first group of epigram programs that may become part of some kind of standard library at some point. I’ve hacked together a little something to generate the dependency graph and a nice clickable interface. You may want to check it out. For now, it lives in a subdirectory of my homepage, but it should move to sneezy at some point.

Comments are very welcome. Note that I’ve gone through the .epi files in epigram/durham/examples, but I haven’t finished looking into ctm, txa, or Thorsten’s course work yet. Besides the library files, I’ve gathered the following examples so far:

• DecEqNat.epi – decidability of equality on Nat
• DecEqType.epi – decidability of equality on simple types
• Lam.epi – untyped lambda calculus, substitutions on terms
• PlusComm.epi – proof that plus commutes
• TakeWhile.epi – the name says it all
• Bounded.epi – the bounded view
• Eval.epi – evaluation of simply typed lambda terms

You can find example X on www.cs.nott.ac.uk/~wss/EpiLib/Examples/X.epi.

The line between examples and library functions can be rather fuzzy. If you disagree with my choices, let me know. I’ve tried to limit the modules in the library to those that have a fairly high chance of being reused.

Any feedback would be very welcome. If things aren’t going the way you would like them too, let me know sooner rather than later.

Scope resolution can be a bit tricky. It creates issues which we need to resolve as straightforwardly as possible. The basic thing we need to determine is when an identifier is a binding occurrence for a local variable, and when it’s a reference to a global variable. We’re used to the situation where this is obvious from the syntax, because patterns are distinct from terms, or whatever. That’s no longer the case.

Where might variables be bound?
Read the rest of this entry »

We planned the homepage which Peter will put together. It should consist of:

• Tarball source downloads and binaries for Linux, Mac OS X, Solaris, and Windows
• Documentation consisting of at least the manual, AFP tutorial, and a selection of papers (including Why Dependent Types Matter, View from the left, A Few Constructions on Constructors, Exploring the Regular Tree Types, and Edwin Brady’s thesis)
• A selection of examples and useful libraries
• Suggested background reading
• Links to the dependent type community, Epilogue, Haskell, ghc, and XEmacs
• Finally, it should just be pretty.

Furthermore, Wouter volunteered to look after the libraries and James will update the manual. Thorsten emphasized the need for an IDE and suggested looking into Eclipse. Finally, Conor gave a nice overview of how the Epigram system is layered before we went for coffee: