Created
July 3, 2015 15:22
-
-
Save chambart/a3b05c0895f6afb9cf01 to your computer and use it in GitHub Desktop.
Peano numbers with ocaml functors
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
type zero = unit | |
type 'a succ = unit -> 'a | |
type 'a nat = | |
| Zero : zero nat | |
| Succ : 'a nat -> 'a succ nat | |
module type T = sig | |
type t | |
val v : t nat | |
end | |
module type Rec = functor (T:T) -> T | |
module type Nat = functor (S:Rec) -> functor (Z:T) -> T | |
module Zero = functor(S:Rec) -> functor (Z:T) -> Z | |
module Succ = functor (N:Nat) -> functor(S:Rec) -> functor (Z:T) -> S(N(S)(Z)) | |
module Add = functor (X:Nat) -> functor (Y:Nat) -> functor (S:Rec) -> functor (Z:T) -> X(S)(Y(S)(Z)) | |
module Mul = functor (X:Nat) -> functor (Y:Nat) -> functor (S:Rec) -> functor (Z:T) -> X(Y(S))(Z) | |
module Z : T with type t = zero = struct | |
type t = zero | |
let v = Zero | |
end | |
module S(T:T) : T with type t = T.t succ = struct | |
type t = T.t succ | |
let v = Succ T.v | |
end | |
module One = Succ(Zero) | |
module Two = Succ(Succ(Zero)) | |
module Two' = Add(One)(One) | |
module One_ = One(S)(Z) | |
module Two_ = Two(S)(Z) | |
module Two'_ = Two'(S)(Z) | |
let rec to_int : type n. n nat -> int = function | |
| Zero -> 0 | |
| Succ n -> succ (to_int n) | |
let () = | |
assert(One_.v = Succ Zero); | |
assert(to_int One_.v = 1); | |
assert(Two_.v = Succ Succ Zero); | |
assert(Two_.v = Two'_.v); | |
() |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment