OCaml中的多態遞歸：返回值

Question

繼續我關於類型級算術的一系列問題，我偶然發現了另一個問題：返回多態遞歸函數的類型。

這是代碼：

module Nat : sig 
    type z = Z 
    type 'n s = S of 'n 

    type ('n) nat = 
      Zero : (z) nat 
     | Succ : ('n) nat -> ('n s) nat 

    val of_int : int -> 'n nat 
end = struct 
    type z = Z 
    type 'n s = S of 'n 
    type ('n) nat = 
      Zero : (z) nat 
     | Succ : ('n) nat -> ('n s) nat 

    let rec of_int n : int -> 'n nat = function 
     0 -> Zero 
     | n -> Succ (of_int (n - 1)) 
end 

編譯收率：

Error: This expression [Succ (of_int (n - 1))] has type 'a s nat 
    but an expression was expected of type z nat 

的問題是，該函數的返回值由零匹配子句第一圖案設定爲z NAT。相反，它應該是'a。 '一個nat？嘗試製作添加兩個不同Nat：的函數時也會發生此問題。

感謝您的幫助。

Answer 1

類型int -> 'n nat，意味着forall n, int -> n nat：該函數的用戶可以選擇在該n使用該函數。因此，您可以撥打of_int函數說：「嘿，這次給我一個(z s) nat」，就像您可以選擇哪種類型的[] : 'a list最終結果一樣。這與實際發生的不匹配，這是你不選擇類型，它是由整數值決定的。

根據定義，類型系統不知道整數的值，所以您不能準確地說出您將得到哪種類型的結果爲n nat。所有你可以說的是，有存在某些類型n如結果有類型n nat。您可以使用「存在類型」來表達它，並且有多種方式可以做到這一點，GADT就是其中之一（GADT是代數數據類型加上存在類型和等式約束）。

type some_nat = 
| Some : 'n nat -> some_nat 

let rec of_int = function 
| 0 -> Some Zero 
| n -> 
    let (Some nat) = of_int (n - 1) in 
    Some (Succ nat) 

some_nat是圍繞nat一個存在的包裝，就相當於，如果你有一流的生存類型你可能會寫exists n. n nat。

處理加法更加困難，因爲您必須在類型級別表達您獲得的回報類型與添加其他兩種類型相對應。這裏是我所定義的類型是：

type (_, _, _) add = 
| AddZ : (z, 'b, 'b) add 
| AddS : ('a, 'b, 'c) add -> ('a s, 'b, 'c s) add 

type ('a, 'b) add_result = 
| Result : ('a, 'b, 'c) add * 'c nat -> ('a, 'b) add_result 

let rec add : type a b . a nat -> b nat -> (a, b) add_result = function 
    ... 

我就讓你定義的add身體，這樣你可以用這個東西發揮自己。

我並不是很高興所有的運行時環繞着add類型（這實際上只是作爲一個類型級證人很有用），所以也許有更好的方法。