OCaml编译器检查向量长度 [英] OCaml compiler check for vector lengths

问题描述

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

I was wondering if it is possible to have compile-time check in OCaml to make sure arrays are the correct length. For my problem, I want to verify that two GPU 1-dim vectors are of the same length before doing piecewise vector subtraction.

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菜鸟，所以我想知道如何实现此目标?我猜我将不得不使用函子或camlp4(我以前从未使用过)

In this example I would like it to throw a compile error as x and y are not the same length. As I am a OCaml noob I would like to know how I can achieve this? I am guessing that I will have to use functors or camlp4 (which I have never used before)

推荐答案

您不能在OCaml中为arrays of length n定义类型族，其中n可以具有任意长度.但是，可以使用其他机制来确保仅GpuVector.sub个兼容长度的数组.

You cannot define a type family in OCaml for arrays of length n where n can have arbitrary length. It is however possible to use other mechanisms to ensure that you only GpuVector.sub arrays of compatible lengths.

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

The easiest mechanism to implement is defining a special module for GpuVector of length 9, and you can generalise the 9 by using functors. Here is an example implementation of a module 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的定义随后被编译器拒绝:

The definition of z is then rejected by the compiler:

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

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

We therefore successfully reflected in the type system the property for two arrays of having the same length. You can take advantage of module inclusion to quickly implement a complete GpuVectorFixedLength.Make functor.

这篇关于OCaml编译器检查向量长度的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！