Type system and polymorphic let's

Learning
1

Hi there!

I am working on a library to provide a type-safe SI units where the result of a calculation must have the correct physical units.

To do this, the library must track the exponent of each unit through the type system.

To do so, I created a module Nat that does exactly that:

module Nat : sig
  type 'a t
  type 'a s

  val to_int : 'a t -> int
  val zero : 'a. ('a * 'a) t
  val succ : 'a 'b. ('a * 'b) t -> ('a * 'b s) t
  val ( + ) : 'a 'b 'c. ('b * 'c) t -> ('a * 'b) t -> ('a * 'c) t
  val ( - ) : 'a 'b 'c. ('b * 'c) t -> ('b * 'a) t -> ('a * 'c) t
end = struct
  type 'a t = int
  type 'a s

  let to_int n = n
  let zero = 0
  let succ n = n + 1
  let ( + ) a b = a + b
  let ( - ) a b = a - b
end

This work correctly, for example with the code:

let three = Nat.(succ (succ zero) + (succ zero))

let () = Printf.printf "%d\n" (Nat.to_int three)

The problem is that, when I create other variables trough the three var, it does not work anymore:

let six = Nat.(three + three) (* does not type-check anymore *)

The problem is that ocaml inferences the types for three and six (with _week types) and it is not possible to reuse the variables in other expressions.

For example, it is possible to circunvent this issue by creating const functions that output the values when called. This all works fine:

let two () = Nat.(succ zero)
let three () = Nat.(succ (succ zero) + succ zero)
let six () = Nat.(two () + three ())
let () = Printf.printf "%d\n" (Nat.to_int (six ()))

It is possible to keep the upper syntax instead of the lower one?

2

It suffices to add covariant type annotations:

module Nat : sig
type +'a t
type +'a s

  val to_int : 'a t -> int
  val zero : 'a. ('a * 'a) t
  val succ : 'a 'b. ('a * 'b) t -> ('a * 'b s) t
  val ( + ) : 'a 'b 'c. ('b * 'c) t -> ('a * 'b) t -> ('a * 'c) t
  val ( - ) : 'a 'b 'c. ('b * 'c) t -> ('b * 'a) t -> ('a * 'c) t
end = struct
type +'a t = int
type +'a s

  let to_int n = n
  let zero = 0
  let succ n = n + 1
  let ( + ) a b = a + b
  let ( - ) a b = a - b
end
1 Like