[Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs

[Conor McBride]

Hello all

oleg at pobox.com wrote:
> Ashley Yakeley wrote on the first day of 2005:
> 
>>This compiled with today's CVS GHC 6.3. I don't think you can do this
>>without GADTs.
> 
> It seems we can do without GADT -- roughly with the same syntax
> (actually, the syntax of expressions is identical -- types differ and
> we have to write `signatures' -- i.e., instance declarations). Tested
> with GHC 6.2.1.

So Ashley sets a challenge and Oleg overcomes it. Well done! But rather
than working on the level of examples, let's analyse the recipe a little.

First take your datatype family (I learned about datatype families too
long ago to adjust to this annoying new "GADT" name)...

> -- data OpenExpression env r where
> --   Lambda :: OpenExpression (a,env) r -> OpenExpression env (a -> r);
> --   Symbol :: Sym env r -> OpenExpression env r;
> --   Constant :: r -> OpenExpression env r;
> --   Application :: OpenExpression env (a -> r) -> OpenExpression env a -> 
> --                  OpenExpression env r

...and throw away all the structure except for arities

data Thing = FirstSym | NextSym Thing | Lambda Thing | Symbol Thing
            | Constant Thing | Application Thing Thing

Next, jack up the unstructured values to their type level proxies,
replacing type Thing by kind *.

data FirstSym = FirstSym
data NextSym thing = NextSym thing
...
data Application thing1 thing2 = Application thing1 thing2

We now have an untyped representation of things. This is clearly progress.
Next, use type classes as predicates to describe the things we want: where
we had

    value :: Family index1 .. indexn

we now want

    instance FamilyClass proxy index1 .. indexn

eg

 > instance OpenExpression t (a,env) r =>
 >   OpenExpression (Lambda a t) env (a->r)

Whoops! Can't write

instance (OpenExpression t1 env (arg->r),
	  OpenExpression t2 env arg)
     => OpenExpression (Application t1 t2) env r

because the instance inference algorithm will refuse to invent arg.
Fix: get the type inference algorithm to invent it instead, by making
Application a phantom type:

data Application arg thing1 thing2 = Application thing1 thing2

Hence we end up using * as a single-sorted language of first-order
proxies for data, with classes acting as single-sorted first-order
predicates.

> class OpenExpression t env r
> data Lambda a t = Lambda t deriving Show
> data Symbol t = Symbol t deriving Show
> data Constant r = Constant r deriving Show
> data Application a t1 t2 = Application t1 t2 deriving Show
> 
> instance OpenExpression t (a,env) r => OpenExpression (Lambda a t) env (a->r)
> instance SymT t env r => OpenExpression (Symbol t) env r
> instance OpenExpression (Constant r) env r
> instance (OpenExpression t1 env (a->r),
> 	  OpenExpression t2 env a)
>     => OpenExpression (Application a t1 t2) env r

Where now? Well, counterexample fiends who want to provoke Oleg into
inventing a new recipe had better write down a higher-order example.
I just did, then deleted it. Discretion is the better part of valour.

Or we could think about programming with this coding. It turns out that
the 'goodness' predicate doesn't behave like a type after all! For
each operation which inspects elements, you need a new predicate: you
can't run the 'good' terms, only the 'runnable' terms. You can require
that all runnables are good, but you can't explain to the compiler
why all good terms are runnable.

The latter also means that the existential type encoding of 'some good
term' doesn't give you a runnable term. There is thus no useful
future-proof way of reflecting back from the type level to the term
level. Any existential packaging fixes in advance the functionality
which the hidden data can be given: you lose the generic functionality
which real first-order data possesses, namely case analysis.

So what have we? We have a splendid recipe for taking up challenges:
given a fixed set of functionality to emulate, crank the handle. This may
or may not be the same as a splendid recipe for constructing reusable
libraries of precise data structures and programs.

Happy New Year!

Conor

PS The datatype family presentation of simply-typed lambda-calculus has
been around since 1999 (Altenkirch and Reus's CSL paper). It's not so
hard to write a beta-eta-long-normalization algorithm which goes under
lambdas. Writing a typechecker which produces these simply-typed terms,
enforcing these invariants is also quite a laugh...

-- 
http://www.cs.nott.ac.uk/~ctm