在Haskell中简单键入失败的Lambda演算 [英] Simply typed lambda calculus with failure, in Haskell

问题描述

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

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

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

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.

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

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.

推荐答案

相当标准的东西.只需编写一个类型检查器，并且仅在对其进行类型检查时对其进行评估. evalMay执行此操作.您当然可以丰富常量和基本类型的集合.为了简单起见，我只使用了其中之一.

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

这篇关于在Haskell中简单键入失败的Lambda演算的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！