System T Combinator 语言的 Haskell 解释器

Question

在上一个问题中SystemT Compiler and dealing with Infinite Types in Haskell我询问如何将 SystemT Lambda Calculus 解析为 SystemT Combinators。我决定使用普通代数数据类型来编码 SystemT Lambda 演算和 SystemT Combinator 演算(基于评论:SystemT Compiler and dealing with Infinite Types in 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，这就是不足为奇。

我认为你可以保持你的synth(粗略地)不变，如果你添加一个简单的传递，将生成的非类型化THom检查到类型化的GADT中，比如说StrongTHom a b。返回存在似乎有风险，最好为其提供传入上下文:

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

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

如果您绝对必须能够推断输入和输出类型，那么我想除了返回存在性之外别无选择。这只是意味着您的类型检查器将包含更多类型相等性检查(参见下面的 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)

(其中 :~: 是 standard type equality )，很容易编写；我只是确保您了解这项技术。

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