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

[Keean Schupke]

Conor,

    I thought you might like this... It shows how to do this without 
phantom types! (we just use scoped type variables to help the 
typechecker sort things out)... What do you think? Does this overcome 
all the problems with Olegs approach? (the only slight problem I have 
found is that you must give the parameters explicitly for definitions 
like test3)

 >test3 a = (runExpression s) (runExpression k) (runExpression k) a

But it doesn't require type annotations!

[If you want to see a scary type, do ":type test3" in ghci]

The key is the change to this instance:

 >instance (OpenExpression t1 env (a -> r),OpenExpression t2 env a)
 >        => OpenExpression (Application t1 t2) env r where
 >    openExpression (Application t1 t2) env =
 >        (openExpression t1 env :: a -> r)
 >        (openExpression t2 env :: a)


I have attached a version ready to run in ghci.

    Keean


Conor McBride wrote:

> 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...
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: expression.hs
Type: text/x-haskell
Size: 2125 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20050103/cb39237b/expression.bin