Nat типа со списком разницы

Question

Я кодирующим натуральных чисел в виде списка разницы:

type z = Z 
type +'a s = S 

type _ nat = 
    | Z : ('l * 'l) nat 
    | S : ('l * 'm) nat -> ('l * 'm s) nat 

Это позволяет мне кодировать добавление легко:

let rec add : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat = 
    fun i1 i2 -> match i2 with 
    | Z -> i1 
    | S i -> S (add i1 i) (* OK *) 

Однако следующий вариант не typecheck:

let rec add2 : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat = 
    fun i1 i2 -> match i2 with 
    | Z -> i1 
    | S i -> add2 (S i1) i (* KO *) 

Кто-нибудь знает, как правильно это сделать, то есть с эффективным вводом текста, возможно, ча nging тип Nat?

Обратите внимание, что этот вопрос является более общим, чем просто добавление Nat: с более сложным типом размера, тот же вопрос возникает. Например. с размером списка, все функции на основе накопителей, такие как rev_append, трудно печатать.

Answer 1

Проблема в том, что S i1 имеет тип (l s * m s) nat, тогда как i имеет тип m * n. Таким образом, рекурсивный вызов add2: add2 ожидает, что самый правый индекс его первого аргумента совпадает с самым левым вторым, а m s определенно отличается от m.

Поскольку вы кодируете значение как разницу, вы можете легко исправить это: вы можете заметить, что (l * m) nat и (l s * m s) nat должны быть одинаковыми. И вы действительно можете определить функцию shift поворот одна в другую, которая в основном функция идентичности:

let rec shift : type l m. (l*m) nat -> (l s * m s) nat = function 
    | Z -> Z 
    | S i -> S (shift i) 

Вы можете настроить тип i в рекурсивном вызове add2 иметь всю вещь typecheck:

let rec add2 : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat = 
    fun i1 i2 -> match i2 with 
    | Z -> i1 
    | S i -> add2 (S i1) (shift i) 

Редактировать: избавиться от не-хвост-рекурсивный shift.

Продолжение трансформации Passing Стиль

Общий метод, чтобы включить функцию, которая не является хвостовой рекурсией в хвост рекурсивной один должен определить его в Continuation Passing Style: функция принимает дополнительный аргумент, который описывает, что делать с Возвращаемое значение

Мы можем превратить shift в хвостовую рекурсию функции shift3 следующим образом:

let shift3 : type l m. (l*m) nat -> (l s * m s) nat = 
    let rec aux : type l m c. ((l s * m s) nat -> c) -> (l * m) nat -> c = 
    fun k i -> match i with 
    | Z -> k Z 
    | S j -> aux (fun i -> k (S i)) j 
    in fun i -> aux (fun x -> x) i 

Который затем позволяет нам определить add3:

let rec add3 : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat = 
    fun i1 i2 -> match i2 with 
    | Z -> i1 
    | S i -> add3 (S i1) (shift3 i) 

Sledgehammer: Obj.magic

Один (простой, но грязный) способ избавиться от не хвост рекурсивной shift функции заменить ее Obj.magic: в самом деле, как уже упоминалось ранее, наш shift s - это не что иное, как структурно определенные функции идентичности.

Это приводит нас к:

let shift4 : type l m. (l*m) nat -> (l s * m s) nat = Obj.magic 

let rec add4 : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat = 
    fun i1 i2 -> match i2 with 
    | Z -> i1 
    | S i -> add4 (S i1) (shift4 i)