3

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

它展示了一个用于System T（一种简单的全功能语言）的小型 OCaml 编译器程序。

整个管道采用 OCaml 语法（通过 Camlp4 元编程）将它们转换为 OCaml AST，然后再转换为 SystemT Lambda Calculus（参见module Term：），最后是 SystemT Combinator Calculus（参见：） module Goedel。最后一步也用 OCaml 元编程Ast.expr类型包装。

我试图在不使用 Template Haskell 的情况下将其翻译成 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 指数相关）。这是因为组合演算没有变量/变量名称。这是通过Elaborate.lookupwhich 使用Quote.find函数来完成的。

问题是我将组合微积分编码为 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'$ >>

进入哈斯克尔：

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

问题源于这样一个事实，即使用和Compose来自GADT会导致类型签名的无限变化。FstSndTHom a b

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

我不确定如何在 Haskell 中解决。我应该使用存在量化的类型，例如

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

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

4

1 回答 1

2

这个答案必须有点高级，因为有三个完全不同的可能设计系列来解决这个问题。你正在做的似乎更接近于接近三，但这些方法是按照复杂性增加的顺序排列的。

原帖中的方法

翻译原帖需要 Template Haskell 和偏心；find将返回一个Q.Exp代表 some 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，您需要（在运行时）检查它们的类型是否匹配。而对于一个简单的存在主义，你不能。因此，您还需要在值级别有类型的表示。

更烦人的存在（像往常一样），因为你不能在你的返回类型中暴露隐藏的类型变量，或者将它们投影出来（不像依赖记录/sigma-types）。老实说，我并不完全确定这最终会奏效。这是 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
于 2018-11-17T23:39:23.007 回答