Epilogue

Over the last few weeks, there have been some changes to Epigram that make programming in the command-line interface slightly more pleasant. We are starting to think about a high-level language, but in the meantime, I thought it would be nice to look at what sort of programming is possible today. None of this is revolutionary or indeed particularly exciting, but it should make the exciting stuff easier to write. This post would be literate Epigram if there was such a thing; as there isn’t, you will have to copy code lines one at a time into Pig if you want to follow along.

Read the rest of this entry »

I think we’re at a point where we need to question our term/value representation technology. That’s not to say we need to change it, but we should look at where things are getting a bit out of hand and ask if there’s anything we can do. The system is not so large that…actually, it’s small. However, before we do anything foolish, I thought I’d try to remember where we’ve been and why. Please join in. We need to figure out what breaks what. Most representation choices have pros and cons (a few just have cons).

Where are we at the moment? Read the rest of this entry »

Here’s a story I’ve had on the go for a while.

It’s an experiment in managing the multitudinous variations on the theme of a datatype, inspired by this overlay from a talk I gave ten years ago. If you squint hard at it, you can see that it shows the difference between lists and vectors. Let’s see how to formalize that notion as a big pile of Agda. The plan, of course, is to do something very like this for real on Epigram’s built in universe of datatypes.

I’ll need some bits and bobs like Sigma-types (Sg). Step one. Build yourself a little language describing indexed functors.

Descriptions


data Desc (I : Set) : Set1 where
  say : I -> Desc I
  sg : (S : Set)(D : S -> Desc I) -> Desc I
  ask_*_ : I -> Desc I -> Desc I

What do these things mean?

