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
[EMAIL PROTECTED] 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...
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
module Expression where
data FirstSym = FirstSym deriving Show
data NextSym t = NextSym t deriving Show
class SymT t env r
instance SymT FirstSym (r,xx) r
instance SymT t env r => SymT (NextSym t) (a,env) r
class SymT t env r => RunSym t env r | t env -> r where
runSym :: t -> env -> r
instance RunSym FirstSym (r,xx) r where
runSym _ (r,xx) = r
instance RunSym var env r => RunSym (NextSym var) (a,env) r where
runSym (NextSym var) (a,env) = runSym var env -- the code literally
data Lambda a t = Lambda t deriving Show
data Symbol t = Symbol t deriving Show
data Constant r = Constant r deriving Show
data Application t1 t2 = Application t1 t2 deriving Show
class OpenExpression t env r | t env -> r where
openExpression :: t -> env -> r
instance OpenExpression t (a,env) r => OpenExpression (Lambda a t) env (a -> r) where
openExpression (Lambda exp) env = \a -> openExpression exp (a,env)
instance RunSym t env r => OpenExpression (Symbol t) env r where
openExpression (Symbol var) env = runSym var env
instance OpenExpression (Constant r) env r where
openExpression (Constant r) _ = r
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)
newtype Expression t r = MkExpression (forall env. OpenExpression t env r => t)
runExpression (MkExpression e) = openExpression e ()
sym0 = Symbol FirstSym
sym1 = Symbol (NextSym FirstSym)
sym2 = Symbol (NextSym (NextSym FirstSym))
k = MkExpression (Lambda (Lambda sym1))
s = MkExpression (Lambda (Lambda (Lambda (Application (Application sym2 sym0) (Application sym1 sym0)))))
test1 = (runExpression k) sym0 sym2
test2 = (runExpression k) sym2 sym0
runS a b = (runExpression s) a b
runK a b = (runExpression k) a b
test3 a = (runExpression s) (runExpression k) (runExpression k) a
test3' = test3 "It's the identity!!! Look at the type!!!"
test3'' = test3 (27 :: Int)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
