OCaml编译器检查向量长度

我想知道是否可以在OCaml中进行编译时检查，以确保数组的长度是正确的。对于我的问题，我想验证两个GPU 1-dim矢量在进行分段矢量减法之前具有相同的长度。OCaml编译器检查向量长度

let init_value = 1 
let length = 10_000_000 
let x = GpuVector.create length init_value and y = GpuVector.create 9 init_value in 
let z = GpuVector.sub v1 v2

在这个例子中，我希望它抛出一个编译错误，因为x和y的长度不一样。由于我是OCaml noob，我想知道我如何实现这一目标？我猜测我将不得不使用函数或camlp4（我从未使用过）

来源

2014-02-21 user3199023

OCaml本身没有依赖类型，它可以用来静态检查数组长度不匹配。你可以做的一件事是使用幻像类型，它携带一个幻像编码数组长度。这些编码可以使用CamlP4从整型常量自动生成......但这不是依赖类型，可能不足以满足您的需求。 – camlspotter

@camlspotter我刚刚找到你的评论。有类似的问题。你能提供一些关于将自然数编码为类型的提示/指针吗？ – krokodil

@ krokodil，现在你可以尝试一巴掌，就像Pierre在他的回答中指出的那样。 – camlspotter

您无法在OCaml中定义一个类型族，arrays of length n其中n可以具有任意长度。然而，可以使用其他机制来确保您只有GpuVector.sub兼容长度的阵列。

最容易实现的机制是为长度为9的GpuVector定义一个特殊模块，您可以通过使用函数来概括9。这里是一个模块GpuVectorFixedLength的示例实现：

module GpuVectorFixedLength = 
struct 
module type P = 
sig 
    val length : int 
end 

module type S = 
sig 
    type t 
    val length : int 
    val create : int -> t 
    val sub : t -> t -> t 
end 

module Make(Parameter:P): S = 
struct 
    type t = GpuVector.t 
    let length = Parameter.length 
    let create x = GpuVector.create length x 
    let sub = GpuVector.sub 
end 
end

您可以使用此说，例如

module GpuVectorHuge = GpuVectorFixedLength.Make(struct let length = 10_000_000 end) 
module GpuVectorTiny = GpuVectorFixedLength.Make(struct let length = 9 end) 
let x = GpuVectorHuge.create 1 
let y = GpuVectorTiny.create 1

的z的定义，然后由编译器拒绝：

let z = GpuVector.sub x y 
         ^
Error: This expression has type GpuVectorHuge.t 
     but an expression was expected of type int array

因此，我们在类型系统中成功地反映了具有相同长度的两个数组的属性。您可以利用模块包含来快速实现完整的仿函数。

来源

2014-09-18 06:23:04

slap库实现了这种类型的大小静态检查（线性代数）。整体方法描述如下this abstract

来源

2014-09-18 08:18:41

抽象链接似乎不存在（404）;你知道现在哪里可以找到它吗？ – akavel

这不完全是原始摘要，但这是我认为更完整的 http://eptcs.web.cse.unsw.edu.au/paper.cgi?ML2014.1.pdf –

OCaml编译器检查向量长度

回答

相关问题