在 Haskell 中生成 Haskell 类型的工具（“二阶 Haskell”）？

Question

如果这个问题有点含糊，请提前道歉。这是周末做白日梦的结果。

借助 Haskell 出色的类型系统，将数学（尤其是代数）结构表达为类型类是非常令人愉快的。我的意思是，看看 数字前奏曲！但在实践中利用如此美妙的类型结构对我来说总是很困难。

你有一种很好的类型系统方式来表达这一点 v1 和 v2 是向量空间的元素 V 然后 w 是向量空间的一个元素 W. 。类型系统允许您编写程序添加 v1 和 v2, ， 但不是 v1 和 w. 。伟大的！但在实践中，您可能想要使用潜在的数百个向量空间，并且您当然不想创建类型 V1, V2, ..., V100 并声明它们是向量空间类型类的实例！或者也许您从现实世界中读取了一些数据，从而产生了符号 a, b 和 c - 您可能想要表达这些符号上的自由向量空间确实是一个向量空间！

所以你被困住了，对吧？为了在科学计算环境中完成您想要使用向量空间做的许多事情，您必须通过放弃向量空间类型类并让函数进行运行时兼容性检查来放弃类型系统。你必须这样做吗？难道不应该利用 Haskell 纯函数式的事实来编写一个程序来生成您需要的所有类型并将它们插入到实际程序中吗？存在这样的技术吗？无论如何，请指出我是否只是忽略了这里的一些基本内容（我可能是）:-)

编辑： 我现在才发现 基金. 。我必须考虑一下它们与我的问题有何关系（对此有启发性的评论表示赞赏）。

Answer 1

哈斯克尔模板 允许这样做。这 维基页面 有一些有用的链接；特别 布拉特的 教程.

顶级声明语法就是您想要的语法。通过输入：

mkFoo = [d| data Foo = Foo Int |]

您生成一个 Template Haskell 拼接（如编译时函数），它将创建一个声明 data Foo = Foo Int 只需插入一行 $(mkFoo).

虽然这个小示例不太有用，但您可以向 mkFoo 提供一个参数来控制所需的不同声明数量。现在一个 $(mkFoo 100) 将为您生成 100 个新数据声明。您还可以使用 TH 生成类型类实例。我的 自适应元组 package 是一个非常小的项目，它使用 Template Haskell 来做类似的事情。

另一种方法是使用 派生, ，它将自动派生类型类实例。如果您只需要实例，这可能会更简单。

Answer 2

Haskell 中还有一些简单的类型级编程技术。一个典型的例子如下：

-- A family of types for the natural numbers
data Zero
data Succ n

-- A family of vectors parameterized over the naturals (using GADTs extension)
data Vector :: * -> * -> * where
    -- empty is a vector with length zero
    Empty :: Vector Zero a
    -- given a vector of length n and an a, produce a vector of length n+1
    Cons  :: a -> Vector n a -> Vector (Succ n) a

-- A type-level adder for natural numbers (using TypeFamilies extension)
type family Plus n m :: *
type instance Plus Zero n = n
type instance Plus (Succ m) n = Succ (Plus m n)

-- Typesafe concatenation of vectors:
concatV :: Vector n a -> Vector m a -> Vector (Plus n m) a
concatV Empty ys = ys
concatV (Cons x xs) ys = Cons x (concatV xs ys)

花点时间考虑一下。我认为它的功效非常神奇。

然而，Haskell 中的类型级编程正处于功能恐怖谷——足以引起人们对你不能做的事情的关注。依赖类型语言，例如 阿格达, 柯克, ， 和 警句 将这种风格发挥到极致并发挥出全部力量。

Template Haskell 更像是通常的 LISP 宏代码生成风格。您编写一些代码来编写一些代码，然后您说“好吧，在此处插入生成的代码”。与上述技术不同，您可以通过这种方式编写任何可计算指定的代码，但您无法获得非常通用的类型检查，如 concatV 多于。

所以你有几个选择来做你想做的事。我认为元编程是一个非常有趣的领域，而且在某些方面仍然很年轻。享受探索的乐趣。:-)