haskell - SystemT 编译器和处理 Haskell 中的无限类型

Question

我正在关注这篇博文:http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html

它显示了 System T (a simple total functional language) 的一个小型 OCaml 编译器程序.

整个管道采用 OCaml 语法(通过 Camlp4 元编程)将它们转换为 OCaml AST，然后再转换为 SystemT Lambda Calculus(请参阅:模块术语)，最后是 SystemT Combinator Calculus(请参阅: 模块 Goedel)。最后一步还包含 OCaml 元编程 Ast.expr 类型。

我正在尝试将其转换为 Haskell，而不使用 Template Haskell。

对于 SystemT Combinator 形式，我将其写为

{-# LANGUAGE GADTs #-}

data TNat = Zero | Succ TNat

data THom a b where
  Id :: THom a a
  Unit :: THom a ()
  ZeroH :: THom () TNat
  SuccH :: THom TNat TNat
  Compose :: THom a b -> THom b c -> THom a c
  Pair :: THom a b -> THom a c -> THom a (b, c)
  Fst :: THom (a, b) a
  Snd :: THom (a, b) b
  Curry :: THom (a, b) c -> THom a (b -> c)
  Eval :: THom ((a -> b), a) b -- (A = B) * A -> B
  Iter :: THom a b -> THom (a, b) b -> THom (a, TNat) b

请注意，Compose 是正向组合，与 (.) 不同。

在将 SystemT Lambda Calculus 转换为 SystemT Combinator Calculus 的过程中，Elaborate.synth 函数尝试将 SystemT Lambda 演算变量转换为一系列组合投影表达式(与 De Brujin 指数相关)。这是因为组合器微积分没有变量/变量名称。这是通过使用 Quote.find 函数的 Elaborate.lookup 完成的。

问题在于我将组合器演算编码为 GADT THom a b。翻译 Quote.find 函数:

  let rec find x  = function
    | [] -> raise Not_found
    | (x', t) :: ctx' when x = x' -> <:expr< Goedel.snd >> 
    | (x', t) :: ctx' -> <:expr< Goedel.compose Goedel.fst $find x ctx'$ >>

进入 Haskell:

find :: TVar -> Context -> _
find tvar [] = error "Not Found"
find tvar ((tvar', ttype):ctx)
  | tvar == tvar' = Snd
  | otherwise     = Compose Fst (find tvar ctx)

导致无限类型错误。

• Occurs check: cannot construct the infinite type: a ~ (a, c)
  Expected type: THom (a, c) c
    Actual type: THom ((a, c), c) c

问题源于以下事实:使用 THom a b GADT 中的 Compose 和 Fst 和 Snd 可以导致类型签名的无限变化。

这篇文章没有这个问题，因为它似乎使用 Ast.expr OCaml 东西来包装底层表达式。

我不知道如何在 Haskell 中解决。我应该使用像这样的存在量化类型

data TExpr = forall a b. TExpr (THom a b)

或者某种类型级别的Fix来适应无限类型问题。但是我不确定这如何改变 find 或 lookup 功能。

Answer 1

这个答案必须有点高层次，因为存在三个完全不同的可能设计家族来解决这个问题。您正在做的事情似乎更接近方法三，但这些方法是按复杂性增加排序的。

原帖中的方法

翻译原帖需要 Template Haskell 和偏爱； find 将返回一个 Q.Exp 表示一些 Hom a b，就像原始帖子一样避免了这个问题。就像在原来的帖子中一样，在对所有 Template Haskell 函数的输出进行类型检查时，会捕获原始代码中的类型错误。因此，类型错误仍然会在运行时之前被捕获，但是您仍然需要编写测试来查找宏输出错误类型表达式的情况。人们可以提供更有力的保证，但代价是复杂性显着增加。

输入和输出中的依赖类型/GADT

如果您想偏离本文，一种替代方法是在全文中使用“依赖类型”并使输入依赖类型。我松散地使用这个术语来包括实际的依赖类型语言、实际的依赖 Haskell(当它落地时)以及今天在 Haskell 中伪造依赖类型的方法(通过 GADT、单例等等)。 但是，您将失去编写自己的类型检查器并选择要使用的类型系统的能力；通常，您最终会嵌入一个简单类型的 lambda 演算，并且可以通过可以生成给定类型的项的多态 Haskell 函数来模拟多态性。这在依赖类型语言中更容易，但在 Haskell 中完全可能。

但老实说，在这条路上使用高阶抽象语法和 Haskell 函数会更容易，例如:

data Exp a where
  Abs :: (Exp a -> Exp b) -> Exp (a -> b)
  App :: Exp (a -> b) -> Exp a -> Exp b
  Var :: String -> Exp a —- only use for free variables
exampleId :: Exp (a -> a)
exampleId = Abs (\x -> x)

如果您可以使用这种方法(此处省略详细信息)，您可以从复杂度有限的 GADT 中获得高度保证。然而，这种方法对于许多场景来说太不灵活，例如，因为类型上下文仅对 Haskell 编译器可见，而不是在您的类型或术语中可见。

从无类型术语到有类型术语

第三个选项是依赖类型和，仍然使您的程序将弱类型输入转换为强类型输出。在这种情况下，您的类型检查器总体上会将某种类型 Expr 的术语转换为 GADT TExp gamma t、Hom a b 等术语。由于您静态地不知道 gamma 和 t(或 a 和 b)是什么，您将确实需要某种存在主义。

但是简单的存在主义太弱了:要构建更大的类型良好的表达式，您需要检查生成的类型是否允许它。例如，要构建一个包含两个较小的 TExpr 的 Compose 表达式的 TExpr，您需要(在运行时)检查它们的类型匹配。对于简单的存在主义来说，你做不到。因此，您还需要在值级别上有类型的表示。

更重要的是，存在性处理起来很烦人(像往常一样)，因为您无法公开返回类型中的隐藏类型变量，或将它们投影出来(与依赖记录/西格玛类型不同)。 老实说，我并不完全确定这最终能否发挥作用。这是 Haskell 中可能的部分草图，最多为 find 的一种情况。

data Type t where
  VNat :: Type Nat
  VString :: Type String
  VArrow :: Type a -> Type b -> Type (a -> b)
  VPair :: Type a -> Type b -> Type (a, b) 
  VUnit :: Type ()
data SomeType = forall t. SomeType (Type t)
data SomeHom = forall a b. SomeHom (Type a) (Type b) (THom a b)

type Context = [(TVar, SomeType)] 
getType :: Context -> SomeType
getType [] = SomeType VUnit 
getType ((_, SomeType ttyp) :: gamma) =  
   case getType gamma of
       SomeType ctxT -> SomeType (VPair ttyp
find :: TVar -> Context -> SomeHom 
find tvar ((tvar’, ttyp) :: gamma)
   | tvar == tvar’ =
       case (ttyp, getType gamma) of
         (SomeType t, SomeType ctxT) ->
          SomeHom (VPair t ctxT) t Fst