防止 Haskell 中的类型变量扩散

Question

参数化类型变量很好，但它不能扩展。作为可能发生的事情的一个例子，http://oleg.fi/gists/posts/2017-04-26-indexed-poptics.html 给出了一个包含 9 个类型变量的抽象。我一直在研究一个由编程语言参数化的程序转换框架，并且可以想象将来有几十个或几百个参数。

所以这是基本问题：我有一个数据类型 T，它在 N 个类型上参数化。如何在 T 上编写一个函数，而无需每次使用时都写下 N 个类型变量？

以下是我研究过的一些方法，但都不能令人满意：

参数化类型变量* -> *

data V = Var1 | Var2 | Var3 | Var4

myfunc :: forall (v :: V -> *). Constraints v => v Var1 -> v Var2
myfunc = ...

所以，现在，我不需要参数化超过 4 个类型变量 Var1, Var2, Var3, Var4，而只需参数化一个类型变量 V -> *。

这行得通，只是在这个例子中，myfunc 不能被调用，因为v 不能被推断出来。您需要将其更改为 Proxy v -> v Var1 -> v Var2。然后，每次您想将 myfunc 与差异变量一起使用时，您都需要定义一个单独的 GADT，并使用它自己的样板。像这样的：

data MyV a where
  MyVar1 :: Int -> MyV Var1
  MyVar2 :: String -> MyV Var2
  MyVar3 :: Bool -> MyV Var3
  MyVar4 :: [Int] -> MyV Var4

不用说，这很不令人满意。

这种方法正是compdata library 的多排序部分所采用的方法。那里很好，因为这个样板与您将要编写的正常数据类型完全一致。

参数化类型变量 (*,*,*,...) 或记录类型

