我是 Haskell 的新手，所以如果这个问题没有太大意义，我深表歉意。

我希望能够在 Haskell 中实现简单类型的 lambda 表达式，这样当我尝试将一个表达式应用于另一个表达式时wrongtype，结果不是类型错误，而是一些设置值，例如没有什么。起初我认为使用 Maybe monad 将是正确的方法，但我无法让任何东西发挥作用。我想知道如果有的话，正确的方法是什么。

如果有帮助的话，问题的背景是我正在从事的一个项目，该项目为句子中的单词分配 POS（词性）标签。对于我的标签集，我使用分类语法类型；这些是类型化的 lambda 表达式，例如(e -> s) or (e -> (e -> s)), where e and s分别是名词和句子的类型。例如，kill有类型(e -> (e -> s))- 它需要两个名词短语并返回一个句子。我想要编写一个函数，该函数接受此类类型的对象列表，并找出是否有任何方法将它们组合起来以达到该类型的对象s。当然，这正是 Haskell 的类型检查器所做的事情，因此为每个单词分配适当类型的 lambda 表达式应该很简单，然后让 Haskell 完成其余的工作。问题是，如果s无法到达，Haskell 的类型检查器自然会停止程序运行。

我想用一种稍微不同的方法来扩展 @Daniel Wagner 的优秀答案：不是返回有效类型（如果有的话）的类型检查，而是返回一个类型化表达式，然后保证我们可以对其进行求值（因为简单类型的 lambda微积分是强标准化的）。基本思想是check ctx t e回报Just (ctx |- e :: t) iff e可以输入t在某些情况下ctx，然后给出一些键入的表达式ctx |- e :: t，我们可以用一些方法来评价它Env正确类型的熨烫。

实施情况

我将使用单例来模拟 Pi 类型check :: (ctx :: [Type]) -> (a :: Type) -> Term -> Maybe (TTerm ctx a)，这意味着我们需要打开每个 GHC 扩展和厨房水槽：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
{-# LANGUAGE TemplateHaskell #-} -- sigh...

import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Type.Equality

第一个位是非类型化表示，直接来自 @Daniel Wagner 的回答：

data Type = Base
          | Arrow Type Type
          deriving (Show, Eq)

data Term = Const
          | Var Int
          | Lam Type Term
          | App Term Term
          deriving Show

但我们还将通过解释来给出这些类型的语义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

为了与 de Bruijn 主题保持一致，上下文是类型列表，变量是上下文的索引。给定上下文类型的环境，我们可以查找变量索引来获取值。注意lookupVar是一个总函数。

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

好的，我们已经准备好所有基础设施来实际编写一些代码。首先，让我们定义一个类型表示Term，与（总计！）评估器一起：

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

到目前为止，一切都很好。eval是很好的和总的，因为它的输入只能表示简单类型 lambda 演算的类型良好的项。因此，@Daniel 评估器的部分工作必须将非类型化表示转换为类型化表示。

背后的基本思想infer如果类型推断成功，则返回Just $ TheTerm t e, where t is a Sing莱顿见证者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

希望最后一步是显而易见的：因为我们只能评估给定类型的类型良好的术语（因为这就是给我们其 Haskell 嵌入的类型），所以我们将类型infer进入类型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'

示例会话

让我们在 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' () ()
()