More on type safe lookup for heterogeneous lists in Haskell

Question

I'm trying to have some fun with dependently typed programming in Haskell, more specifically with type safe lookup operation. Previously, I've asked about how to implement a lookup operation for the following data type:

data Attr (xs :: [(Symbol,*)]) where
   Nil  :: Attr '[]
   (:*) :: (Sing s, t) -> Attr xs -> Attr ('(s , t) ': xs)

And I've got the answer:

lookupAttr :: (Lookup s env ~ 'Just t) => Sing s -> Attr env -> t
lookupAttr s ((s', t) :* env') = case s %:== s' of
   STrue  -> t
   SFalse -> lookupAttr s env'

That works fine. Now, I want to define a heterogeneous list of values of typed syntax, represented by type Exp:

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeOperators, PolyKinds #-}
import Data.Singletons.Prelude.List
import Data.Singletons.Prelude.Bool
import Data.Singletons.Prelude.Eq

data Exp (env :: [(Symbol,*)]) :: * -> * where
   Value :: String -> Exp env String
   Var :: (Lookup s env ~ 'Just t) => Sing s -> Exp env t
   Op :: Exp env t -> Exp env t -> Exp env t

The heterogeneous list type is defined by Env data type:

data Env (env :: [(Symbol,*)]) where
  Nil  :: Env '[]
  Cons :: (Lookup s' env ~ 'Nothing) =>
         (Sing s' ,
          Exp ('(s', a) ': env) a) ->
         Env env ->
         Env ('( s',a) ': env)

Using these data types, I define a lookup function using some sort of existential quantification (type Ex2):

data Ex2 (p :: k -> k' -> *) where
   Ex2 :: p e i -> Ex2 p

lookupEnv :: Lookup s env ~ 'Just t => Sing s -> Env env -> Ex2 Exp
lookupEnv s (Cons (s',e) env)
    = case s %:== s' of
         STrue -> Ex2 e
         SFalse -> lookupEnv s env

So far, so good. Now, I arrive at some interesting problems:

1) Is there a way to define lookupEnv without use this kind of existential quantification provided by type Ex2?

2) Suppose that I want to define a operation for modifying a giving entry in a value of type Env. The obvious attempt to define this function is

modifyEnv :: Lookup s env ~ 'Just t => Sing s -> Exp env t -> Env env -> Env env
modifyEnv s e (Cons (s',e') env')
     = case s %:== s' of
          STrue -> Cons (s', Op e e') env'
          SFalse -> Cons (s',e') (modifyEnv s e env')

Function modifyEnv compose some expression with another in the environment. This function isn't accepted by GHC which returns a cryptic error message. How could I define such modification function?

Cactus Cactus · Accepted Answer · 2016-06-20T03:19:22

I realize this is not a full solution because it doesn't use a Symbol-indexed Environment, but it might give you a good starting point. I am using a "typed de Bruijn index into a context" type instead:

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeOperators #-}

data Var (ctx :: [*]) :: * -> * where
    Here :: Var (a ': ctx) a
    There :: Var ctx a -> Var (b ': ctx) a

data Exp (ctx :: [*]) :: * -> * where
    Value :: String -> Exp ctx String
    Var :: Var ctx t -> Exp ctx t
    Op :: Exp ctx t -> Exp ctx t -> Exp ctx t

data Env (ctx :: [*]) where
    Nil :: Env '[]
    Cons :: Exp (a ': ctx) a -> Env ctx -> Env (a ': ctx)

This allows writing a typed version of lookupEnv, like so:

lookupEnv :: Env ctx -> Var ctx t -> Exp ctx t
lookupEnv (Cons e env) v = case v of
    Here -> e
    There v -> weaken $ lookupEnv env v

by making it possible to write the following weakening function:

weaken :: Exp ctx t -> Exp (a ': ctx) t
weaken (Value s) = Value s
weaken (Var v) = Var (There v)
weaken (Op f e) = Op (weaken f) (weaken e)

It seems to me that with using Symbol-indexed contexts, it is this last, weakening step that fails, because Lookup s ctx ~ Nothing doesn't seem to have enough structure for GHC to prove what you'd need for weaken (that you can shift the context since you know there's not going to be a shadowing issue).

More on type safe lookup for heterogeneous lists in Haskell

1 Answers