8

在上一个问题SystemT Compiler and handling Infinite Types in Haskell 中，我询问了如何将 SystemT Lambda Calculus 解析为 SystemT Combinators。我决定使用纯代数数据类型来编码 SystemT Lambda 演算和 SystemT Combinator 演算（基于评论：SystemT Compiler and processing 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)

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

根据原始博客文章，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树，这样我才能得到某种功能，可以以部分方式执行。

4

2 回答 2

3

要以THom保证类型良好的方式进行解释，您需要向 Haskell 类型检查器“解释”其类型。我看到您已经考虑过 GADT 版本THom，这将是进行此解释的传统方式，而这仍然是我将采用的方法。如果我理解正确，您面临的麻烦是 的逻辑synth太复杂，无法证明它总是会产生一个类型良好的THom，这不足为奇。

我认为你可以保持你的synth（粗略的）原样，如果你添加一个简单的传递，类型检查生成的非类型THom化到类型化的 GADT，比如StrongTHom a b. 返回存在似乎是有风险的，最好为其提供一个传入的上下文：

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应该像热黄油一样通过。祝你好运！

于 2019-01-01T19:55:01.953 回答
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

然后你可以非常直接地使用你的 untyped THom，作为一个合适的解释器 monad Interp（也许只是一个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上面的类型与 的 codomain 相同eval，因为嵌入式函数也可能失败。

于 2019-01-02T02:41:20.073 回答