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

[Conor McBride]

Hello again

Keean Schupke wrote:
> Conor McBride wrote:
> 
>>
>> Yeah, that's nice. Scoped type variables are really handy for this sort
>> of thing. You've got rid of the annotation on application (hey, what are
>> typecheckers for?) but it's not so easy to lose it on the lambda: you
>> need that for the fundep. To have a good story here, we need to show
>> either how to get rid of the fundep or how to ensure we always have one.
>>
> However I don't understand what you meed by 'ensuring you always have 
> one'... As far as I understand it we are lifting a value level operation (a type 
> with several constructors) to the type level (a class containing several 
> types) in this case each 'class' models a function.

I'm not sure that's quite the picture. We're using classes as predicates here,
to define when a type-level proxy stands for a well-indexed piece of data. The
fundep asserts that the proxy determines an index. In the expression example,
an expression proxy is supposed to determine the type index (but not the
environment index), hence the Lambda proxy must carry the argument type.
The whole thing seems to fall apart without this fundep, although I don't
see precisely why just now. But I think it's always possible and usually
sensible to add enough phantom arguments to ensure that the fundep is
available.

Here's another variation: this time, the open expressions are equipped with a
dependent case analysis operator. As Oleg has pointed out, you don't need to
go that far to write eval, but I did anyway.

data Top = Top
data Pop i = Pop i
data Var i = Var i
data Lam s e = Lam e
data App e1 e2 = App e1 e2

data Inx env t = forall i . GoodInx i env t => Inx i
class GoodInx i env t | i env -> t where
   inxCase :: i ->
              (forall env'. p Top (env', t) t) ->
              (forall env' i' s' t'. GoodInx i' env' t =>
                 i' -> p (Pop i') (env', s') t) ->
              p i env t
instance GoodInx Top (env, t) t where
   inxCase Top mTop mPop = mTop
instance GoodInx i env t => GoodInx (Pop i) (env, s) t where
   inxCase (Pop i) mTop mPop = mPop i

data Exp env t = forall e. GoodExp e env t => Exp e
class GoodExp e env t | e env -> t where
   expCase :: e ->
              (forall i' env' t'. GoodInx i' env' t' =>
               i' -> p (Var i') env' t') ->
              (forall i' env' e' s' t'. GoodExp e' (env', s') t' =>
               e' -> p (Lam s' e') env' (s' -> t')) ->
              (forall i' env' e1' e2' s' t'.
               (GoodExp e1' env' (s' -> t'), GoodExp e2' env' s') =>
               e1' -> e2' -> p (App e1' e2') env' t') ->
              p e env t
instance GoodInx i env t => GoodExp (Var i) env t where
   expCase (Var i) mVar mLam mApp = mVar i
instance GoodExp e (env, s) t => GoodExp (Lam s e) env (s -> t) where
   expCase (Lam e) mVar mLam mApp = mLam e
instance (GoodExp e1 env (s -> t), GoodExp e2 env s) =>
   GoodExp (App {-s-} e1 e2) env t where
   expCase (App e1 e2) mVar mLam mApp = mApp e1 e2

data Sem x env t = Sem {sem :: env -> t}

evalInx :: GoodInx i env t => i -> Sem i env t
evalInx i = inxCase i
   (Sem (\ (_, t) -> t))
   (\ i -> Sem (\ (env, _) -> sem (evalInx i) env))

evalExp :: GoodExp e env t => e -> Sem e env t
evalExp e = expCase e
   (\ i -> Sem (\env -> sem (evalInx i) env))
   (\ e -> Sem (\ env arg -> sem (evalExp e) (env, arg)))
   (\ e1 e2 -> Sem (\ env -> sem (evalExp e1) env (sem (evalExp e2) env)))

Meanwhile, I thought I'd write some more dependent programs, with the
ubiquitous finite set family.

{- We need natural numbers, equipped with case analysis -}

data Nat = forall n. (GoodNat n) => Nat n
class GoodNat n where
   natCase :: n ->
     (p Zero) ->
     (forall n'. GoodNat n' => n' -> p (Suc n')) ->
     p n

data Zero = Zero
instance GoodNat Zero where
   natCase Zero mZero mSuc = mZero
zero :: Nat
zero = Nat Zero

data Suc n = Suc n
instance GoodNat n => GoodNat (Suc n) where
   natCase (Suc n) mZero mSuc = mSuc n
suc :: Nat -> Nat
suc (Nat n) = Nat (Suc n)

{- Now we can develop a family of sized finite types -}

data Fin n = forall i. (GoodFin i n) => Fin i
class GoodNat n => GoodFin i n | i -> n where
   finCase :: i ->
     (forall n'. GoodNat n' => p (FZ n') (Suc n')) ->
     (forall n' i'. GoodFin i' n' => i' -> p (FS i') (Suc n')) ->
     p i n

data FZ n = FZ {- phantom for the fundep -}
instance GoodNat n => GoodFin (FZ n) (Suc n) where
   finCase FZ mFZ mFS = mFZ
fz :: GoodNat n => Fin (Suc n)
fz = Fin FZ

data FS i = FS i deriving
instance GoodFin i n => GoodFin (FS i) (Suc n) where
   finCase (FS i) mFZ mFS = mFS i
fs :: GoodNat n => Fin n -> Fin (Suc n)
fs (Fin i) = Fin (FS i)

{- Every nonempty finite set has a largest element.
    Here we must really do dependent case analysis on
    the number. -}

data PMax n = PMax {pMax :: Fin (Suc n)}

fmax :: GoodNat n => n -> Fin (Suc n)
fmax n = pMax (natCase n (PMax fz)
                          (\n -> PMax (fs (fmax n))))

{- There's a constructor-preserving embedding from
    each finite set to the next. -}

data PWeak i n = PWeak {pWeak :: Fin (Suc n)}

fweak :: GoodNat n => Fin n -> Fin (Suc n)
fweak (Fin i) = pWeak (finCase i
                         (PWeak fz)
                         (\j -> PWeak (fs (fweak (Fin j)))))


Now, before we get too excited about having some sort of case
analysis principle, observe that all of these examples involve
computing with unconstrained data: an expression of any type,
an element of any finite set, etc. There's more to case analysis
on datatype familes than that. You need to be able to handle
constrained data too: an expression of type Int (which can't be
Lambda), an element of the set of size two (which is FZ or
FS FZ, but nothing larger). That's where the fun starts, and
having unification in the typing rules is really rather handy.

First test: to write

lift :: forall n. (GoodNat m, GoodNat n) =>
         (Fin m -> Fin n) -> Fin (Suc m) -> Fin (Suc n)
-- as it were,
-- lift f fz = fz
-- lift f (fs i) = fs (f i)

But I've plenty more where that came from. The old ones are the
best...

Cheers

Conor

-- 
http://www.cs.nott.ac.uk/~ctm