# Type system and polymorphic let's

**URL:** <https://discuss.ocaml.org/t/type-system-and-polymorphic-lets/14990>\
**Category:** Learning\
**Created:** [July 18, 2024, 4:08pm UTC](https://discuss.ocaml.org/t/type-system-and-polymorphic-lets/14990 "2024-07-18T16:08:11Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![bml](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/bml/32/4744_2.png) [@bml](https://discuss.ocaml.org/u/bml)\
**Post date:** [July 18, 2024, 4:08pm UTC](https://discuss.ocaml.org/t/type-system-and-polymorphic-lets/14990/1 "2024-07-18T16:08:11Z")

</div>

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:

```auto
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:

```auto
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:

```auto
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:

```auto
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?

---

<div class="post-metadata">

**Author:** ![sacerdot](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/sacerdot/32/4144_2.png) [@sacerdot](https://discuss.ocaml.org/u/sacerdot)\
**Post date:** [July 18, 2024, 4:35pm UTC](https://discuss.ocaml.org/t/type-system-and-polymorphic-lets/14990/2 "2024-07-18T16:35:41Z")

</div>

It suffices to add covariant type annotations:

```auto
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

```