OCaml 教程 / GADTs（广义代数数据类型）

(* 普通 ADT *)
type expr =
  | Int of int
  | Add of expr * expr
  | Bool of bool

(* GADT 语法 *)
type 'a value =
  | Int : int -> int value       (* 返回类型是 int value *)
  | Bool : bool -> bool value   (* 返回类型是 bool value *)

type _ term =
  | Int : int -> int term
  | Bool : bool -> bool term
  | Add : int term * int term -> int term
  | If : bool term * 'a term * 'a term -> 'a term

type expr =
  | EInt of int
  | EBool of bool
  | EAdd of expr * expr

type value =
  | VInt of int
  | VBool of bool

let rec eval = function
  | EInt n -> VInt n
  | EBool b -> VBool b
  | EAdd (a, b) ->
    match eval a, eval b with
    | VInt x, VInt y -> VInt (x + y)
    | _ -> failwith "type error"  (* 运行时错误！ *)

type _ value =
  | Int : int -> int value
  | Bool : bool -> bool value

type _ expr =
  | Val : 'a value -> 'a expr
  | Add : int expr * int expr -> int expr
  | Equal : int expr * int expr -> bool expr
  | If : bool expr * 'a expr * 'a expr -> 'a expr

let rec eval : type a. a expr -> a = function
  | Val (Int n) -> n
  | Val (Bool b) -> b
  | Add (a, b) -> eval a + eval b
  | Equal (a, b) -> eval a = eval b
  | If (cond, then_, else_) ->
    if eval cond then eval then_ else eval else_

let two : int = eval (Add (Val (Int 1), Val (Int 1)))
let is_true : bool = eval (Equal (Val (Int 1), Val (Int 1)))
let result : int = eval (If (Val (Bool true), Val (Int 42), Val (Int 0)))

type ('a, 'b) eq = Eq : ('a, 'a) eq  (* 只有当 'a = 'b 时才能构造 *)

let cast : type a b. (a, b) eq -> a -> b = fun Eq x -> x
(* 编译器知道：当 Eq 匹配时，a = b *)

let x : string = cast Eq 42   (* 编译错误！int ≠ string *)
let y : int = cast Eq 42      (* OK *)

type locked = Locked
type unlocked = Unlocked

type 'state door =
  | Closed : locked door
  | Open : unlocked door

let open_door : locked door -> unlocked door = function
  | Closed -> Open

let close_door : unlocked door -> locked door = function
  | Open -> Closed

(* 类型安全：不能打开已经打开的门 *)
(* let bad = open_door Open  (* 编译错误！ *) *)

type initial = Initial
type connected = Connected
type authenticated = Authenticated

type _ connection =
  | Connecting : initial connection
  | Connected : string -> connected connection
  | Authed : string * string -> authenticated connection

let connect : initial connection -> connected connection = function
  | Connecting -> Connected "127.0.0.1"

let authenticate : connected connection -> string -> authenticated connection =
  fun conn password ->
    match conn with
    | Connected host -> Authed (host, password)

let execute : authenticated connection -> string -> string =
  fun (Authed (host, user)) cmd ->
    host ^ ": executing " ^ cmd ^ " as " ^ user

(* ✅ 类型安全的调用链 *)
let session =
  let conn = connect Connecting in
  let authed = authenticate conn "secret" in
  execute authed "SELECT *"

(* ❌ 不能跳过步骤 *)
(* let bad = execute (connect Connecting) "SELECT *"  (* 编译错误！ *) *)

type packed = Pack : 'a * ('a -> string) -> packed

let print_packed (Pack (x, show)) = show x

(* 异构集合 *)
let items : packed list = [
  Pack (42, string_of_int);
  Pack ("hello", fun s -> s);
  Pack (3.14, string_of_float);
]

let () = List.iter (fun p -> print_endline (print_packed p)) items

type any = Any : 'a -> any

let forget x = Any x

type showable = Show : 'a * ('a -> string) -> showable

