用于System T组合器语言的Haskell解释器

Question

在之前的一个问题SystemT编译器和Haskell中处理无限类型中，我询问了如何将SystemT Lambda微积分解析为SystemT Combinators。我决定使用普通代数数据类型来编码SystemT Lambda演算和SystemT Combinator演算(基于注释：SystemT编译器和在Haskell中处理无限类型)。

SystemTCombinator.hs:

module SystemTCombinator where
data THom = Id
| Unit
| Zero
| Succ
| Compose THom THom
| Pair THom THom
| Fst
| Snd
| Curry THom
| Eval
| Iter THom THom
deriving (Show)

SystemTLambda.hs:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE TypeSynonymInstances      #-}
module SystemTLambda where
import           Control.Monad.Catch
import           Data.Either (fromRight)
import qualified SystemTCombinator    as SystemTC
type TVar = String
data TType = One | Prod TType TType | Arrow TType TType | Nat deriving (Eq)
instance Show TType where
show ttype = case ttype of
One -> "'Unit"
Nat -> "'Nat"
Prod ttype1 ttype2 ->
"(" ++ show ttype1 ++ " * " ++ show ttype2 ++ ")"
Arrow ttype1@(Arrow _ _) ttype2 ->
"(" ++ show ttype1 ++ ") -> " ++ show ttype2
Arrow ttype1 ttype2 -> show ttype1 ++ " -> " ++ show ttype2
data TTerm = Var TVar
| Let TVar TTerm TTerm
| Lam TVar TTerm
| App TTerm TTerm
| Unit
| Pair TTerm TTerm
| Fst TTerm
| Snd TTerm
| Zero
| Succ TTerm
| Iter TTerm TTerm TVar TTerm
| Annot TTerm TType
deriving (Show)
-- a context is a list of hypotheses/judgements
type TContext = [(TVar, TType)]
-- our exceptions for SystemT
data TException = TypeCheckException String
| BindingException String
deriving (Show)
instance Exception TException
newtype Parser a = Parser { run :: TContext -> Either SomeException a }
instance Functor Parser where
fmap f xs = Parser $ ctx ->
either Left (v -> Right $ f v) $ run xs ctx
instance Applicative Parser where
pure a = Parser $ ctx -> Right a
fs <*> xs = Parser $ ctx ->
either Left (f -> fmap f $ run xs ctx) (run fs ctx)
instance Monad Parser where
xs >>= f = Parser $ ctx ->
either Left (v -> run (f v) ctx) $ run xs ctx
instance MonadThrow Parser where
throwM e = Parser (const $ Left $ toException e)
instance MonadCatch Parser where
catch p f = Parser $ ctx ->
either
(e -> case fromException e of
Just e' -> run (f e') ctx -- this handles the exception
Nothing -> Left e) -- this propagates it upwards
Right
$ run p ctx
withHypothesis :: (TVar, TType) -> Parser a -> Parser a
withHypothesis hyp cmd = Parser $ ctx -> run cmd (hyp : ctx)
tvarToHom :: TVar -> Parser (SystemTC.THom, TType)
tvarToHom var = Parser $ ctx ->
case foldr transform Nothing ctx of
Just x -> Right x
Nothing -> throwM $ BindingException ("unbound variable " ++ show var)
where
transform (var', varType) homAndType =
if var == var'
then Just (SystemTC.Snd, varType)
else homAndType >>= ((varHom, varType) -> Just (SystemTC.Compose SystemTC.Fst varHom, varType))
check :: TTerm -> TType -> Parser SystemTC.THom
-- check a lambda
check (Lam var bodyTerm) (Arrow varType bodyType) =
withHypothesis (var, varType) $
check bodyTerm bodyType >>= (bodyHom -> return $ SystemTC.Curry bodyHom)
check (Lam _    _    ) ttype                 = throwM
$ TypeCheckException ("expected function type, got '" ++ show ttype ++ "'")
-- check unit
check Unit One = return SystemTC.Unit
check Unit ttype =
throwM $ TypeCheckException ("expected unit type, got '" ++ show ttype ++ "'")
-- check products
check (Pair term1 term2) (Prod ttype1 ttype2) = do
hom1 <- check term1 ttype1
hom2 <- check term2 ttype2
return $ SystemTC.Pair hom1 hom2
check (Pair _      _     ) ttype                = throwM
$ TypeCheckException ("expected product type, got '" ++ show ttype ++ "'")
-- check primitive recursion
check (Iter baseTerm inductTerm tvar numTerm) ttype = do
baseHom   <- check baseTerm ttype
inductHom <- withHypothesis (tvar, ttype) (check inductTerm ttype)
numHom    <- check numTerm Nat
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id numHom)
(SystemTC.Iter baseHom inductHom)
-- check let bindings
check (Let var valueTerm exprTerm) exprType = do
(valueHom, valueType) <- synth valueTerm
exprHom <- withHypothesis (var, valueType) (check exprTerm exprType)
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom
check tterm ttype = do
(thom, ttype') <- synth tterm
if ttype == ttype'
then return thom
else throwM $ TypeCheckException
(  "expected type '"
++ show ttype
++ "', inferred type '"
++ show ttype'
++ "'"
)
synth :: TTerm -> Parser (SystemTC.THom, TType)
synth (Var tvar) = tvarToHom tvar
synth (Let var valueTerm exprTerm) = do
(valueHom, valueType) <- synth valueTerm
(exprHom, exprType) <- withHypothesis (var, valueType) (synth exprTerm)
return (SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom, exprType)
synth (App functionTerm valueTerm) = do
(functionHom, functionType) <- synth functionTerm
case functionType of
Arrow headType bodyType -> do
valueHom <- check valueTerm headType
return (SystemTC.Compose (SystemTC.Pair functionHom valueHom) SystemTC.Eval, bodyType)
_ -> throwM $ TypeCheckException ("expected function, got '" ++ show functionType ++ "'")
synth (Fst pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Fst, fstType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth (Snd pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Snd, sndType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth Zero = return (SystemTC.Compose SystemTC.Unit SystemTC.Zero, Nat)
synth (Succ numTerm) = do
numHom <- check numTerm Nat
return (SystemTC.Compose numHom SystemTC.Succ, Nat)
synth (Annot term ttype) = do
hom <- check term ttype
return (hom, ttype)
synth _ = throwM $ TypeCheckException "unknown synthesis"

我使用上面的双向类型检查器将SystemTLambda.TTerm解析为SystemTCombinator.THom。

systemTLambda :: TTerm
systemTLambda =
Let "sum"
(Annot
(Lam "x" $ Lam "y" $
Iter (Var "y") (Succ $ Var "n") "n" (Var "x"))
(Arrow Nat $ Arrow Nat Nat))
(App
(App
(Var "sum")
(Succ $ Succ Zero))
(Succ $ Succ $ Succ Zero))
systemTCombinator :: Either SomeException (SystemTC.THom, SystemTC.TType)
systemTCombinator = fromRight Unit $ run (synth result) []

组合子表达式为：

Compose (Pair Id (Curry (Curry (Compose (Pair Id (Compose Fst Snd)) (Iter Snd (Compose Snd Succ)))))) (Compose (Pair (Compose (Pair Snd (Compose (Compose (Compose Unit Zero) Succ) Succ)) Eval) (Compose (Compose (Compose (Compose Unit Zero) Succ) Succ) Succ)) Eval)

我现在的问题是如何解释这个组合子表达式。我知道所有的组合子表达式都应该被解释为一个函数。问题是，我不知道这个函数的输入和输出类型，我希望"解释器"函数是部分的，因为如果它试图错误地解释某个东西，它应该会导致RuntimeException，因为组合子表达式是非类型的，可能会有坏的组合子表达式。然而，我的类型检查器应该确保一旦到达解释器，组合子应该已经是好类型的了。

根据最初的博客文章，http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html组合子具有所有的等价函数。类似于：

evaluate Id = id
evaluate Unit = const ()
evaluate Zero = () -> Z
evaluate (Succ n) = S n
evaluate (Compose f g) = (evaluate g) . (evaluate f)
evaluate (Pair l r) = (evaluate l, evaluate r)
evaluate Fst = fst
evaluate Snd = snd
evaluate (Curry h) = curry (evaluate h)
evaluate Eval = (f, v) -> f v
evaluate (Iter base recurse) = (a, n) ->
case n of
Z   -> evaluate base a
S n -> evaluate recurse (a, evaluate (Iter base recurse) (a, n))

但显然这是行不通的。似乎必须有某种方法来解释THom树，这样我就可以得到某种可以部分执行的函数。

Answer 1

要以保证良好类型的方式解释THom，您需要向Haskell类型检查器"解释"其类型。我知道您已经考虑过THom的GADT版本，这将是进行此解释的传统方法，并且这仍然是我将采用的方法。如果我理解正确的话，你面临的问题是synth的逻辑太复杂，无法证明它总是会产生一个好类型的THom，这并不奇怪。

我认为，如果您添加一个简单的过程，将生成的未类型化的THom类型检查到类型化的GADT中，比如StrongTHom a b，您可以保持synth(rougly)原样。回归存在主义似乎有风险，最好为其提供一个传入的上下文：

checkTHom :: THom -> TType a -> TType b -> Maybe (StrongTHom a b)

(其中TType是上一个答案中的单例形式)。它只需要你在顶层知道你的输入和输出类型是什么。这通常很好，因为为了实际使用结果，你最终必须知道它实例化的类型。(您可能需要将此预期类型信息向外推几级，直到知道具体类型为止)

如果你绝对必须能够推断输入和输出类型，那么我想别无选择，只能返回一个存在主义。这只是意味着您的类型检查器将包括更多的类型相等检查(参见下面的typeEq)，而非类型化的THom可能还需要包括更多类型信息。

在任何一种情况下，THom都必须包含它所擦除的任何类型。例如，在Compose :: THom a b -> THom b c -> THom a c中，b被擦除，checkTHom将不得不重建它。因此，Compose需要包括足够的信息，以便这是可能的。在这一点上，存在主义(上一个答案中的SomeType)可能会很好，因为使用它的唯一方法是打开它并递归传递。

要写这个检查器，我有一种感觉，你需要一个强大的平等检查：

typeEq :: TType a -> TType b -> Maybe (a :~: b)

(其中:~:是标准类型相等)，其易于写入；我只是想让你知道这个技巧。

一旦你有了这个，那么eval :: StrongTHom a b -> a -> b应该会像热黄油一样通过。祝你好运

Answer 2

或者，通过声明所有可能值的类型来进行运行时类型检查非常容易。

data Value
= VUnit                          -- of type One
| VPair Value Value              -- of type Pair
| VFunc (Value -> Interp Value)  -- of type Func
| VNat Integer                   -- of type Nat

然后，您可以非常直接地使用未键入的THom作为适当的解释器monadInterp(可能只是一个Exceptmonad)：

eval :: THom -> Value -> Interp Value
eval Id v  = v
eval Unit _ = VUnit
eval Zero VUnit = VNat Zero
eval Succ (VNat n) = VNat (n + 1)
...
eval _ _ = throwE "type error"

还要注意，上面的VFunc与eval的共域具有相同的类型，因为嵌入函数也可能失败。