如何使用类型约束将两个数字相加？

Question

在这里，我将加法编码为 1 作为包装元组类型，将减法编码为提取元组类型的第二个元素：

type zero = unit * unit
type 'a minus1 = 'snd constraint 'a = unit * 'snd
type 'a plus1 = unit * 'a

到目前为止，编码有效：

type one = zero plus1
type two = one plus1
type two' = zero plus1 plus1
type two'' = unit * (unit * (unit * unit))

let minus1 ((), n) = n
let plus1 n = ((), n)
let zero = ((), ())
let one : one = plus1 zero
let two : two = plus1 one
let two : two = plus1 (plus1 zero)
let two : two' = two
let two : two'' = two

我试图将加法实现为左侧减 1，右侧加 1，直到左侧为 0，但我不知道如何执行这样的分支逻辑。如果类型信息有一个or，这将表达我正在寻找的内容：

type ('a, 'b) plus = 'res
                (constraint 'a = zero constraint 'res = 'b)
            or  (
                 constraint  ('a_pred, 'b_succ) plus = 'res
                 constraint 'a_pred = 'a minus1
                 constraint 'b_succ = 'b plus1
            )

有没有办法沿着这些思路实施plus？

Answer 1

这不可能直接实现：您无法使用类型约束在类型系统中编码无界计算。但是，您可以使用统一将在类型的某些部分完成的一些计算工作转移到另一部分。

模仿带有加法的自然数的经典 GADT 编码，我们可以定义：

type ('x,'y) nat = 'x * 'y

type 'a zero = ('a, 'a) nat
let zero (type a) (x:a): a zero = x, x

type 'nat s = (unit * 'a, 'b) nat
  constraint 'nat = ('a, 'b) nat

let succ (nat:'s -> 'n) (x:'s) : 'n s  =
  let x, y = nat x in
  ((), x), y

其中类型表示类型的基础整数与自然数('res,'start) nat相加的结果（其本身使用一元皮亚诺编码）natstart

1我们可以检查是否可以构建、2和3的编码

type 'a one = 'a zero s
type 'a two = 'a one s
type 'a three = 'a two s
let one (x:'a): 'a one = succ zero x
let two (x:'a): 'a two = succ one x
let three (x:'a): 'a three = succ two x

那么定义加法就是使用类型统一来组合对每个操作数的类型完成的计算工作：

type ('x,'y) nat = 'x * 'y

type 'a zero = ('a, 'a) nat
let zero (type a) (x:a): a zero = x, x

type 'nat s = (unit * 'a, 'b) nat
  constraint 'nat = ('a, 'b) nat

let succ (nat:'s -> 'n) (x:'s) : 'n s  =
  let x, y = nat x in
  ((), x), y

然后我们可以使用类型检查器来1 + 2 = 3检查

let three' x = (one + two) x
let ok = [ three;  three' ]