Проверка компилятора OCaml для длины вектора

Question

Мне было интересно, есть ли возможность проверки времени компиляции в OCaml, чтобы убедиться, что массивы имеют правильную длину. Для моей проблемы, я хочу проверить, что два GPU 1-dim-вектора имеют одинаковую длину, прежде чем делать кусочно-векторное вычитание.

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 (которые я никогда раньше не использовал)

Answer 1

Вы не можете определить семейство типов в OCaml для arrays of length n, где n может иметь произвольную длину. Тем не менее, можно использовать другие механизмы для обеспечения того, чтобы вы только GpuVector.sub массивов совместимых длин.

Самый простой механизм для реализации - это специальный модуль для GpuVector длины 9, и вы можете обобщить 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 

Поэтому мы успешно отразили в системе типов свойство для двух массивов одинаковой длины. Вы можете воспользоваться включением модулей, чтобы быстро реализовать полный функтор GpuVectorFixedLength.Make.

Answer 2

Библиотека slap реализует такие статические проверки размера (для линейной алгебры). Описан общий подход this abstract