在Haskell中生成Haskell类型的设施("二阶Haskell")？

Question

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

使用Haskell的精彩类型系统,将数学(特别是代数)结构表达为类型类很令人高兴.我的意思是,只看看数字前奏!但是在实践中利用这种奇妙的类型结构对我来说似乎总是很困难.

你有表达的是一个很好的,类型系统的方式v1和v2是向量空间的元素V,并且w是一个向量空间的元素W.该型系统让你写一个程序追加v1和v2,但不v1和w.大!但在实践中你可能要与几百个潜在向量空间的发挥,你肯定不希望创建类型V1,V2......,V100并宣布他们的向量空间类型类的实例!或者你可能从现实世界中读取一些产生符号的数据a,b并且c- 你可能想表达这些符号上的自由向量空间确实是一个向量空间!

所以你被卡住了吧？为了完成您在科学计算设置中对向量空间做的许多事情,您必须通过前面的向量空间类型类来放弃您的类型系统,并且让函数执行运行时兼容性检查.你应该吗？是不是可以使用Haskell纯粹功能的事实来编写一个程序,生成所需的所有类型并将它们插入到真正的程序中？这种技术存在吗？无论如何,请指出我是否只是忽略了一些基本的东西(我可能是):-)

编辑:刚才我发现了fundeps.我将不得不考虑一下他们与我的问题的关系(对此有启发性的评论表示赞赏).

Answer 1

模板Haskell允许这样做.该wiki页面有一些有用的链接; 特别是Bulat的 教程.

顶级声明语法是您想要的语法.输入:

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

你生成一个模板Haskell拼接(就像一个编译时函数),它将data Foo = Foo Int通过插入行创建一个声明$(mkFoo).

虽然这个小例子不太有用,但你可以为mkFoo提供一个参数来控制你想要多少个不同的声明.现在a $(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中的类型级编程处于特征 - 不可思议的山谷中 - 足以引起人们对你不能做多少的关注.依旧类型的语言,如Agda,Coq和Epigram,将这种风格发挥到极致和全面的力量.

模板Haskell更像是通常的LISP-macro代码生成方式.你编写一些代码来编写一些代码,然后你说"确定插入生成的代码".与上述技术不同,您可以通过这种方式编写任何可计算指定的代码,但是您没有得到concatV如上所述的非常一般的类型检查.

所以你有几个选择来做你想要的.我认为元编程是一个非常有趣的空间,在某些方面还很年轻.玩得开心.:-)