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

[Conor McBride]

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