Epilogue

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.

Fresh from my practice with Haskell, I built a lexer and layout manager for Epigram 2 today. You can

darcs get http://www.e-pig.org/darcs/Pig09/

for not much action. But I start as I hope to continue, with all the source living in an lhs2TeX document — the ‘Epitome’:

make dvi

and you’re away.

I promise not to implement λ-calculus again until I’ve written a parser to feed it.

The plan, by the way, is to implement an electrical stooge, a kind of annoying co-author who reads what you’ve done and comments out the bits which don’t typecheck. In time, you may be able to persuade this unlikely conspirator also to do some work.

She’s got idiom brackets now. A parser example.

> import Parsley

> data Exp
>   = V Char
>   | Neg Exp
>   | Exp :+: Exp
>   deriving Show

> pExp :: P Char Exp
> pExp =
>   (| Neg {teq '-'} pExp
>    | {teq '('} pExp :+: {teq '+'} pExp {teq ')'}
>    | V (tok isAlpha)
>    |)

You can write a bunch of alternatives in (| .. | .. | .. |) each alternative is an application (possibly infix) whose function is taken as pure, and whose arguments are effectful. Additional noise, contributing effects but no values can be inserted with { .. ; .. }. I know, I’ve stolen record update syntax. Boo hoo.

More in a bit.

We like to organise Epigram source by feature rather than by component. Nicolas and I wrote some dodgy scissors-and-stickytape code to rearrange our files before we compiled them, along with some bad Makefile voodoo. I’ve built more or less the same functionality into she, so it’s just as dodgy, but the build is easier. Here’s an example trio of files.

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, KindSignatures, GADTs #-}
> module Pig where

> import Control.Applicative
> import Data.Char
> import Parsley

> import Hig
> import Jig

> data ExpF :: * -> * where
>   import < - ExpF

> instance Functor ExpF where
>   import < - FunctorExpF

> data Free :: (* -> *) -> * -> * where
>   V :: x -> Free f x
>   C :: f (Free f x) -> Free f x

> fEval :: Functor f => (x -> t) -> (f t -> t) -> Free f x -> t
> fEval g f (V x)  = g x
> fEval g f (C fe) = f (fmap (fEval g f) fe)

> type Exp = Free ExpF
> import < - ExpPS

> eval :: (x -> Int) -> Exp x -> Int
> eval g = fEval g $ \ e -> case e of
>   import < - EvAlg

> pExp :: P Char (Exp Char)
> pExp = V < $> tok isAlpha
>   import < - EvParser

What are these import ← Blah things? Read the rest of this entry »

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators #-}

> module Fix where

> data Fix f = In (f (Fix f))

> newtype (:+:) f g x = Plus (Either (f x) (g x))
> newtype (:*:) f g x = Times (f x, g x)
> newtype K a x = K a
> newtype I x = I x

> type ListF x = K () :+: (K x :*: I)

> type List x = Fix (ListF x)

> pattern NilF = Plus (Left (K ()))
> pattern ConsF x xs = Plus (Right (Times (K x, I xs)))
> pattern Nil = In NilF
> pattern Cons x xs = In (ConsF x xs)

> foldFix :: Functor f => (f t -> t) -> Fix f -> t
> foldFix phi (In xs) = phi (fmap (foldFix phi) xs)

> (+++) :: List x -> List x -> List x
> xs +++ ys = foldFix phi xs where
>   phi NilF = ys
>   phi (ConsF x xs) = Cons x xs

> blat :: List x -> [x]
> blat = foldFix phi where
>   phi NilF = []
>   phi (ConsF x xs) = x : xs

> talb :: [x] -> List x
> talb = foldr Cons Nil

> instance (Functor f, Functor g) => Functor (f :+: g) where
>   fmap p (Plus (Left fx)) = Plus (Left (fmap p fx))
>   fmap p (Plus (Right gx)) = Plus (Right (fmap p gx))

> instance (Functor f, Functor g) => Functor (f :*: g) where
>   fmap p (Times (fx, gx)) = Times (fmap p fx, fmap p gx)

> instance Functor (K a) where
>   fmap p (K a) = K a

> instance Functor I where
>   fmap p (I a) = I (p a)

I’ve pushed some patches, and now it is!

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# OPTIONS #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE KindSignatures #-}

> module Vec where

> import Control.Applicative

> data Nat = Z | S Nat

> data Vec :: {Nat} -> * -> * where
>   VNil :: Vec {Z} x
>   (:>) :: x -> Vec {n} x -> Vec {S n} x

> vtail :: Vec {S n} x -> Vec {n} x
> vtail (x :> xs) = xs

> vapp :: Vec {n} (s -> t) -> Vec {n} s -> Vec {n} t
> vapp VNil VNil = VNil
> vapp (f :> fs) (s :> ss) = f s :> vapp fs ss

Yes, in a manner of speaking. But you need a bit of

darcs get http://personal.cis.strath.ac.uk/~conor/pub/she

Update: she’s on hackage!

Update: I had to…

> type family (m :: {Nat}) :+ (n :: {Nat}) :: {Nat}
> type instance {Z} :+ n = n
> type instance {S m} :+ n = {S} (m :+ n)

> vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x
> vappend VNil ys = ys
> vappend (x :> xs) ys = x :> vappend xs ys