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)
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.
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.
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.
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 () .
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With