Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Type-level arithmetics in OCaml

Tags:

types

math

ocaml

Ok, more type hackery failure. :) :P

In my week-long pursuit of getting rid of (runtime) assert(n > 0) and instead checking it statically, I've come up with this module:

module Nat : sig 
  type z
  type 'n s

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

  val add : ('a, 'n) nat -> ('a, 'n s) nat

end = struct          
  type z
  type 'n s
  type ('a, 'n) nat = 
          Zero : ('a, z) nat 
        | Succ : ('a, 'n) nat -> ('a, 'n s) nat 

  let add n = Succ n

  (*  
  let rec to_int n = function 
        | Succ a -> 1 + (to_int a)
        | Zero -> 0
        *)
end

This gives Peano numbers where the number is encoded in it's own type:

# Zero;;
- : ('a, Nat.z) Nat.nat = Zero
# Succ (Zero);;
- : ('a, Nat.z Nat.s) Nat.nat = Succ Zero
# add (Succ Zero);;
- : ('_a, Nat.z Nat.s Nat.s) Nat.nat = Succ (Succ Zero) 

However, the last function to_int won't compile:

Error: This pattern [Zero -> 0] matches values of type ('a, z) nat
   but a pattern was expected which matches values of type
     ('a, ex#0 s) nat

This is, I think, because z and s is different types. Is it possible to make them the same type, and still have them as phantom types?

(Possible duplicate: type level integers in ocaml)

like image 462
Olle Härstedt Avatar asked Mar 30 '13 17:03

Olle Härstedt


People also ask

What is type unit in OCaml?

unit — The Unit Value The built-in printing functions return type unit, for example; the value of a while or for loop (both of which are expressions, not "statements") is also of type unit. OCaml uses this convention to help catch more type errors.

What does type A mean in OCaml?

The type 'a is a type variable, and stands for any given type. The reason why sort can apply to lists of any type is that the comparisons (=, <=, etc.) are polymorphic in OCaml: they operate between any two values of the same type. This makes sort itself polymorphic over all list types.

What does :: mean in OCaml?

Regarding the :: symbol - as already mentioned, it is used to create lists from a single element and a list ( 1::[2;3] creates a list [1;2;3] ). It is however worth noting that the symbol can be used in two different ways and it is also interpreted in two different ways by the compiler.

What is () in OCaml?

This is a way to indicate there is no value for an argument. It's necessary to do this in ML because all functions are unary. You can't have a function with zero arguments, so instead you pass an argument containing no information, which is () .


1 Answers

First, there is a genuine error in your code: it's let to_int = function, not let to_int n = function.

The real problem is that you are using a polymorphic recursive function: you are calling it recursively with different types for the second parameter of the nat type. As type inference of code using polymorphic recursion is undecidable in the general case, OCaml won't try to guess it for you, so you have to be explicit with a polymorphic recursion annotation:

let rec to_int : type n . ('a, n) nat -> int =
   ...

Another point that is not a problem right now but may become one in the future (and show that you still need a bit of training with GADTs): the fact that 'a s and z are distinct types is essential to your function working as you want. It tells you that if you have a value of type ('a, z) nat (note that the 'a parameter is useless in all this stuff), it can only be a Zero. You can write the following functions and they're total, you get no exhaustivity warning:

let is_zero : ('a, z) nat -> unit = function
  | Zero -> ()
  (* case Succ not considered *)

let equal : type n . ('a, n) nat * ('a, n) nat -> bool = function
  | Zero, Zero -> true
  | Succ n1, Succ n2 -> equal (n1, n2)
  (* cases (Zero, SUcc _) or (Succ _, Zero) not considered *)

If there was a possibility that the types z and 'a s overlap (for example if you define type 'a s = z), the type-checker could not reason on these cases being distinct, and you would have to handle the cases that I have omitted here.

The problem with your current definition is that the types 'a s and z are abstracted through a module interface. Inside the definition of the module, the definitions (as distinct abstract types) are visible, but outside the module you don't know anymore how they've been defined, and in fact maybe it was type 'a s = z. So when you are outside the module, you also won't be able to write those functions anymore. The solution is to pick concrete definitions for those types, and let them be visible through the module interface, so that the type-checker always know that they don't overlap:

module Nat : sig
  type z = Z
  type 'a s = S of 'a
  ...
end ...

It doesn't matter that you will never use those Z and S constructors, they're just here to let the type-checker know that z is never equal to 'a s. One could have used int and bool instead.

like image 199
gasche Avatar answered Sep 20 '22 15:09

gasche