Simply typed lambda calculus with failure, in Haskell

Question

I'm a newcomer to Haskell, so apologies if this question doesn't make too much sense.

I want to be able to implement simply typed lambda expressions in Haskell in such a way that when I try to apply an expression to another of the wrong type, the result is not a type error, but rather some set value, e.g. Nothing. At first I thought using the Maybe monad would be the right approach, but I've not been able to get anything working. I wondered what, if any, would be the correct way to do this.

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

Variform

Can you include a complete example of what you are trying to do? Perhaps a few words, a sentence that type checks, and a sentence that doesn't type check that you'd like a runtime value for the failure instead of a compile time one? If you want to find out if "there is any way to combine them" to reach a type, you are looking for some sort of search which is more than what Haskell's type checker currently does (there's a tool that does that with "genie" in its name, but I can't find a link for it right now). – Castrato

Ahh yes, the tool is djinn. It's related in that, given a small set of typed objects - unit (), tuples (,), and the lambda constructor for functions, it tries to deduce an object with a given type. There's a related question about deducing Haskell code from types. – Castrato

I can't precisely understand your goal. In particular, whether you want type checking to be performed statically (before running your program) or dynamically (at run time). Your last statement about an unreachable s seems to indicate you want dynamic checking, but you should clarify that. – Waddle

Answer 1

Pretty standard stuff. Just write a type-checker, and only evaluate the term when it typechecks. evalMay does this. You can of course enrich the set of constants and base types; I just used one of each 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 i o <- 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 m n 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

Thecla

Can anyone clarify what's going on in the subst n tm (Var m) case, particularly, when the comparison is GT? It seems to me that either m = n (so we make the substitution) or m <> n (so the substitution has no effect), but the result should never be Var (m-1). Maybe this is trying to do a canonical de Bruijn "shift" operation? – Housecarl

@brianberns Note that (other than recursive calls) subst is only called when evaluating the application of a lambda to a term. In that case, we are about to erase the existence of that lambda, hence erase the existence of the variable it binds. So, yes, we are shifting, so that any references to variables outside this lambda (say, because we are trying to evaluate an open term) will still point to the right place. – Thecla

Answer 2

I'd like to extend @Daniel Wagner's excellent answer with a slightly different approach: instead of typechecking returning a valid type (if there is one), return a typed expression that is then guaranteed we can evaluate it (since the simply-typed lambda calculus is strongly normalizing). The basic idea is that check ctx t e returns Just (ctx |- e :: t) iff e can be typed at t in some context ctx, and then given some typed expression ctx |- e :: t, we can evaluate it in some Environment of the right type.

The implementation

I will be using singletons to emulate the Pi type of check :: (ctx :: [Type]) -> (a :: Type) -> Term -> Maybe (TTerm ctx a), which means we will need to turn on every GHC extension and the 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 the untyped representation, straight 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 by 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 with the de Bruijn theme, contexts are the list of types, and variables are indices of the context. Given an environment of a context type, we can look up a variable index to get a value. Note that lookupVar is a total 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 in place to actually write some code. First of all, let's define a typed representation of Term, together with a (total!) evaluator:

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 a b)
    TApp :: TTerm ctx (Arrow a b) -> 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 f e) = eval env f $ eval env e

So far so good. eval is nice & total because its input can only represent well-typed terms of the simply-typed lambda calculus. So part of the work from @Daniel's evaluator will have to be done in the transformation of the untyped representation to the typed one.

The basic idea behind infer is that if type inference succeeds, it returns Just $ TheTerm t e, where t is a Singleton witness of e's type.

$(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 t v <- inferVar ts n
    return $ TheTerm t $ TVar v
infer ts (App f e) = 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 t e' <- 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 t v <- inferVar ts (n-1)
    return $ TheVar t $ There v
inferVar _ _ = Nothing

Hopefully the last step is obvious: since we can only evaluate a well-typed term at a given type (since that's what gives us the type of its Haskell embedding), we turn type inference into type checking:

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

Example session

Let's try our functions out 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 -- \x y -> 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' () ()
()

Templin