[_] : forall {I} -> Desc I -> (I -> Set) -> (I -> Set)
[ say i' ] X i = i' == i
[ sg S D ] X i = Sg S \ s -> [ D s ] X i
[ ask i' * D ] X i = X i' * [ D ] X i

Here, [ D ] X i is the set of D-described data which say they have index i; everywhere the description asks for some index i’, the corresponding set has an X i’. Meanwhile sg just codes for ordinary Sg-types, allowing nodes of datatypes to be built like dependent records. The X marks the spot for recursive data. Our next move is to take a fixpoint.

data Data {I : Set}(D : Desc I)(i : I) : Set where
  <_> : [ D ] (Data D) i -> Data D i

I guess I’d better give you an example. Read the rest of this entry »

In this post, I talk about the computation of normal forms in Epigram. Quotation is a key step of normalization, doing some rather exciting magic.

Setting the scene

This post tells a story about terms. We shall discover that some classes of term are more desirable than others. Let us have a look at the battlefield. We define 3 classes of terms, gently sketched by Bosch:

Read the rest of this entry »

I thought I would write a line or two about some recently acquired infrastructure.

Weeks ago, we had left our ivory tower, or rather, our beloved Livingstone tower for a gig in Oxford. Lot of fun, lot of adjunctions. But also a surprising discovery: we met some people who had pulled Epigram source code and actually looked at it. I mean, I might have pulled the code once or twice in the past, to impress girls in a Pub. But reading it…

Worse, we actually got our first bug report! Andrea Vezzosi, as a modern Dante Alighieri, braved the Inferno of She-ism (translates to “shitism” in Italian for some reason) and somehow went through the Purgatorio of Epigram’s syntax (honestly, I have no clue how he did that). Once there, Paradiso was at hand. But these damned labels were preventing the magic from happening! No mailing list, no bug tracker: no hope.

Around the same time, our counter-intelligence team reported that several Epigram agents under cover in Sweden had been busted and exposed to bursts of .45mm questions.

All in all, we came to the conclusion that, out there, there are people working harder on Epigram than we do. So, here is the kit for you to become an Epigram implementor:

• A mailing list!
• A bug tracker!
• An IRC channel, #epigram on Freenode

If you don’t feel like becoming a modern hero (tough job, indeed), you are also welcome to come on board and have a chat with the captain.

I’m putting a rough skeleton of my PhD thesis in the repository. I’m off to Honolulu, will be back in 3 years. Keep up the good work folks!

Let me try to make a bit of high-level sense about Prop in Epigram 2. It’s quite different from Prop in Coq, it does a different job, and it sits in quite a delicate niche.

Firstly, Prop is explicitly a subuniverse of Set. If P is a Prop, then :- P is the set of its proofs, but P itself is not a type. (Are propositions types? How, functionally, should the Curry-Howard “isomorphism” be manifest?) Note that :- is a canonical set constructor; it is preserved by computation. Hence you know a proof set when you see one.

Secondly, we squash proof sets. All inhabitants of proof sets are considered equal, definitionally. We have that :- P ∋ p ≡ p’, and we can easily see when this rule applies, just because :- is canonical. Contrast this with Coq, where Prop is silently embedded in Type: that makes it harder to spot opportunities to squash proofs.

And that’s kind of it. Prop is a subuniverse of Set that’s safe to squash, even when computing with open terms. There’s nothing we do with Prop that we couldn’t do more clunkily in Set. It is, in effect, an optimization. However, the pragmatic impact of this optimization is considerable. More on what we’ve bought in a bit; let’s check that we can afford it.
Read the rest of this entry »

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.
Read the rest of this entry »

I thought I’d start writing a thing or two about the setup for the incarnation of Epigram we’re currently working on. At the heart of the thing is a Language Of Verifiable Evidence, which is all you need, really. You can stick a fancy syntax and lots of abbreviation mechanisms on top of it, and you can glue lots of erasure mechanisms and a compiler to the bottom of it, but in the middle, there’s this language whose (open) terms you can typecheck and evaluate, without any need for further elaboration, wishful thinking, or appeal to oracle. Is this a core language? I don’t know: that phrase has been used in so many ways.

The setup of this language is obsessively bidirectional, to the point of separating the syntactic categories for which types get pushed in and from which types are extracted.

Pushing types in: TYPE ∋ INTM
Extracting types: EXTM ∈ TYPE
Read the rest of this entry »

This may not seem startling, and it isn’t. It’s the first thing we check when we have a system that’s beginning to work. Today, we constructed + for the natural numbers by appeal to the generic elimination operator. Then we applied this + to two and two. Then we compiled the resulting definition to a standalone executable. Then we ran that executable. It printed four (in a suitable encoding). Dr Brady has been visiting, which helps with this sort of shenanigans.

When I say “the generic elimination operator”, I don’t mean the elimination operator for the natural numbers. I mean the generic elimination operator for all inductive datatypes, applied to the piece of data which describes the natural numbers. This version of Epigram has datatype-generic programming built in. So what we’ve really been doing is thrashing that datatype encoding mechanism. It seems to be working, so I’d better change it.

The long dark is ending. We’ve been hacking up bits of kit for ages, but we now have an end-to-end system: construction commands go in; compiled code comes out. Time to chuck in functionality and get playing!

Location: peripatetic. Exeunt: Peter and James. Brunch: Rio Café. Cake: The Liquid Ship. Enter: our web consultant.

Today, less hacking, more packing. Some plotting.

It’s been a good week. We have the infrastructure for the core theory, and we’re populating it with stuff. Peter is well on the way to the universe of containers: more on that in another post. James is getting in the zone with Observational Equality. Conor is trying to figure out how the elaboration monad comes together, and fixing She. Edwin has shown us how to communicate with his Epic compiler.

We’ll have a version of the core, its typechecker, and its compiler pretty soon, I think. The challenge now is to design the high-level source language. I can’t help feeling that we should think about effects sooner rather than later.

Location: Livingston Tower – University of Strathclyde.
Clientele: Conor, Peter, James, Edwin.
Lunch: Oko.
Cake; Fifi and Ally’s.
Dinner: La Valleé Blanche.

Bit of propositional equality (James), bit of container technology (Peter) and some actual computation (Edwin). Conor continues to keep us well fed, well watered and well stocked with things to manufacture, he’s also keeping She in working order. The end of a productive week is drawing near. Edwin has gone back to St. Andrews, Peter and I are off tomorrow. It’s been good, hope to be back soon.

Location: Conor’s Flat. Crew: Conor T. McBride, Peter W.J. Morris, James M. Chapman, Edwin C. Brady, joined for the afternoon by Nicolas P. Oury.
Lunch: Crabshakk
Cake: Kember and Jones
Dinner: Banana Leaf

Achievements: PWJM implemented a universe for containers, JMC worked on updating the proof state, ECB plugged his compiler in and learned his way around the source code, CTM successfully loaded and typechecked a term, while continuing to update She, and NPO got up to speed with the state of the system.

Here are terms and values, bidirectionally. Inevitably, I can’t decide what to call things and forgot what I did last time.

> data Dir    = In | Ex
> data Phase  = TT | VV
>
> data Tm :: {Dir, Phase} -> * -> * where
>   L     :: Scope p x           -> Tm {In, p} x
>   C     :: Can (Tm {In, p} x)  -> Tm {In, p} x
>   N     :: Tm {Ex, p} x        -> Tm {In, p} x
>   P     :: x                   -> Tm {Ex, p} x
>   V     :: Int                 -> Tm {Ex, TT} x
>   (:-)  :: Tm {Ex, p} x -> Elim (Tm {In, p} x) -> Tm {Ex, p} x
>   (:?)  :: Tm {In, TT} x -> Tm {In, TT} x -> Tm {Ex, TT} x
>
> data Scope :: {Phase} -> * -> * where
>   (:.)  :: String -> Tm {In, TT} x         -> Scope {TT} x
>   H     :: Env -> String -> Tm {In, TT} x  -> Scope {VV} x
>   K     :: Tm {In, p} x                    -> Scope p x
>
> data Can :: * -> * where
>   Set   :: Can t
>   Pi    :: t -> t -> Can t
>   deriving (Show, Eq)
>
> data Elim :: * -> * where
>   A :: t -> Elim t
>   deriving (Show, Eq)

And there’ll be more, no doubt. The parser is a bit scrappy.

The evaluator is idiombastic:

> ($-) :: VAL -> Elim VAL -> VAL
> L (K v)      $- A _  = v
> L (H g _ t)  $- A v  = eval t (g :< v)
> N n          $- e    = N (n :- e)

> body :: Scope {TT} REF -> Env -> Scope {VV} REF
> body (K v)     g = K (eval v g)
> body (x :. t)  g = H g x t

> eval :: Tm {d, TT} REF -> Env -> VAL
> eval (L b)     = (|L (body b)|)
> eval (C c)     = (|C (eval ^$ c)|)
> eval (N n)     = eval n
> eval (P x)     = (|(pval x)|)
> eval (V i)     = (!. i)
> eval (t :- e)  = (|eval t $- (eval ^$ e)|)
> eval (t :? _)  = eval t

where ^$ is a short infix name for traverse.