简单地在Haskell中输入失败的lambda演算

Question

我是Haskell的新手,如果这个问题没有多大意义,那么道歉.

我希望能够在Haskell中实现简单的类型化lambda表达式,当我尝试将表达式应用于另一个错误类型时,结果不是类型错误,而是一些设置值,例如Nothing.起初我以为使用Maybe monad会是正确的方法,但我无法得到任何工作.我想知道如果有的话,这是正确的方法.

问题的上下文,如果它有帮助,是我正在研究的项目,它将POS(词性)标签分配给句子中的单词.对于我的标签集,我使用的是分类语法类型; 这些是类型的lambda表达式,如(e -> s)or (e -> (e -> s)),where e和where s分别是名词和句子的类型.例如,kill有类型(e -> (e -> s))- 它需要两个名词短语并返回一个句子.我想写一个函数,它接受这些类型的对象列表,并找出是否有任何方法将它们组合以到达类型的对象s.当然,这正是Haskell的类型检查器所做的事情,因此为每个单词分配适当类型的lambda表达式应该很简单,让Haskell完成剩下的工作.问题是,如果s 无法达到,Haskell的类型检查器自然地阻止程序运行.

Answer 1

很标准的东西。只需编写一个类型检查器，并仅在类型检查时评估该术语。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

Answer 2

我想用稍微不同的方法扩展@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

但我们也会通过解释Baseas ()和Arrow t1 t2as 来为这些类型提供语义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是Singleton见证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 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转换为类型check:

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