Just a typed lambda calculus with failure, in Haskell

Question

I am new to Haskell, so I apologize if this question doesn't make much sense.

I want to be able to implement only typed lambda expressions in Haskell in such a way that when I try to apply the expression to another incorrect type, the result is not a type error, but rather some given value, for example. Nothing. At first I thought that using the Maybe monad would be the right approach, but I could not get anything to work. I wondered what, if any, would be the right way to do this.

The context of the problem, if that helps, is the project I'm working on that assigns POS tags (part of speech) to words in sentences. For my tag set, I use categorical grammar types; these are typed lambda expressions of the type (e -> s) or (e -> (e -> s)) , where e and s are types for nouns and sentences, respectively. So, for example, kill is of type (e -> (e -> s)) - it takes two noun phrases and returns a sentence. I want to write a function that takes a list of objects of these types, and finds out if there is a way to combine them to achieve an object of type s . Of course, this is exactly what the Haskell type check does, so it should just assign a lambda expression of the appropriate type to each word and let Haskell do the rest. The problem is that if s cannot be reached, a Haskell type check naturally stops the program from executing.

Answer 1

Pretty standard stuff. Just write a type checker and evaluate only that term when it is being tested. evalMay does this. You can, of course, enrich a set of constants and basic types; I just used one of them for simplicity.

 import Control.Applicative ((<$), (<$>)) import Control.Monad (guard) import Safe (atMay) data Type = Base | Arrow Type Type deriving (Eq, Ord, Read, Show) data Term = Const | Var Int -- deBruijn indexing; the nearest enclosing lambda binds Var 0 | Lam Type Term | App Term Term deriving (Eq, Ord, Read, Show) check :: [Type] -> Term -> Maybe Type check env Const = return Base check env (Var v) = atMay env v check env (Lam ty tm) = Arrow ty <$> check (ty:env) tm check env (App tm tm') = do Arrow io <- check env tm i' <- check env tm' guard (i == i') return o eval :: Term -> Term eval (App tm tm') = case eval tm of Lam _ body -> eval (subst 0 tm' body) eval v = v subst :: Int -> Term -> Term -> Term subst n tm Const = Const subst n tm (Var m) = case compare mn of LT -> Var m EQ -> tm GT -> Var (m-1) subst n tm (Lam ty body) = Lam ty (subst (n+1) tm body) subst n tm (App tm' tm'') = App (subst n tm tm') (subst n tm tm'') evalMay :: Term -> Maybe Term evalMay tm = eval tm <$ check [] tm 

Answer 2

I would like to extend @Daniel Wagner's excellent answer with a slightly different approach: instead of typechecking returning a valid type (if any), return a typed expression that is then guaranteed, we can evaluate it (since a simple-typed lambda calculus is very normal). The main idea is that check ctx te returns Just (ctx |- e :: t) iff e can be entered in t in some ctx context and then some typed expression ctx |- e :: t , we can evaluate him in some Env ironing the right type.

Implementation

I will use singletones to emulate the type Pi check :: (ctx :: [Type]) -> (a :: Type) -> Term -> Maybe (TTerm ctx a) , which means that we will need to enable each GHC extension and kitchen sink:

 {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-} {-# LANGUAGE TemplateHaskell #-} -- sigh... import Data.Singletons.Prelude import Data.Singletons.TH import Data.Type.Equality 

The first bit is an untyped representation, right from Daniel Wagner's answer:

 data Type = Base | Arrow Type Type deriving (Show, Eq) data Term = Const | Var Int | Lam Type Term | App Term Term deriving Show 

but we will also give semantics for these types, interpreting Base as () and Arrow t1 t2 as t1 -> t2 :

  type family Interp (t :: Type) where Interp Base = () Interp (Arrow t1 t2) = Interp t1 -> Interp t2 

To keep de Bruin's theme, contexts are a list of types, and variables are context indexes. Given the context type environment, we can find the index of the variable to get the value. Please note that lookupVar is a complete function.

 data VarIdx (ts :: [Type]) (a :: Type) where Here :: VarIdx (a ': ts) a There :: VarIdx ts a -> VarIdx (b ': ts) a data Env (ts :: [Type]) where Nil :: Env '[] Cons :: Interp a -> Env ts -> Env (a ': ts) lookupVar :: VarIdx ts a -> Env ts -> Interp a lookupVar Here (Cons x _) = x lookupVar (There v) (Cons _ xs) = lookupVar v xs 

