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.

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