Hello all oleg@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