{-# LANGUAGE TypeInType #-}
import Data.Kind

type Vars = (*,*,*,*)

myfunc :: forall (v :: Vars). ...
myfunc = ...

这不起作用，因为据我所知，没有办法破坏类型变量 v 类型的 (*,*,*,*) 。我可以创建一个实例(Int, String, Bool, [Int])，但我实际上无法提取组件Int、String等。我能做的最好的就是编写一个类型族：

type family Fst (v :: Vars) where
  Fst '(a,b,c,d) = a
type family Snd ....

myfunc :: forall (v :: Vars). Fst Vars -> Snd Vars

但是，这与之前的解决方案存在相同的问题：它无法推断出v，除非您单独传入Proxy v。我也尝试添加约束type Extensional v = (v ~ '(Fst v, Snd v, Third v, Fourth v))，但没有帮助。

使用存在量化变量

data HasFourTypeVariables a b c d = ....
data IOnlyCareAboutTwo a b = forall c d. IOnlyCareAboutTwo (HasFourTypeVariables a b c d)

这不起作用。这是您尝试使用它时的样子：

update :: IOnlyCareAboutTwo a b -> IOnlyCareAboutTwo a b
update = ...

useUpdate :: HasFourTypeVariables a b c d -> HasFourTypeVariables a b c d
useUpdate x = case update (IOnlyCareAboutTwo x) of
                IOnlyCareAboutTwo y -> y

这不进行类型检查，因为类型检查器不知道update 的输入和输出具有相同的存在见证。

使用背包

背包看起来是迄今为止最好的竞争者。依赖于具有 5 种类型和相关操作/约束的模块签名有点像在每个操作中都有 5 个普遍量化的约束类型变量，除非您不需要将它们写下来。

Backpack 还是相当新的，尚未与 Stack 集成；我还没有任何经验。此外，它似乎是为对整个包而不是更小的功能单元进行参数化而构建的；我的印象是它对这里需要的那种显式实例化的支持很差。

有一长串类型变量，并忍受它

我正在考虑做的解决方案。 :(

---

一些背景

这个问题可能会在我的多语言程序转换工作中出现，扩展https://arxiv.org/pdf/1707.04600.pdf。

在我的系统中，编程语言中的术语具有Term f l 类型，其中f 是一种编程语言的签名（类型为(*->*)->(*->*) -- 参见the CDTs paper 的解释），@987654350 @ 是一种排序。因此，C 中的语句可能具有 Term CSig StmtL 类型，而 Java 表达式可能具有 Term Java ExpL 类型。

到目前为止，这只是两个类型变量。但是，随着我将系统推向更通用化并能够抽象出越来越深的语义属性，类型变量的数量可能会激增。以下是一些示例：

1. 我想在 AST 节点上存储注释。一些，如节点标签及其源源，是每棵树上的好主意，但其他一些，如符号解析，或该子树是否已被修改的标记，在某些树中是可取的，但在其他树中则不是。因此，我希望我的表示能够灵活地在某些表示中添加注释，但不能在其他表示中添加注释，并且能够编写只关心这些注释的子集是否存在的运算符。这个怎么做？注释的一个或多个类型变量，以及许多“HasSymbolResolutionAnnotation a”约束。

2. 经过大量经验和数小时的思考后，我认为可变 AST 实际上是一个不错的主意。然后，我希望能够编写可以在纯 AST 和可变 AST 上工作的运算符。我还没有弄清楚如何最好地做到这一点，但你可以打赌它会为我的类型添加至少一个类型变量。

3. 在CSig 或JavaSig 签名中，可能有许多语言通用节点，例如“添加”。对于许多简单的分析和转换，只需说“这种语言有加法”并坚持一个通用的 Add 节点就足够了。但是对于更复杂的情况，您的语言中的加法是否会溢出，以及 (+) 运算符是原始运算符还是可以像 C++ 或 Haskell 中那样被覆盖，以及它对周围类型施加的约束，这些都可能很重要。现在，您的语言可能有一个 Add MonomorphicAddition NonOverridable OverflowWrapsToNegative 节点，而不是“添加”节点，并且您的符号分析定义了具有 Add a b OverflowWrapsToNegative 节点的语言的传递函数。您可以像这样编码的运算符的变体数量没有限制。对于这种只引用其几个参数的参数化运算符，只要您能说出许多有用的话，就可以这样对待它们。

我希望这有助于解释为什么这是一个问题。

Answer 1

这个答案的灵感来自Trees That Grow 论文。它假定仅存在有限数量的数据类型“变体”，即仅使用 N 个参数的所有可能实例化的一小部分。

{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language FlexibleContexts #-}

我们这样定义数据类型

data MyType (v::Variant) = MyType (Xa v) (Xb v) (Xc v) Int

data Variant = V1 | V2

type family Xa (v::Variant) :: * where
    Xa V1 = Int
    Xa V2 = Bool

type family Xb (v::Variant) :: * where
    Xb V1 = Bool
    Xb V2 = Char

type family Xc (v::Variant) :: * where
    Xc V1 = String
    Xc V2 = Maybe Int

数据类型有两个“变体”。每个变化的字段都有自己的（公认的样板）类型族，它将一个变体映射到该变体中字段的实际类型。

这是一个适用于所有数据类型变体的简单函数：

getInt :: MyType (v :: Variant) -> Int
getInt (MyType _ _ _ i) = i

使用-XConstraintKinds，我们可以定义一个所有字段共享的约束：

{-# language ConstraintKinds #-}
import GHC.Exts (Constraint)
type MyForAll (p :: * -> Constraint) (v::Variant) = (p (Xa v),p (Xb v),p (Xc v))

我们可以用它来定义类似的函数

myShow :: MyForAll Show (v :: Variant) => MyType v -> String
myShow (MyType a b c i) = show a ++ show b ++ show c ++ show i

我们也可以启用-XTypeApplications来指定变体：

λ :t MyType
MyType :: forall {v :: Variant}. Xa v -> Xb v -> Xc v -> Int -> MyType v
λ :set -XTypeApplications
λ :t MyType @V1
MyType @V1 :: Int -> Bool -> String -> Int -> MyType 'V1

Answer 2

如果您想将多个类型变量组合在一起，您可以这样做。 在值级别上，您只需使用一条记录，您也可以在类型级别上这样做。创建一个记录类型，然后它的提升版本可用于对类型进行分组。记录访问有点笨拙，因为值级别记录选择器语法没有提升。

这里有一个例子可以阐明我的意思。

{-# LANGUAGE StandaloneDeriving, TypeInType, UndecidableInstances #-}
module RecordTyVars where
import Data.Kind

-- The normal way, with 3 type variables.
data OExpr sym lit op = OVar sym | OLit lit | OPrimOp op [OExpr sym lit op]
     deriving (Show)

oe :: OExpr String Integer Op
oe = OPrimOp Add [OVar "x", OLit 1]

data Op = Add | Sub
     deriving (Show)

--------

-- Record that when lifted will contain the types.
data ExprTypes = Types Type Type Type

-- Record access functions, since the record syntax doesn't lift.
type family SymType (r :: ExprTypes) :: * where
    SymType ('Types sym lit op) = sym
type family LitType (r :: ExprTypes) :: * where
    LitType ('Types sym lit op) = lit
type family OpType (r :: ExprTypes) :: * where
    OpType  ('Types sym lit op) = op

-- Using the record of types
data Expr r = Var (SymType r) | Lit (LitType r) | PrimOp (OpType r) [Expr r]

-- Must use standalone deriving when thing the going gets tough.
deriving instance (Show (SymType r), Show (LitType r), Show (OpType r)) =>
                  Show (Expr r)

e :: Expr ('Types String Integer Op)
e = PrimOp Add [Var "x", Lit 1]