Type level environment in Haskell

Question

I'm trying to use some Haskell extensions to implement a simple DSL. A feature that I'd like is to have a type level context for variables. I know that this kind of thing is common place in languages like Agda or Idris. But I'd like to know if is possible to achieve the same results in Haskell.

My idea to this is to use type level association lists. The code is as follows:

{-# LANGUAGE GADTs, 
         DataKinds, 
         PolyKinds, 
         TypeOperators, 
         TypeFamilies, 
         ScopedTypeVariables, 
         ConstraintKinds, 
         UndecidableInstances #-}

import Data.Proxy    
import Data.Singletons.Prelude   
import Data.Singletons.Prelude.List

import GHC.Exts    
import GHC.TypeLits

type family In (s :: Symbol)(a :: *)(env :: [(Symbol, *)]) :: Constraint where
     In x t '[] = ()
     In x t ('(y,t) ': env) = (x ~ y , In x t env)


data Exp (env :: [(Symbol, *)]) (a :: *) where
     Pure :: a -> Exp env a
     Map  :: (a -> b) -> Exp env a -> Exp env b        
     App  :: Exp env (a -> b) -> Exp env a -> Exp env b        
     Set :: (KnownSymbol s, In s t env) => proxy s -> t -> Exp env ()
     Get :: (KnownSymbol s, In s t env) => proxy s -> Exp env t


test :: Exp '[ '("a", Bool), '("b", Char) ]  Char
test = Get (Proxy :: Proxy "b")        

Type family In models a type level list membership constraint that is used to ensure that a variable can only be used if it is on a given environment env.

The problem is that GHC constraint solver isn't able to entail the constraint In "b" Char [("a",Bool), ("b",Char)] for test function, giving the following error message:

Could not deduce (In "b" Char '['("a", Bool), '("b", Char)])
   arising from a use of ‘Get’
In the expression: Get (Proxy :: Proxy "b")
In an equation for ‘test’: test = Get (Proxy :: Proxy "b")
Failed, modules loaded: Main.

I'm using GHC 7.10.3. Any tip on how can I solve this or an explanation of why this isn't possible is highly welcome.

Answer 1

Your In is not what you think - it's actually more like All. A value of type In x t xs is a proof that every element of the (type-level) list xs is equal to '(x,t).

The following GADT is a more usual proof of membership:

data Elem x xs where
    Here :: Elem x (x ': xs)
    There :: Elem x xs -> Elem y (x ': xs)

Elem is like a natural number but with more types: compare the shape of There (There Here) with that of S (S Z). You prove an item is in the list by giving its index.

For the purposes of writing a lambda calculus type checker, Elem is useful as a de Bruijn index into a (type-level) list of types.

data Ty = NatTy | Ty ~> Ty

data Term env ty where
    Lit :: Nat -> Term env NatTy
    Var :: Elem t env -> Term env t
    Lam :: Term (u ': env) t -> Term env (u ~> t)
    ($$) :: Term env (u ~> t) -> Term env u -> Term env t

de Bruijn indices have great advantages for compiler writers: they're simple, you needn't worry about alpha-equivalence, and in this example you don't have to mess around with type-level lookup tables or Symbols. But no one in their right mind would ever program in a language with de Bruijn indices, even with a type checker to help. This makes them a good choice for an intermediate language in a compiler, to which you'd translate a surface language with explicit variable names.

Type-level environments and de Bruijn indices are both rather complicated, so you should ask yourself: who is the target audience for this language? (and: is a type-level environment worth the costs?) Is it an embedded DSL with expectations of familiarity, simplicity, and performance? If so I'd consider a deeper embedding using higher-order abstract syntax. Or is it to be used as an intermediate language, for whom the primary audience is yourself, the compiler writer? Then I'd use a library like Kmett's bound to take care of variable binding and suck up the possibility of type errors because they could happen anyway.

For more on type-level environments et al, see The View from the Left for (as far as I know) the first example of a statically-checked lambda calculus type-checker embedded in a dependently-typed programming language. Norell gives an Agda-flavoured exposition of the same program in the Agda tutorial and a series of lectures. See also this question which seems relevant to your use-case.

Answer 2

In generates impossible constraints:

In "b" Char '['("a", Bool), '("b", Char)] =
("b" ~ "a", ("b" ~ "b", ())

It's a conjunction and it has an impossible element "a" ~ "b", so it's impossible overall.

Moreover, the constraint doesn't tell us anything about Char which I assume is the looked-up value.

The simplest way would be directly using a lookup function:

type family Lookup (s :: Symbol) (env :: [(Symbol, *)]) :: * where
  Lookup s ('(s  , v) ': env) = v
  Lookup s ('(s' , v) ': env) = Lookup s env

We can use Lookup k xs ~ val to put constraints on the looked-up types.

We could also return Maybe *. Indeed, the Lookup in Data.Singletons.Prelude.List does that, so that can be used too. However, on the type level we can often get by with partial functions, since type family applications without a matching case get stuck instead of throwing errors, so having a value of type Lookup k xs :: * is already sufficient evidence that k is really a key contained in xs.