Archive for June, 2005

Lightning

Thursday, June 30th, 2005

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


\Rule{\vx :^i \vS;\Gamma \vdash }{\vx :^i \vS;\Gamma \vdash \vx :^j\vS} i\le j\quad
\Rule{\vx \mapsto\vs:^i \vS;\Gamma \vdash }
         {\vx  \mapsto\vs:^i \vS;\Gamma \vdash \vx :^j\vS} i\le j

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


\Rule{\vdash \vt :^j \vT}{\vdash \vT:^{j+1}\Type}

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


\Axiom{\vdash}\quad
\Rule{\vdash \vS:^{i+1}\Type}{\vx:^i\vS\vdash}\quad
\Rule{\vdash \vs:^i\vS}{\vx\mapsto\vs:^i\vS\vdash}\quad
\Rule{\vdash}{\vdash\Type:^i\Type}

Next, the slight generalisation of ExTT to have a funny λ
(more…)

Modules and Patching

Tuesday, June 28th, 2005

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’.

Scoping

Monday, June 27th, 2005

Scoping traverses concrete syntax, threading some effects:

  • reading the scope, being (concretely) an alist of strings to namerefs; what is its abstract interface?
  • generating new namerefs, due either to an explicit binding (in a pattern or a shadow), or to an implicit binding (a previously unseen name in an lhs or a sig)
  • accumulating the set of new namerefs, when we see a name which is not in an explicit binding position, we should look it up if we can and generate a new nameref if not; we must accumulate the set of these names so we can add them to the relevant shadow; this way, the elaborator will know exactly where everything is to be bound
  • building imperative syntax trees: we may as well get our node identifiers from the ref supplier; also, we can equip trees with backpointers, and possibly other editor-related gubbins

Scoping will also need to generate binary applications, handling any weird operators we might allow. I’ll have a stab at the datatype of nodes in a bit.

MPgram tutorial

Saturday, June 25th, 2005

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

MPgram: MPS-based Epigram editor

Wednesday, June 22nd, 2005

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

Implicit Syntax and Manual Override

Sunday, June 19th, 2005

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.
(more…)

1st Annual Epigram Photography Competition

Saturday, June 18th, 2005

I’m currently in the process of sprucing up the Epigram website and at the same time sharpening up the look of the blog so that there’s a common look and feel, but at the same time making it look less like an out of the box weblog (which is what this style is modulo some grass).

So to the competition, I’ve been struggling to come up with 2 banner pictures which are appropriate for the two sites, ideally they should:

  • be approximately the size of the current Epilogue banner
  • be related in some way to each other…
  • …but also recognisably different from each other so the two sites are distinct
  • not be too fussy, so that the titles and subtitles of the pages are easily read
  • not be copyrighted (unless it’s your copyright and you are happy for us to abuse it)

They could also be related to the project or just pretty, it’s up to you.

Any entries on the back of a postcard to the usual address (or you can email pwm AT cs DOT nott DOT ac DOT uk).

Prizes include a pint when i next see you

Where Clauses

Wednesday, June 15th, 2005

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 : 546x32]

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


\AR{
\FN{f}\:\vx\:\vy\:\BY\:\RW{view}\:(\FN{eqDec}\:\vx\:\vy) \\
\quad\FN{f}\:\vx\:\vx\:\cq\:\cdots \\
\quad\FN{f}\:\vx\:\vy\:\cq\:\cdots \\
\quad\quad\RW{where}\;\vp\hab\vx\TC{=}\vy\To\TC{Zero}\\
}

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.

Concrete Syntax Again

Tuesday, June 14th, 2005

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

\[
\begin{array}[t]{rl}
\textsc{Small} := & (\left< \textsc{Field}\right>^{;\ast}) \\
| & \textsc{Var} \\
| & \texttt{\_} \\
| & [\textsc{Text}] \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Field} := & \left< \_\right>^{?}\:\left< \textsc{Pat}\texttt{=>}\right>^{?}
\: \textsc{Term} \left< \texttt{:}\textsc{Term}\right>^{?} \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Term} := & \textsc{Small}^+ \\
| & \textsc{Bop}\: \textsc{Sig}\: \textsc{Rhs} \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Var} := &  \textsc{Id}\left< {{}^{\wedge}\textsc{Nat}}\right>^? \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Bop} := & \texttt{lam} \\
| & \texttt{all} \\
| & \texttt{ex} \\
\end{array}
\]
(more…)

Lib service

Sunday, June 12th, 2005

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.

Bindings and References

Sunday, June 12th, 2005

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?
(more…)

\TeXtiles

Thursday, June 9th, 2005

Thanks to Wouter for finding it (as some of you will have already seen) we now have a \LaTeX plugin to pull off crazy stunts such as:

