A big thanks to James Chapman for organising EE-PigWeek at the Institute of Cybernetics, Tallinn, Estonia. This time around, the crew comprised Brady, Chapman, Dagand, Gundry, McBride, Morris, and Norell. We started the week with an experimental system which did almost nothing. We finished the week with an experimental system which almost does something.
I’ll go into more details later, but this post is a quick summary of the equipment we’re on track with. All of this stuff would benefit from more careful pedagogy, one topic at a time. I’m thinking of the following list as a bunch of placeholders to be fleshed out in future, preferably once the technologies have paid off enough to sustain some useful examples.
Note, notation here is informal. Our syntax is still a matter of negotiation.
- Elimination with a Motive: the McKinna/McBride machinery for attacking problems with general programming schemes; you give us anything whose type looks like
(P : … → ∗) → … → P t1…tn and we’ll clobber your goal with it. This machinery is a handful of gremlins away from go-condition. When it surfaces, we’ll have something that’s recognizably turning into Epigram. - Labelled Types for Programming Problems Suppose I give you a ‘relation’
Plus : Nat → Nat → ∗ and ask you to ‘prove’ (x : Nat)(y : Nat) → Plus x y by induction. The subgoals —
(y : Nat) → Plus zero y
(x : Nat) → ((y : Nat) → Plus x y) → (y : Nat) → Plus (suc x) y
— specify the patterns for a recursive program, and the inductive hypothesis indicates which recursive calls are permitted by the recursion scheme. If there turns out to be a family of isomorphisms,
return : Nat → Plus x y, call x y : Plus x y → Nat
we can use this idea to organise programming tasks as ‘explanations of computability’. Dependent types give us pattern-vision when we program with recursion operators. Moral: even if your programs are simply typed, make ‘em dependent so you can see what you’re doing. Types indicate purpose, not just representation. - Three Variations on μF We started the week with a systematic presentation of describing strictly positive functors by data. We have a datatype Desc : ∗ with an interpretation function [D : Desc] : ∗ → ∗ explaining which functor a Desc describes. Mu (D : Desc) : ∗ delivers the least fixpoint μ[D], with a single constructor
@ (ts : [D](Mu D)) : Mu D
To get anywhere, we had to arrange for the functoriality of [D] to be obvious: we have a general map-operator, mapD, and it obeys the functor laws definitionally. We introduced a simplification procedure which rearranges terms which don’t compute:
map id xs = xs, and map f (map g xs) = map (f . g) xs
Ordinary evaluation lifts these laws inductively to all terms. - Variation Red: ν[D] We added Nu (D : Desc) : ∗, overloading @ as the coconstructor
@ (ts : [D](Nu D)) : Nu D
and adding the coiterator,
coit (D : Desc)(S : ∗)(φ : S → [D]S)(s : S) : Nu D.
A nondependent projection, currently and nastily a postfix %, either unpacks the coconstructor or unfolds the coiterator — you can’t observe which. We used a little programming with Desc to implement a generic version of take, so we could test the machinery. We also wired it up to Edwin’s epic compiler (call-by-value with explicit laziness override): Edwin gave it a thump and everything became smooth. - Variation Green: [D]*X We equipped each functor [D] with its free monad, adding
Term (D : Desc)(X : ∗) : ∗ = ‘ (x : X) | @ (ts:[D](Term D X))
As well as a general-purpose dependent eliminator, these terms come with a hardwired substitution operator, satisfying the monad laws definitionally, by the same method of rearranging stuck substitutions. - Variation Blue: indexed descriptions We began the process of generalising Desc to IDesc (I : ∗) : ∗, whose interpretation makes sets from I-indexed families.
[D : IDesc I] : (I → ∗) → ∗
Correspondingly, a function F : I → IDesc I can be interpreted by
λ P i → [F i]P
as an endofunctor on the category of indexed sets (I → ∗). In this way, we actually get to have the indexed data structures you know and love. Welcome back to vectors. We can also exploit F’s ability to inspect the given index to optimize the description of data in special cases. For example, we can give the type of vectors one constructor, with its description chosen on the basis of whether the length index is zero or more: this amounts to performing Edwin’s datatype optimizations by source-to-source transformation of descriptions. - Magenta, Yellow, Cyan, White? These three variations can, in principle, be combined to make all the colours of the sinclair spectrum. Indeed, we started work on the magenta variation (indexed codata), because we need it to describe bisimulations — the appropriate notion of observational equality for codata. The yellow variation, completely iterative monads, describe infinite terms (or strategies for potentially nonterminating state-insensitive interaction). The cyan variation, free indexed monads describe typed syntaxes (or DSLs for state-sensitive interaction, about which Edwin give a very interesting talk) (or just what happens when you use a Hoare Logic as a type system). The white variation, completely iterative indexed monads, may not quite be the moon on a stick, but it does let you describe how to stay alive in a dangerous world.
- Quotients Give us a set (the ‘carrier’) and an equivalence relation on it, and we’ll give you a set of equivalence classes. The constructor takes any element of the carrier to its equivalence class. The eliminator says ‘You can do whatever you want with equivalence classes, and even inspect the representative element, provided you prove that whatever you do respects the equivalence.’. Equality on our quotients is substitutive in a way that setoids just can’t manage.
- Elaboration and Distillation We’ve separated the syntax of terms for communication with the user from the terms which carry the full information required for typechecking and evaluation. Elaboration is the type-directed process of filling in the (often computationally significant) details of terms, given their types. Distillation is the reverse, separating the spirit of a term from its heavy fractions, eliding information recoverable from types. Please note the active role types play in determining the meaning of the things you write. Types are not an additional ‘police action’ serving only to deny execution: they’re a succinct way to replace low-level detail by high-level structure.
There’s a lot of positive stuff happening at all levels of the system. As a consequence, things have become a little ragged, but it’s in one piece and it compiles just now. If you’re curious and interpid, the darcs repo is at http://www.e-pig.org/darcs/Pig09 and highly volatile.
It’s a joy to have a great bunch of people working on this. I’d like to grow that hacking community. I’ll try to write more usefully about what’s going on in the not too distant future.