Coinduction, observationally

March 22nd, 2010

I thought I might report a bit about what I’ve been up to with coinduction. Headline: we can set up propositional equality so that every coprogram equals its unfolding, even though that had jolly well better not hold definitionally if we want decidable anything.

What I’ve got is an Agda universe with inductive and coinductive Petersson-Synek trees (also known as Hancock-Setzer interaction structures). Actually, it’s a pair of universes—PROP and SET. Equality is a proposition computed recursively over the structure of sets and elements.
Read the rest of this entry »

W-types: good news and bad news

March 7th, 2010

I thought I’d just collect together some disparate observations about W-types, and their use in encoding other recursive datatypes. My motivation, bluntly, is to point out the inevitable unsuitability of W-types as the basis for recursive datatypes in an implementation of decidable type theories. I don’t want to downplay the conceptual importance of W-types as a uniform basis for recursive structures in an extensional setting. I’m just saying that computers aren’t clever enough to cope all that well with W-type encodings: if we want to make our understanding go, we need to refine it. This is a long post, so if you want the bad news first, skip to the end.

What are W-types?

Martin-Löf identified a general notion of well-ordering — data with a well-founded notion of ‘structurally smaller’. The power of dependent types enabled him to express this parametrically, once for all, rather than by fiddling about with syntactic criteria for acceptable recursive definitions. Here goes (informal notation)

W (S : Set) (P : S → Set) : Set
(s : S) ⊲ (f : P s → W S P) : W S P
Read the rest of this entry »


February 8th, 2010

I’ve had an enquiry for more details on quotients in the new Epigram setup, so I’ll take that as a cue to blog a bit.

First, I’d better sketch some basics about propositions and equality. It’s the novel treatment of these things which lets us handle quotients in (hopefully) a neater way than has been possible thus far in a decidable type theory. The headlines:

  • quotients given by a ‘carrier’ set, equivalence relation
  • definitional equality on equivalence classes inherited from carrier on representatives
  • propositional equality on equivalence classes is equivalence of representatives
  • propositional equality is substitutive

The tabloid headline is STUFF YOUR SETOIDS.
Read the rest of this entry »

EE-PigWeek 4-9 Jan 2010

January 13th, 2010

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 »

Bidirectional Basics

January 3rd, 2010

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: TYPEINTM
Extracting types: EXTMTYPE
Read the rest of this entry »


December 18th, 2009

I’ve just uploaded a new version of Epic to hackage, so installing it should now be a matter of typing:

cabal install epic.

You will also need the Boehm garbage collector, available from here. If you’re on a Mac, installing it should require nothing more than:

port install boehmgc

Also, if you’re on a Mac, you will probably have to persuade gcc to look in the right place for the relevant libraries. I have the following lines in my .profile which do the trick:

export C_INCLUDE_PATH=/opt/local/include:$C_INCLUDE_PATH
export CPLUS_INCLUDE_PATH=/opt/local/include:$CPLUS_INCLUDE_PATH
export LD_LIBRARY_PATH=/opt/local/lib:$LD_LIBRARY_PATH
export LIBRARY_PATH=/opt/local/lib:$LIBRARY_PATH

To check if everything has worked, put the following text into a file called hello.e:

main () -> Unit =
   foreign Unit "putStr" ("Hello world!\n":String)

Then execute epic hello.e -o hello, and you should have an executable hello world program.


December 16th, 2009

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!

Autumn Leaves

December 6th, 2009

I thought I’d scribble something about what we’re up to. The team (Pierre-Évariste Dagand, Adam Gundry, Peter Morris, James Chapman) have been hard at work. I have been otherwise engaged. As a result, there has been considerable progress. Don’t worry. I expect I’ll mess things up properly over Christmas.

We’ve decided that the best way to get our new type theory out there for you to play with, sooner rather than later, is not to wrap it up in a new version of the Epigram language, but rather to present it as is, in a low-budget command-driven interactive proof assistant. This is beginning to materialise.

One of the good things about having new people in the team is that they’ve had to learn about how we get this stuff to work, and they’ve been writing down what they’re learning in the Epitome. Literate Programming Considered Essential. We’re not trying to take over the world: we’re just trying to make stuff worth stealing. That’s an unusual optimisation problem.

So, the rumours of our death have been slightly exaggerated. My plan is to continue staying out of the way of the coders and write more articles about How It All Works. We’re plotting a bit of a New Year hacking hooley in Tallinn (Glasgow isn’t cold enough). There might be a thing that does something a bit after that.

I’m hoping that this blog will wire up to the new repo real soon, so that you can peer on in. Afore I go, though, let me remark on the importance of Haskell as an enabling technology. Our engineering philosophy is do it once: we prefer to write one abstract piece of code which captures a concept than many concrete pieces of code which follow a pattern; without higher-kind types and classes, we’d be hosed. Given that our main implementation problem is (or rather, was) No Programmers, it is only because of Haskell that a thing exists at all.

PigWeek: Friday

July 25th, 2009

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.

Pigweek: Thursday

July 24th, 2009

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.

PigWeek: Wednesday

July 22nd, 2009

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.

PigWeek: Tuesday

July 21st, 2009

Location: Strathclyde Uni. Crew: C. McBride, P. Morris, J. Chapman and we welcomed the arrival of one E. Brady
Lunch: Peckham’s
Cake: Peckham’s
Dinner: we chopped, Mel cooked

Achievements: JC made a universe for propositions and PM one for finite enumerations; along the way they put together a setup for built-in operators. EB started to make his compiler do things in a more Pig-like way and CM built something that might load definitions into the system.

Tomorrow: The world.

PigWeek: Monday

July 21st, 2009

Location: Conor’s flat. Crew: Conor McBride, James Chapman, Peter Morris. Lunch: Cafézique. Cake from: Delizique. Dinner: Banana Leaf, Home Wok, Oriental West, the chippy.

Freddie Flintoff helped us to a cracking start by skittling the Aussie tail end. James implemented the setup for untyped quotation (β-normal forms), typed quotation (η-long β-normal forms), definitional equality, and bidirectional type checking.

Peter Morris implemented the feature file for Sigma-types, contributing code fragments to several components via the aspect-oriented programming technology which she supports. He also sorted out our Makefile, so that code gets preprocessed in the right order.

She is getting quite a lot of challenging work, so I’m on running repairs, and other boring jobs.

Wrote a parser; implemented λ-calculus again

July 11th, 2009

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.

New repo; new Epitome

July 10th, 2009

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

darcs get

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.

Idiom Brackets, take 1

July 7th, 2009

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.

The Strathclyde Haskell Enhancement

July 5th, 2009

She’s on hackage, ready to

cabal install she

and you should find that the repo has some web waffle attached to it.

I seem to have released some software. I’m as surprised as you are. No good can possibly come of it.

Higgledy-Piggledy rides again

July 4th, 2009

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 »

And is this Haskell?

June 30th, 2009

> {-# 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!

Is this Haskell?

June 30th, 2009

> {-# 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

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