In Final Fantasy, the original game for the NES, there are four starter jobs (+ mage variations) and four advanced jobs that they upgrade to. The following example encodes the promotion by associating each job with a number and then checking some properties of that number so that the 'promote' function can't be written to mis-promote a job.
module FF = struct
type job =
| Fighter
| Thief
| Monk
| Mage
| Knight
| Ninja
| Master
| Wizard
end
module Promotion = struct
type z = Z
type 'n s = S of 'n
type (_, _) finite =
| FZ : ('n s, z) finite
| FS : ('n, 'k) finite -> ('n s, 'k s) finite
module N = struct
let fighter = FZ
let thief = FS FZ
let monk = FS (FS FZ)
let mage = FS (FS (FS FZ))
end
type _ job =
| Fighter : z job
| Thief : z s job
| Monk : z s s job
| Mage : z s s s job
| Knight : z s s s s job
| Ninja : z s s s s s job
| Master : z s s s s s s job
| Wizard : z s s s s s s s job
[@@ocamlformat "disable"]
let promote : type n. (z s s s s, n) finite * n job -> n s s s s job =
function
| FZ, Fighter -> Knight
| FS FZ, Thief -> Ninja
| FS (FS FZ), Monk -> Master
| FS (FS (FS FZ)), Mage -> Wizard
| _ -> .
let erase : type n. n job -> FF.job = function
| Fighter -> FF.Fighter
| Thief -> FF.Thief
| Monk -> FF.Monk
| Mage -> FF.Mage
| Knight -> FF.Knight
| Ninja -> FF.Ninja
| Master -> FF.Master
| Wizard -> FF.Wizard
end
usage:
# Promotion.(erase (promote (N.fighter, Fighter)));;
- : FF.job = FF.Knight
# Promotion.(erase (promote ((FS (FS (FS (FS FZ)))), Knight)));;
Error: The constructor FZ has type ('a s, z) finite
but an expression was expected of type (z, 'b) finite
Type 'a s is not compatible with type z
# Promotion.(erase (promote (N.mage, Fighter)));;
Error: The constructor Fighter has type z job
but an expression was expected of type z s s s job
Type z is not compatible with type z s s s
Here we have an ADT for Peano numbers, then a GADT for bounded Peano numbers, then an association of jobs with Peano numbers, finally promote's type expresses both that only the first four jobs can be promoted, and that promotion must add 4 to the job's number.
Of the bounded Peano numbers, note the polymorphic type:
# FS (FZ);;
- : ('a s s, z s) finite = FS FZ
This is double-entry bookkeeping, expressing the same logic in multiple different ways which can be automatically verified to agree with each other. Correctness doesn't always follow from agreement, but incorrectness certainly follows from disagreement: somebody is wrong. An unintentional error (an implementation rather than design error) would have to be made multiple times in the same way to fail to present as disagreement. ype-checking does this, unit tests do it, theorem-proving and refinement types in ATS do it, and you can do it (with admittedly intense machinery) with GADTs.
This OCaml code was adapted from an ATS example:
datatype job(int) =
| fighter(0) | thief(1) | monk(2) | mage(3)
| knight(4) | ninja(5) | master(6) | wizard(7)
fun promote{n:nat | n < 4}(j: job(n)): [m:int | m == n + 4] job(m) =
case+ j of
| fighter() => knight()
| thief() => ninja()
| monk() => master()
| mage() => wizard()
OCaml's not trying to be a dependently typed language so the ergonomics suffer a bit vs. ATS, but I think it's quite typical for OCaml for an explicit proof (N.fighter) to need to be passed along with the GADT. This is similar to fmt's reconstruction of the type of the values passed to it, or Scanf.format_from_string's static format string argument that accompanies the runtime format string:
let () =
try
let fmt = Scanf.format_from_string Sys.argv.(1) "%s%d" in
Printf.printf (fmt ^^ "\n") "camel" 3
with Scanf.Scan_failure _ ->
let fmt = Scanf.format_from_string Sys.argv.(1) "%d%s" in
Printf.printf (fmt ^^ "\n") 3 "camel"
$ ocaml example.ml "I have %d %ss." I have 3 camels. $ ocaml example.ml "%s count: %d" camel count: 3