在F#和Haskell(依赖类型)中键入向量维数的约束

Question

我是F#和Haskell的新手,我正在实施一个项目,以确定我希望将更多时间花在哪种语言上.

我有很多情况,我希望给定的数字类型基于给予顶级函数的参数给定维度(即,在运行时).例如,在这个F#片段中,我有

type DataStreamItem = LinearAlgebra.Vector<float32>

type Ball =
    {R : float32;
     X : DataStreamItem}

我希望所有类型的实例DataStreamItem都有D尺寸.

我的问题在于算法开发和调试的兴趣,因为这样的形状错配错误可能是令人头疼的问题,但是当算法正在运行时应该是一个非问题:

有没有办法在F#或Haskell中约束DataStreamItem和/或Ball维度D？或者我是否需要在每次计算时采用模式匹配？

如果是后者,是否有任何好的,轻量级的范例可以在它们发生时立即捕获这些约束违规(当性能至关重要时可以删除)？

编辑:

澄清D受约束的意义:

D定义为如果您将函数的算法表示main(DataStream)为计算图,则所有中间计算将取决于D执行的维度main(DataStream).我能想到的最简单的例子将是一个点积M有DataStreamItem:的尺寸DataStream将确定的尺寸参数的创建M

另一个编辑:

一周之后,我发现以下博客准确概述了我在Haskell中依赖类型中寻找的内容:

https://blog.jle.im/entry/practical-dependent-types-in-haskell-1.html

另一个: 这个reddit包含了一些关于Haskell中Dependent Types的讨论,并且包含了一篇关于 R. Eisenberg 非常有趣的论文提案的链接.

Answer 1

Haskell而不是F#类型系统都不足以(直接)表达" 递归类型T的N个嵌套实例,其中N在2到6之间 "或" 一串字符正好为6个长 "的语句.不是那些确切的术语,至少.

我的意思是,当然,你总是可以表达这样一个6长字符串类型type String6 = String6 of char*char*char*char*char*char或某种类型的变体(技术上应该足够你的特定例子用矢量,除非你没有告诉我们整个例子),但是你不能说类似的东西type String6 = s:string{s.Length=6},更重要的是,你不能定义表格的功能,在concat: String<n> -> String<m> -> String<n+m>哪里n和m表示字符串长度.

但你不是第一个提出这个问题的人.这个研究方向确实存在,被称为" 依赖类型 ",我可以将其最基本的要点表达为" 对类型进行更高阶,更强大的操作 "(而不仅仅是联合和交集,就像我们所拥有的那样) ML语言) - 注意在上面的例子中我如何String使用数字而不是另一种类型参数化类型,然后对该数字进行算术运算.

在这个方向上最突出的语言原型(我知道)是Agda,Idris,F*和Coq(并不是真正的全部AFAIK).检查出来,但要注意:这是明天的优势,我不建议基于这些语言开始一个大项目.

(编辑:显然你可以在Haskell中做一些技巧来模拟依赖类型,但它不是很方便,你必须启用UndecidableInstances)

或者,您可以选择在运行时进行检查的较弱解决方案.一般要点是:将矢量类型包装在一个普通的包装器中,不允许直接构造它,而是提供构造函数,并使这些构造函数确保所需的属性(即长度).就像是:

type Stream4 = private Stream4 of DataStreamItem
   with
      static member create (item: DataStreamItem) =
         if item.Length = 4 then Some (Stream4 item)
         else None

         // Alternatively:
         if item.Length <> 4 then failwith "Expected a 4-long vector."
         item

以下是对Scott Wlaschin方法的更全面解释:约束字符串.