[Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs
Conor McBride
ctm at cs.nott.ac.uk
Mon Jan 3 07:54:59 EST 2005
Hi again
Actually, things are a little weirder than I first thought...
Me:
>>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.
Ashley:
> If I understand you correctly, without GADTs/datatype families, you
> cannot create Expression as a type-constructor without Oleg's auxiliary
> "t" argument that in fact encodes the structure of the expression. Is
> that right? I certainly can't see any way of getting rid of it: if, as
> you say, you existentially package it, the compiler can't deduce
> runnability.
It is possible to quantify the t existentially. It's even possible to
quantify the t existentially and the env universally. Here's a cut down
version, without the operational semantics:
module Fam where
data Top = Top
data Pop i = Pop i
data Var i = Var i
data Lam s e = Lam e
data App {-s-} e1 e2 = App e1 e2
{- I was wrong: instance inference is quite happy without the s, but... -}
class GoodVar i env t | i env -> t where {}
instance GoodVar Top (env, t) t where {}
instance GoodVar i env t => GoodVar (Pop i) (env, s) t where {}
class GoodExp e env t | e env -> t where {}
instance GoodVar i env t => GoodExp (Var i) env t where {}
instance GoodExp e (env, s) t => GoodExp (Lam s e) env (s -> t) where {}
instance (GoodExp e1 env (s -> t), GoodExp e2 env s) =>
GoodExp (App {-s-} e1 e2) env t
{- ...nothing works without the fundeps, so you need the argument type
on Lam, which I suppose isn't surprising -}
{- This does suggest that this recipe may not always be usable, or may
require a lot of hand-annotation, where there is no fundep to be had. -}
{- hiding the witness, leaving just a type family with the original
indices -}
data Exp env t = forall e. GoodExp e env t => MkExp e
{- demanding, moreover, arbitrariness of environment -}
data UExp t = forall e. MkUExp (forall env. GoodExp e env t => e)
{- the usual suspects -}
s :: Exp env ((r -> s -> t) -> (r -> s) -> r -> t)
s = MkExp (Lam (Lam (Lam (App (App (Var (Pop (Pop Top))) (Var Top))
(App (Var (Pop Top)) (Var Top))))))
k :: Exp env (x -> r -> x)
k = MkExp (Lam (Lam (Var (Pop Top))))
us :: UExp ((r -> s -> t) -> (r -> s) -> r -> t)
us = MkUExp (Lam (Lam (Lam (App (App (Var (Pop (Pop Top))) (Var Top))
(App (Var (Pop Top)) (Var Top))))))
uk :: UExp (x -> r -> x)
uk = MkUExp (Lam (Lam (Var (Pop Top))))
However, the point remains that having an Exp env t does you no good,
because you can't deduce any functionality from mere goodness. It's
just the usual problem with abstract datatypes, really. I wonder if
there's some awful half-baked discriminator-selector interface to
these things.
Cheers
Conor
--
http://www.cs.nott.ac.uk/~ctm
More information about the Haskell-Cafe
mailing list