CODEWITHSUNDEEP
typesocamlgadt
lavi
lavi

Reputation: 237

Nat type with difference list

I am encoding natural numbers as a difference list:

type z = Z
type +'a s = S

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

This allows me to encode addition easily :

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 *)

However the following variant don't 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 *)

Does anybody know how to make it right, i.e. having an efficient typed add, possibly changing the Nat type ?

Note that this question is more general than just the Nat addition: with more complicated sized type, the same question arrise. E.g. with sized list, all the accumlator-based function like rev_append are hard to type.

Upvotes: 3

Views: 248

Answers (1)

gallais
gallais

Reputation: 12113

The problem here is that S i1 has type (l s * m s) nat whilst i has type m * n. The recursive call to add2 is therefore ill-typed: add2 expect the rightmost index of its first argument to match the leftmost one of its second and m s is most definitely different from m.

Because you are encoding a value as a difference, you can easily fix that: you can notice that (l * m) nat and (l s * m s) nat should be the same thing. And you can indeed define a function shift turning one into the other which is basically an identity function:

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

You can then adjust the type of i in the recursive call to add2 to have the whole thing 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)

Edit: getting rid of the non tail-recursive shift.

Continuation Passing Style Transformation

A common technique to turn a function which is not tail-recursive into a tail recursive one is to define it in Continuation Passing Style: the function takes an extra argument which describes what to do with the returned value

We can turn shift into a tail-recursive function shift3 like so:

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

Which then lets us define 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

One (easy but dirty) way of getting rid of the non tail-recursive shift function is to replace it with Obj.magic: indeed, as mentioned before, our shifts are nothing but structurally defined identity functions.

This leads us to:

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)

Upvotes: 1

Related Questions