2

Continuing my series of questions regarding type-level arithmetic, I stumbled across another problem: return types of polymorphic recursive functions.

This is the code:

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

Compiling yields:

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

The problem is that the return value of the function is set to z nat by Zero in the first pattern matching clause. Instead it should be something like 'a. 'a nat? This problem also occurs when trying to make a function that adds two different Nat:s.

Grateful for your help.

4

1 回答 1

4

The type int -> 'n nat, means forall n, int -> n nat: the user of the function may choose at which nto use the function. So you could call the of_int function saying "hey, give me a (z s) nat this time", just like you can pick which type [] : 'a list ends up being. That doesn't match what really happens, which is that you do not choose the type, it is determined by the value of the integer.

By definition, the value of the integer is not known to the type system, so you can't say precisely which type n nat you will get as a result. All you can say is that there exists some type n such as the result has type n nat. You can express that using "existential types", and there are various ways to do that, GADTs being one of them (GADTs are algebraic datatypes plus existential types and equality constraints).

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 is an existential wrapping around nat, it is equivalent to what you might write exists n. n nat if you had first-class existential types.

Handling addition is even harder, because you have to express at the type level that the type you get in return really corresponds to the addition of two other types. Here is how I defined the type for it:

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
   ...

I'll let you define the body of add so that you can play with this stuff yourself.

I'm not very happy of all the runtime wrapping that goes around the add type (which is really just useful as a type-level witness), so maybe there is a better way.

于 2013-03-31T13:58:20.573 回答