OK, we have all the infrastructure to actually write code. First of all, we define a typed representation of Term together with an evaluator (total!):

 data TTerm (ctx :: [Type]) (a :: Type) where TConst :: TTerm ctx Base TVar :: VarIdx ctx a -> TTerm ctx a TLam :: TTerm (a ': ctx) b -> TTerm ctx (Arrow ab) TApp :: TTerm ctx (Arrow ab) -> TTerm ctx a -> TTerm ctx b eval :: Env ctx -> TTerm ctx a -> Interp a eval env TConst = () eval env (TVar v) = lookupVar v env eval env (TLam lam) = \x -> eval (Cons x env) lam eval env (TApp fe) = eval env f $ eval env e 

So far so good. eval is nice and total because its input can only display typed members of a simply typed lambda calculus. Therefore, part of the work of the appraiser @ Daniel must be done when converting an untyped representation to a printed one.

The main idea of infer is that if type inference succeeds, it returns Just $ TheTerm te , where t is Sing lithuanian witness of type e .

 $(genSingletons [''Type]) $(singDecideInstance ''Type) -- I wish I had sigma types... data SomeTerm (ctx :: [Type]) where TheTerm :: Sing a -> TTerm ctx a -> SomeTerm ctx data SomeVar (ctx :: [Type]) where TheVar :: Sing a -> VarIdx ctx a -> SomeVar ctx -- ... and pi ones as well infer :: Sing ctx -> Term -> Maybe (SomeTerm ctx) infer _ Const = return $ TheTerm SBase TConst infer ts (Var n) = do TheVar tv <- inferVar ts n return $ TheTerm t $ TVar v infer ts (App fe) = do TheTerm t0 e' <- infer ts e TheTerm (SArrow t0' t) f' <- infer ts f Refl <- testEquality t0' t0 return $ TheTerm t $ TApp f' e' infer ts (Lam ty e) = case toSing ty of SomeSing t0 -> do TheTerm te' <- infer (SCons t0 ts) e return $ TheTerm (SArrow t0 t) $ TLam e' inferVar :: Sing ctx -> Int -> Maybe (SomeVar ctx) inferVar (SCons t _) 0 = return $ TheVar t Here inferVar (SCons _ ts) n = do TheVar tv <- inferVar ts (n-1) return $ TheVar t $ There v inferVar _ _ = Nothing 

We hope that the last step is obvious: since we can evaluate only a typed term in a given type (since this gives us the type of its Haskell embedding), we return the infer ence type to the check ING type:

 check :: Sing ctx -> Sing a -> Term -> Maybe (TTerm ctx a) check ctx te = do TheTerm t' e' <- infer ctx e Refl <- testEquality tt' return e' 

Session Example

Let's try our functions in GHCi:

 λ» :set -XStandaloneDeriving -XGADTs λ» deriving instance Show (VarIdx ctx a) λ» deriving instance Show (TTerm ctx a) λ» let id = Lam Base (Var 0) -- \x -> x λ» check SNil (SBase `SArrow` SBase) id Just (TLam (TVar Here)) λ» let const = Lam Base $ Lam Base $ Var 1 -- \xy -> x λ» check SNil (SBase `SArrow` SBase) const Nothing -- Oops, wrong type λ» check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const Just (TLam (TLam (TVar Here))) λ» :t eval Nil <$> check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const eval Nil <$> check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const :: Maybe (() -> () -> ()) -- Note that the `Maybe` there comes from `check`, not `eval`! λ» let Just const' = check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const λ» :t eval Nil const' eval Nil const' :: () -> () -> () λ» eval Nil const' () () ()