在Haskell中实现带有失败的简单类型λ演算

Question

我是Haskell的新手，如果这个问题不太合理，请谅解。

我想以这样的方式在Haskell中实现简单类型的lambda表达式，即当我尝试将一个表达式应用于另一个错误类型时，结果不会出现类型错误，而是一些集合值，例如Nothing。起初我认为使用Maybe monad是正确的方法，但我无法让任何东西工作。我想知道是否有正确的方法来解决这个问题。

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

- Reuben

---

你能否提供一个完整的示例来说明你正在尝试做什么？也许是几个单词，一个类型检查的句子和一个不进行类型检查的句子，你想要运行时的失败值而不是编译时的值？如果你想要找出是否“有任何方法将它们组合起来”以达到一种类型，那么你需要寻找某种搜索方式，这超出了Haskell类型检查器目前所做的事情（有一个工具在其名称中带有“genie”，但我现在找不到链接）。 - Cirdec

啊，是的，这个工具叫做djinn。它的相关性在于，给定一小组类型化对象——单元()、元组(,)和函数的lambda构造器，它试图推断出一个具有给定类型的对象。关于从类型中推导Haskell代码的问题，有一个相关的问题。 - Cirdec

我无法准确理解你的目标。特别是，你想要类型检查是在静态（程序运行之前）还是动态（运行时）执行。你关于一个无法访问的s的最后一句话似乎表明你想要动态检查，但你应该澄清这一点。 - chi

Answer 1

我希望能够在@Daniel Wagner的优秀答案基础上提供一种略有不同的方法：与其返回一个有效类型（如果有），不如返回一个已经确定我们可以评估它的类型表达式（因为简单类型的λ演算是强正规化的）。基本思想是，如果e可以在某个上下文ctx中以t的类型进行类型标记，则check ctx t e将返回Just (ctx |- e :: t)，然后给定一些已分类的表达式ctx |- e :: t，我们可以在正确类型的环境中对其进行评估。

实现

我将使用单例来模拟check :: (ctx :: [Type]) -> (a :: Type) -> Term -> Maybe (TTerm ctx a)的Pi类型，这意味着我们需要打开每个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 解释为（），将 Arrow t1 t2 解释为 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，其中t是e类型的一个Singleton证明。

$(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嵌入类型的方法），所以我们将类型推断转换为类型检查：

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' () ()
()

- Cactus

Answer 2

这是非常标准的内容。只需编写一个类型检查器，在它通过类型检查之后再对该术语进行评估。 evalMay 可以实现这一点。当然，您可以增加常量和基本类型的集合；我只是为了简单起见使用了每个类型的一个。

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

- Daniel Wagner

---

有人能澄清一下在 subst n tm (Var m) 情况下发生了什么，特别是当比较为 GT 时吗？在我看来，要么 m = n（所以我们进行替换），要么 m <> n（所以替换没有效果），但结果永远不应该是 Var (m-1)。也许这是在尝试进行一个规范的 de Bruijn "shift" 操作？ - Brian Berns

请注意（除了递归调用之外），subst 仅在评估 lambda 应用于术语时调用。 在这种情况下，我们即将删除该 lambda 的存在，因此删除它绑定的变量的存在。 因此，是的，我们正在进行移位，以便对于此 lambda 外部的任何变量引用（例如，因为我们正在尝试评估开放术语），仍将指向正确的位置。 - Daniel Wagner