OCaml 教程 / 依赖记录与类型级编程

(* OCaml 不能直接写出 replicate : (n:int) -> 'a -> 'a list
   其中返回类型依赖于 n 的值，但可以用 GADTs 模拟 *)

(* 先引入类型级自然数 *)
type zero = Zero
type 'n succ = Succ

type _ nat =
  | Z : zero nat
  | S : 'n nat -> 'n succ nat

(* 长度索引向量 *)
type (_, _) vec =
  | Nil : (zero, 'a) vec
  | Cons : 'a * ('n, 'a) vec -> ('n succ, 'a) vec

let x : (zero succ succ, int) vec = Cons (1, Cons (2, Nil))
(* x 是长度为 2 的 int 向量 *)

type zero = Zero
type 'n succ = Succ

type _ nat =
  | Z : zero nat
  | S : 'n nat -> 'n succ nat

(* 类型级自然数：0, 1, 2, 3, ... *)
let n0 : zero nat = Z
let n1 : zero succ nat = S Z
let n2 : zero succ succ nat = S (S Z)
let n3 : zero succ succ succ nat = S (S (S Z))

(* 类型级加法证明 *)
type (_, _, _) plus =
  | PlusZ : (zero, 'n, 'n) plus
  | PlusS : ('m, 'n, 'p) plus
    -> ('m succ, 'n, 'p succ) plus

(* 证明 2 + 1 = 3 *)
let proof_2_plus_1 : (zero succ succ, zero succ, zero succ succ succ) plus =
  PlusS (PlusS PlusZ)

(* 运行时加法 *)
let rec nat_to_int : type n. n nat -> int = function
  | Z -> 0
  | S n -> 1 + nat_to_int n

let rec add_nat : type m n. m nat -> n nat -> (m, n, _) nat =
  fun m n -> match m with
  | Z -> n
  | S m' -> S (add_nat m' n)

let result = add_nat n2 n1  (* 类型: zero succ succ succ nat *)
let () = Printf.printf "2 + 1 = %d\n" (nat_to_int result)

(* ∃(n:nat). vec(n, int) *)
type packed_vec = PV : 'n nat * ('n, int) vec -> packed_vec

let pv1 = PV (S (S Z), Cons (1, Cons (2, Nil)))
let pv2 = PV (S (S (S Z)), Cons (3, Cons (4, Cons (5, Nil))))

(* 获取长度 *)
let pv_length (PV (n, _)) = nat_to_int n

let () = Printf.printf "pv1 length: %d\n" (pv_length pv1)  (* 2 *)
let () = Printf.printf "pv2 length: %d\n" (pv_length pv2)  (* 3 *)

type true_ = True
type false_ = False

type (_, _, _) and_ =
  | AndTT : (true_, true_, true_) and_
  | AndTF : (true_, false_, false_) and_
  | AndFT : (false_, true_, false_) and_
  | AndFF : (false_, false_, false_) and_

type (_, _, _) or_ =
  | OrTT : (true_, true_, true_) or_
  | OrTF : (true_, false_, true_) or_
  | OrFT : (false_, true_, true_) or_
  | OrFF : (false_, false_, false_) or_

type _ not =
  | NotT : true_ not -> false_
  | NotF : false_ not -> true_

type nil = Nil
type ('h, 't) cons = Cons

type _ tlist =
  | TNil : nil tlist
  | TCons : 'h * 't tlist -> ('h, 't) cons tlist

(* 类型级列表操作 *)
type (_, _, _) tappend =
  | TAppendNil : (nil, 'b, 'b) tappend
  | TAppendCons : ('t, 'b, 'c) tappend
    -> (('h, 't) cons, 'b, ('h, 'c) cons) tappend

type (_, _) eq = Refl : ('a, 'a) eq

let cast : type a b. (a, b) eq -> a -> b = fun Refl x -> x

(* 证明 int = int *)
let int_eq_int : (int, int) eq = Refl

(* 对称性 *)
let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl

(* 传递性 *)
let trans : type a b c. (a, b) eq -> (b, c) eq -> (a, c) eq =
  fun Refl Refl -> Refl

type zero = Zero
type 'n succ = Succ

type (_, _) vec =
  | Nil : (zero, 'a) vec
  | Cons : 'a * ('n, 'a) vec -> ('n succ, 'a) vec

(* 安全的 head —— 非空向量一定有 head *)
let head : type n. (n succ, 'a) vec -> 'a = fun (Cons (x, _)) -> x

(* 安全的 tail *)
let tail : type n. (n succ, 'a) vec -> (n, 'a) vec = fun (Cons (_, xs)) -> xs

(* 长度 *)
let rec length : type n a. (n, a) vec -> int = function
  | Nil -> 0
  | Cons (_, xs) -> 1 + length xs

(* 映射 *)
let rec vmap : type n a b. (a -> b) -> (n, a) vec -> (n, b) vec =
  fun f -> function
  | Nil -> Nil
  | Cons (x, xs) -> Cons (f x, vmap f xs)

(* zip —— 两个相同长度的向量 *)
let rec vzip : type n a b. (n, a) vec -> (n, b) vec -> (n, a * b) vec =
  fun xs ys -> match xs, ys with
  | Nil, Nil -> Nil
  | Cons (x, xs'), Cons (y, ys') -> Cons ((x, y), vzip xs' ys')

let v1 : (zero succ succ succ, int) vec =
  Cons (1, Cons (2, Cons (3, Nil)))

let v2 : (zero succ succ succ, string) vec =
  Cons ("a", Cons ("b", Cons ("c", Nil)))

let zipped = vzip v1 v2
(* 类型保证：只能 zip 相同长度的向量 *)

let () =
  let (Cons ((1, "a"), Cons ((2, "b"), Cons ((3, "c"), Nil)))) = zipped in
  print_endline "zipped OK"

(* 编译时安全检查 *)
(* let bad = vzip v1 (Cons (1, Nil))  (* 编译错误！长度不匹配 *) *)

(* 使用类型级自然数作为索引 *)
type (_, _) fin =
  | FZ : ('n succ, zero) fin
  | FS : ('n, 'i) fin -> ('n succ, 'i succ) fin

(* fin 类型：fin(n, i) 表示 i 是 0..n-1 范围内的索引 *)

(* 安全的向量索引访问 *)
let rec vget : type n a i. (n, a) vec -> (n, i) fin -> a =
  fun vec idx -> match vec, idx with
  | Cons (x, _), FZ -> x
  | Cons (_, xs), FS i -> vget xs i
  | Nil, _ -> .  (* 不可能：fin 保证索引在范围内 *)

(* 示例 *)
let v : (zero succ succ succ, int) vec = Cons (10, Cons (20, Cons (30, Nil)))

let idx0 : (zero succ succ succ, zero) fin = FZ
let idx1 : (zero succ succ succ, zero succ) fin = FS FZ
let idx2 : (zero succ succ succ, zero succ succ) fin = FS (FS FZ)

let () =
  Printf.printf "v[0] = %d\n" (vget v idx0);  (* 10 *)
  Printf.printf "v[1] = %d\n" (vget v idx1);  (* 20 *)
  Printf.printf "v[2] = %d\n" (vget v idx2)   (* 30 *)

(* 编译时安全：不能越界 *)
(* let idx3 = FS (FS (FS FZ))  (* 编译时无法匹配 3 元素向量 *) *)

(* 类型级格式化规范 *)
type (_, _) fmt =
  | FEnd : (string, string) fmt
  | FInt : ('r, 's) fmt -> (int -> 'r, 's) fmt
  | FStr : ('r, 's) fmt -> (string -> 'r, 's) fmt
  | FLit : string * ('r, 's) fmt -> ('r, 's) fmt

(* 格式化函数 *)
let rec sprintf : type r s. (r, s) fmt -> r = function
  | FEnd -> ""
  | FInt rest -> fun n -> string_of_int n ^ sprintf rest
  | FStr rest -> fun s -> s ^ sprintf rest
  | FLit (lit, rest) -> lit ^ sprintf rest

(* 格式化字符串解析器 *)
let rec format : type r s. (r, s) fmt -> r -> s = function
  | FEnd -> fun acc -> acc
  | FInt rest -> fun f n -> format rest (f n)
  | FStr rest -> fun f s -> format rest (f s)
  | FLit (_, rest) -> fun f -> format rest f

(* 构建格式化规范 *)
let hello_fmt : (int -> string -> string, string) fmt =
  FLit ("Hello, ", FInt (FLit ("! Your name is ", FStr (FLit (".", FEnd)))))

(* 使用 *)
let result = format hello_fmt (fun n name ->
  Printf.sprintf "Hello, %d! Your name is %s." n name
) 42 "Alice"

(* 更实用的版本 *)
type ('a, 'b) fmt =
  | Lit : string * ('a, 'b) fmt -> ('a, 'b) fmt
  | Int : ('a, 'b) fmt -> (int -> 'a, 'b) fmt
  | Str : ('a, 'b) fmt -> (string -> 'a, 'b) fmt
  | End : (string, string) fmt

let rec ksprintf : type a b. (string -> b) -> (a, b) fmt -> a = fun k -> function
  | End -> k ""
  | Lit (s, rest) -> ksprintf (fun acc -> k (s ^ acc)) rest
  | Int rest -> fun n -> ksprintf (fun acc -> k (string_of_int n ^ acc)) rest
  | Str rest -> fun s -> ksprintf (fun acc -> k (s ^ acc)) rest

let sprintf fmt = ksprintf Fun.id fmt

(* 使用 *)
let my_fmt : (int -> string -> string, string) fmt =
  Lit ("User ", Int (Lit (" is ", Str (End))))

let () = print_endline (sprintf my_fmt 42 "Alice")
(* 输出: "User 42 is Alice" *)

type locked = Locked
type unlocked = Unlocked

type (_, _) action =
  | InsertCoin : (locked, unlocked) action
  | Push : (unlocked, locked) action

type 'state machine = {
  state : string;
  process : 'state;
}

let insert_coin : locked machine -> unlocked machine = fun m ->
  { state = "unlocked (" ^ m.state ^ ")"; process = Unlocked }

let push : unlocked machine -> locked machine = fun m ->
  { state = "locked (" ^ m.state ^ ")"; process = Locked }

(* 使用 *)
let start : locked machine = { state = "initial"; process = Locked }
let opened = insert_coin start
let closed = push opened
let opened_again = insert_coin closed

let () = Printf.printf "Final state: %s\n" opened_again.state

type disconnected = Disconnected
type connected = Connected
type authenticated = Authenticated

type (_, _) protocol =
  | Connect : (disconnected, connected) protocol
  | Authenticate : string -> (connected, authenticated) protocol
  | Disconnect : (_, disconnected) protocol
  | Send : string -> (authenticated, authenticated) protocol
  | Receive : (authenticated, string * authenticated) protocol

type 'state connection = {
  state : string;
  data : 'state;
}

let connect : disconnected connection -> connected connection = fun c ->
  { state = "connected"; data = Connected }

let authenticate : string -> connected connection -> authenticated connection =
  fun _pass c ->
    { state = "authenticated"; data = Authenticated }

let send : string -> authenticated connection -> authenticated connection =
  fun _msg c -> c

let disconnect : type s. s connection -> disconnected connection = fun _c ->
  { state = "disconnected"; data = Disconnected }

(* 使用 *)
let session =
  let c0 : disconnected connection = { state = "init"; data = Disconnected } in
  let c1 = connect c0 in
  let c2 = authenticate "password" c1 in
  let c3 = send "Hello" c2 in
  disconnect c3

let () = Printf.printf "Final: %s\n" session.state

(* ✅ 好的使用场景：简单的 phantom type *)
type 'a validated = Validated of 'a
type unvalidated
type validated

let validate : unvalidated validated -> validated validated =
  fun (Validated x) -> Validated x

(* ✅ 好的使用场景：有限状态机 *)
type off = Off
type on = On
type 'state light = { state : string }

(* ⚠️ 谨慎使用：复杂的类型级计算 *)
(* 当代码变得不可读时，考虑用运行时检查替代 *)