$\bfig \Vtrianglepair/>`<-`>`..>`>/[A`A+B`B`C ;\mathrm{inl}`\mathrm{inr}`f`{[f,g]}`g] \efig$

Hmm, I wonder if I can get Conor’s Epigram macros into it…

UPDATE:


$\footnotesize
\AR{
\RW{data}\;\;
\Axiom{\TC{Nat}\hab \Type}\;\;
\RW{where}\;\;
\Axiom{\DC{zero}\hab\TC{Nat}}\;\;
\Rule{\vn\hab\TC{Nat}}{\DC{suc}\;\vn\hab\TC{Nat}}\\
\RW{let}\;\;
\Rule{\vm, \vn\hab\TC{Nat}}{\vm\FN{+}\vn\hab\TC{Nat}}\\
\begin{array}{llll}
\vm & \FN{+} & \vn & \BY\RW{rec}\;\vm\\
\;\;\DC{zero}& \FN{+} & \vn & \cq \vn \\
\;\;(\DC{suc}\ \vm) & \FN{+} & \vn & \cq\DC{suc}\;(\vm\FN{+}\vn)\\
\end{array}}$

Yes, it seems I can.

It guess the next thing people would want is lhs2tex. I’m on it

UPDATE 2:

%format ^+^ = &#8220;\ensuremath{\oplus}&#8221;

> data Nat        = Zero
>                 | Succ Nat
>
> (^+^)            :: Nat -> Nat -> Nat
> Zero      ^+^ n  = n
> (Succ m)  ^+^ n  = Succ (m ^+^ n)

BINGO

Epigram meeting, June 7

Tuesday, June 7th, 2005

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:

Phases of source analysis

Tuesday, June 7th, 2005

Figuring out the phases of source analysis to be done outside the elaborator will help figure out the details in the concrete syntax, so here goes.

  • the ‘lexer’ takes String to lists of tokens (actually with location info, thanks Peter);
  • the ‘grouper’ takes token lists to Doc, the type of documents with their brackets resolved;
  • the ‘parser’ takes Doc and produces unmarked concrete syntax with a Doc at each shed and (String, Int) for each identifier x^i (where x is short for x^0); we might imagine a more sophisticated editor which produces this format directly; remark—applications
    in this format are flat sequences of ‘small’ terms;
  • the ‘scoper’ takes this unvarninshed concrete syntax and
    • resolves the identifiers as variables, given the bindings in scope—the elaborator will provide the context of variables, but the front end must maintain the map to identifiers; hole—figure out how to represent locally bound variables and unbound variables; forbid shadowing in left-hand sides (but allow it in binders?);
    • resolves the structure of applications into binary form, dealing with operator precedence or whatever
    • labels the nodes with editor marks;
    • erases the sheds; concrete syntax should be polymorphic in the shed type, and so should the scoper, meaning that it can’t reveal the contents of sheds;

(more…)

Representing Concrete Syntax

Monday, June 6th, 2005

We need a generic protocol for communicating and elaborating concrete syntax. This creates a problem. How specific should we be wrt the syntactic categories of Epigram? My inclination is not at all. We either need a generic technology which will adapt to arbitrary syntactic categories, or we need to flatten the syntactic categories. At the moment, I don’t feel like figuring out how to do the former. So I suggest we adopt some very general setup like this

type Concrete shed = (Mark, CTree shed)
data CTree shed
  = CShed shed
  | CNode Node [Concrete shed]

Remarks

  • It’s polymorphic in the contents of sheds, but the elaborator is only ever sent Concrete ()
  • The type Mark is some equality type which belongs to the UI: it is used to mark information coming back from the elaborator as concrete syntax is processed.
  • The type Node represents both the terminal and nonterminal symbols, whatever they may be. Blah code will need to interrogate this type in arbitrary ways, so things might get a touch existential. As in
    data Blah
      = ...
      | ∀α. Case (Node → Maybe α, [String]) (α → Blah) Blah

    The function tests if the node suits the success continuation. If so, the strings name the subnodes and the success continuation executes; if not, the failure case runs. Of course, the whole thing suspends if we have a shed rather than a node.

Parsing to this representation requires that we can generate suitable elements of Mark (I suspect this may involve refs.) The real exciting stuff in the parser is more likely to involve figuring names out—more on that anon.

Printing. Hmm.

www.e-pig.org

Thursday, June 2nd, 2005

The above domain is now at our disposal, currently it points to http://sneezy.cs.nott.ac.uk/epigram but that is only because I had nothing better to aim at. Everything under that folder also has a dual in the e-pig domain so for instance this blog is also available at www.e-pig.org/epilogue.

Now I need to sort the page out so it’s worth people looking at it… To that end I would ask if people had any of the following to let me know:

  1. Libraries compatable with the new include mechanism
  2. Ideas on what should be in the downloadable versions of Epigram1
  3. Ideas what should be on the front page of e-pig.org