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編譯器檢查向量長度

回答

相關問題