let show (Show (x, f)) = f x

let items = [Show (42, string_of_int); Show ("hello", Fun.id)]
let () = List.iter (fun x -> print_endline (show x)) items

type 'a typ =
  | TInt : int typ
  | TBool : bool typ
  | TString : string typ

let default_value : type a. a typ -> a = function
  | TInt -> 0
  | TBool -> false
  | TString -> ""

(* 编译器知道匹配 TInt 时 a = int，所以返回 int 是安全的 *)

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

type ('a, 'b) either =
  | Left : 'a -> ('a, 'b) either
  | Right : 'b -> ('a, 'b) either

(* GADT 使得某些函数类型更加精确 *)
let apply_eq : type a b. (a, b) eq -> a -> b = fun Refl x -> x

type _ expr =
  | Lit : int -> int expr
  | Neg : int expr -> int expr
  | Add : int expr * int expr -> int expr
  | And : bool expr * bool expr -> bool expr
  | Not : bool expr -> bool expr
  | Eq : int expr * int expr -> bool expr

let rec eval : type a. a expr -> a = function
  | Lit n -> n
  | Neg e -> -(eval e)
  | Add (a, b) -> eval a + eval b
  | And (a, b) -> eval a && eval b
  | Not e -> not (eval e)
  | Eq (a, b) -> eval a = eval b

let to_string : type a. a expr -> string = function
  | Lit n -> string_of_int n
  | Neg e -> "-(" ^ to_string e ^ ")"
  | Add (a, b) -> "(" ^ to_string a ^ " + " ^ to_string b ^ ")"
  | And (a, b) -> "(" ^ to_string a ^ " && " ^ to_string b ^ ")"
  | Not e -> "!(" ^ to_string e ^ ")"
  | Eq (a, b) -> "(" ^ to_string a ^ " = " ^ to_string b ^ ")"

type 'a witness =
  | WInt : int witness
  | WString : string witness
  | WList : 'a witness -> 'a list witness
  | WOption : 'a witness -> 'a option witness

let rec default : type a. a witness -> a = function
  | WInt -> 0
  | WString -> ""
  | WList _ -> []
  | WOption _ -> None

(* ❌ 陷阱1：忘记局部抽象类型 *)
(* let f (x : int expr) = match x with Lit n -> n | _ -> 0 *)
(* 错误：需要 type annotation *)

(* ✅ 正确写法 *)
let f : int expr -> int = function Lit n -> n | _ -> 0

(* ❌ 陷阱2：GADT 不支持 polymorphic recursion *)
(* 需要额外的类型注解 *)

type _ query =
  | Select : string list -> string list query
  | Where : bool condition * 'a query -> 'a query
  | Limit : int * 'a query -> 'a query

and _ condition =
  | Eq : string * string -> bool condition
  | Gt : string * int -> bool condition
  | And : bool condition * bool condition -> bool condition

let rec string_of_query : type a. a query -> string = function
  | Select cols -> "SELECT " ^ String.concat ", " cols
  | Where (cond, q) ->
    string_of_query q ^ " WHERE " ^ string_of_condition cond
  | Limit (n, q) ->
    string_of_query q ^ " LIMIT " ^ string_of_int n

and string_of_condition : type a. a condition -> string = function
  | Eq (col, val_) -> col ^ " = '" ^ val_ ^ "'"
  | Gt (col, n) -> col ^ " > " ^ string_of_int n
  | And (a, b) ->
    "(" ^ string_of_condition a ^ " AND " ^ string_of_condition b ^ ")"

type _ endpoint =
  | GetUsers : user list endpoint
  | GetUser : int -> user option endpoint
  | CreateUser : user -> user endpoint

and user = { id : int; name : string }

let handle_request : type a. a endpoint -> a = function
  | GetUsers -> [{ id = 1; name = "Alice" }]
  | GetUser id -> Some { id; name = "User " ^ string_of_int id }
  | CreateUser u -> { u with id = 42 }