SystemT编译器和Haskell中的无限类型处理 [英] SystemT Compiler and dealing with Infinite Types in Haskell

问题描述

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

I'm following this blog post: http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html

它显示了用于系统T(一种简单的总功能语言)的小型OCaml编译器程序).

整个管道采用OCaml语法(通过Camlp4元编程)将其转换为OCaml AST，然后将其转换为SystemT Lambda微积分(请参见:module Term)，最后是SystemT组合器微积分(请参见: module Goedel).最后一步还封装了OCaml元编程Ast.expr类型.

The entire pipeline takes OCaml syntax (via Camlp4 metaprogramming) transforms them to OCaml AST that is translated to SystemT Lambda Calculus (see: module Term) and then finally SystemT Combinator Calculus (see: module Goedel). The final step is also wrapped with OCaml metaprogramming Ast.expr type.

我正在尝试不使用模板Haskell将其翻译为Haskell.

I'm attempting to translate it to Haskell without the use of Template Haskell.

对于SystemT Combinator表单，我将其编写为

For the SystemT Combinator form, I've written it as

{-# 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是前向构图，与(.)不同.

Note that Compose is forward composition, which differs from (.).

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

During the translation of SystemT Lambda Calculus to SystemT Combinator Calculus, the Elaborate.synth function tries to convert SystemT Lambda calculus variables into series of composed projection expressions (related to De Brujin Indices). This is because combinator calculus doesn't have variables/variable names. This is done with the Elaborate.lookup which uses the Quote.find function.

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

The problem is that with my encoding of the combinator calculus as the GADT THom a b. Translating the Quote.find function:

  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可能导致类型签名无限变化的事实.

The problem stems from the fact that using Compose and Fst and Snd from the THom a b GADT can result in infinite variations of the type signature.

本文没有这个问题，因为它似乎使用了Ast.expr OCaml东西来包装基础表达式.

The article doesn't have this problem because it appears to use the Ast.expr OCaml thing to wrap the underlying expressions.

我不确定如何在Haskell中解决.我应该使用像这样存在的量化类型吗?

I'm not sure how to resolve in Haskell. Should I be using an existentially quantified type like

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

或某种类型级别的Fix来适应无限类型问题.但是，我不确定这将如何更改find或lookup函数.

Or some sort of type-level Fix to adapt the infinite type problem. However I'm unsure how this changes the find or lookup functions.

推荐答案

此答案必须有点高级，因为存在三种完全不同的家族可能的设计来解决该问题. .您正在做的事情似乎接近于方法三，但是方法的复杂性是按顺序排列的.

This answer will have to be a bit high-level, because there are three entirely different families of possible designs to fix that problem. What you’re doing seems closer to approach three, but the approaches are ordered by increasing complexity.

翻译原始帖子需要模板Haskell和局部性； find将返回表示某些Hom a b的Q.Exp，避免了与原始帖子一样的此问题.就像在原始帖子中一样，在对所有Template Haskell函数的输出进行类型检查时，将捕获原始代码中的类型错误.因此，仍然在运行时 捕获类型错误，但是您仍然需要编写 tests 来查找宏输出错误类型表达式的情况.可以以大大增加复杂性为代价来提供更有力的保证.

Translating the original post requires Template Haskell and partiality; find would return a Q.Exp representing some Hom a b, avoiding this problem just like the original post. Just like in the original post, a type error in the original code would be caught when typechecking the output of all the Template Haskell functions. So, type errors are still caught before runtime, but you will still need to write tests to find cases where your macros output ill-typed expressions. One can give stronger guarantees, at the cost of a significant increase in complexity.

如果您希望与该文章有所不同，一种选择是在整个文章中使用依赖类型"，并使 input 成为依赖类型.我宽松地使用该术语来包括实际的依赖类型的语言，实际的依赖Haskell(当其着陆时)以及当今在Haskell中伪造依赖类型的方法(通过GADT，单例以及其他方法). 但是，您将失去编写自己的类型检查器并选择要使用的类型系统的能力.通常，您最终会嵌入一个简单类型的lambda演算，并且可以通过可生成给定类型项的多态Haskell函数来模拟多态.在依赖类型的语言中，这更容易，但是在Haskell中完全可以实现.

If you want to diverge from the post, one alternative is to use "dependent typing" throughout and make the input dependently-typed. I use the term loosely to include both actually dependently-typed languages, actual Dependent Haskell (when it lands), and ways to fake dependent typing in Haskell today (via GADTs, singletons, and what not). However, you lose the ability to write your own typechecker and choose which type system to use; typically, you end up embedding a simply-typed lambda calculus, and can simulate polymorphism via polymorphic Haskell functions that can generate terms at a given type. This is easier in dependently-typed languages, but possible at all in Haskell.

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

But honestly, in this road it’s easier to use higher-order abstract syntax and Haskell functions, with something like:

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编译器可见，而对您的类型或术语不可见.

If you can use this approach (details omitted here), you get high assurance from GADTs with limited complexity. However, this approach is too inflexible for many scenarios, for instance because the typing contexts are only visible to the Haskell compiler and not in your types or terms.

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

A third option is go dependently-typed and to still make your program turn weakly-typed input to strongly typed output. In this case, your typechecker overall transforms terms of some type Expr into terms of a GADT TExp gamma t, Hom a b, or such. Since you don’t know statically what gamma and t (or a and b) are, you’ll indeed need some sort of existential.

但是简单的存在性太弱了:要构建更大的类型正确的表达式，您需要检查所产生的类型是否允许它.例如，要构建包含两个较小的TExpr中的Compose表达式的TExpr，您需要(在运行时)检查它们的类型是否匹配.有了简单的存在性，您就不能做到.因此，您还需要在值级别上具有类型的表示形式.

But a plain existential is too weak: to build bigger well-typed expression, you’ll need to check that the produced types allow it. For instance, to build a TExpr containing a Compose expression out of two smaller TExpr, you'll need to check (at runtime) that their types match. And with a plain existential, you can't. So you’ll need to have a representation of types also at the value level.

还有什么要处理的烦人的事情(像往常一样)，因为您永远无法在返回类型中公开隐藏的类型变量，也无法将其投影(与从属记录/sigma类型不同). 老实说，我并不完全确定这最终能否奏效.这是Haskell中可能的局部草图，其中最多是find的情况.

What's more existentials are annoying to deal with (as usual), since you can’t ever expose the hidden type variables in your return type, or project those out (unlike dependent records/sigma-types). I am honestly not entirely sure this could eventually be made to work. Here is a possible partial sketch in Haskell, up to one case of 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

这篇关于SystemT编译器和Haskell中的无限类型处理的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！