在Haskell中生成Haskell类型的设备（“second order Haskell”）？

Question

如果这个问题有点模糊，请事先道歉。这是一些周末白日梦的结果。

使用Haskell的精彩类型系统，将数学（特别是代数）结构表示为类型类是令人高兴的。我的意思是，只要看看numeric-prelude！但是，在实践中利用这种美妙的类型结构对我来说似乎总是很困难。

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

所以你卡住了吧？为了在科学计算设置中执行很多你想要处理矢量空间的事情，你必须放弃你的类型系统，方法是先向量空间类型类别，然后让函数执行运行时兼容性检查。你应该吗？难道不可能使用Haskell纯粹的功能来编写一个程序来生成所需的所有类型，并将它们插入到真正的程序中吗？这种技术是否存在？通过一切手段指出，如果我只是在这里忽略一些基本的东西（我可能是）:-)

编辑：刚才我发现fundeps。我将不得不考虑他们与我的问题有何关系（有关这方面的启发性评论，我们将不胜感激）。

Answer 1

Template Haskell允许这个。 wiki page有一些有用的链接;特别是Bulat'stutorials。

顶层声明语法是你想要的。通过键入：

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

你生成一个模板哈斯克尔拼接（如编译时的功能），将刚刚通过插入线$(mkFoo)创建data Foo = Foo Int声明。

虽然这个小例子不是太有用，但您可以提供一个参数给mkFoo来控制您想要的多少个不同的声明。现在，$(mkFoo 100)将为您生成100个新的数据声明。您也可以使用TH来生成类型类实例。我的adaptive-tuple包是一个非常小的项目，它使用Template Haskell来做类似的事情。

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

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中的类型级编程是在feature-uncanny-valley中 - 仅仅足以让人们注意到你不能做多少事情。诸如Agda，Coq和Epigram这样的依赖型语言将这种风格设置为极限和全功能。

模板Haskell更像通常的LISP宏代码生成风格。你写一些代码来编写一些代码，然后你说“OK在这里插入生成的代码”。与上述技术不同的是，您可以用这种方式编写任何可计算的指定代码，但是您没有像上面的concatV中看到的那样进行非常普遍的类型检查。

所以你有几个选择去做你想做的。我认为元编程是一个非常有趣的领域，在某些方面还很年轻。玩得开心。 :-)