https://x.com/5htco/status/1910790679451906457

gistfile1.txt

Ця система типів є фундаментом і алгебраїчної геометрії тому шо квантор узагальнення Pi
є нетривіальним ізоморфізмом до розшарування Fiber Bundle, використовується як
основний примітив алгебраїчної геометрії.

  type term =

I) Мова складається з 5 слів. 2 слова універсальні для всіх типізованих мов програмування.

1) Перше слово --- це "Змінна" --- інтуітивно природнє поняття, яке показує іменоване алфавітами або числами місце в програмі-реченні, що може містити інші програми-речення.

  | Var of string

2) Друге слово -- це "Всесвіт", що містить всі типи аксіоми мови (в даному випадку тільки одни тип --- "Розшарування".

  | Universe of int

let universe = function
    | Universe i -> i
    | _ -> raise (Failure ("Expected a universe"))

II) Далі йде те, що називається одноаксіоматичною системою, де аксіомою (або типом) називається складна конструкція, яка нагадує ізоморфізм, в даному випадку це Pi тип "Розшарування", який складається з трьох слів:

3) "Узагальнення" (правило формації),

4) "Лямбда" (правило ускладнення),

5) "Застосування" (правило спрощення, або аплікація --- застосування функції до аргументу, виконання підстановки змінної в тілі функції і заміна цих місць на аргумент).

let rec subst x s = function
    | Var y -> if x = y then s else Var y
    | Pi (y, a, b) when x <> y -> Pi (y, subst x s a, subst x s b)
    | Lam (y, a, b) when x <> y -> Lam (y, subst x s a, subst x s b)
    | App (f, a) -> App (subst x s f, subst x s a)
    | t -> t

Не існує більш компактної системи яка реалізує конструктивно "Розшарування".

  | Pi of string * term * term   (* ∀ (x : a), b *)
  | Lam of string * term * term  (* λ (x : a), b *)
  | App of term * term

Тут важливо сказати, шо ви можете знайти в літературі системи, де конструктори Pi і Lam містять string * term, для таких систем важко побудувати бідірекшінал тайп-чекер, тому розберіться самі чому саме string * term * term надається у якості рекомендації.

III) Виконання логіки відбувається в контексті, який є просто "Списком" "Пар" "Ім'я" "Слово" в класичному розумінні, проце слова ці вже стосуються мета-мови, на якій пишеться цей інтепретатор, який ми будемо називати "Внутрішньою" мовою.

  type context = (string * term) list

Отже контекст --- це мета-рівень. Щодо мета рівня, то студенту важливо знати, що для імплементації теорії типів для одноаксіоматичної системи "Розшарування" потрібна мова де дозволена взаємна рекурсія для функцій, тому, що функція дефініційної "Рівності" яка використовується для порівняння нормалізованих термів, функції Покрокової нормалізації "Редюс" і "Нормалайз", а також головна функція виводу типів для деталізації рівня бідірекшинал тайп чекерів.

let rec lookup x = function
    | [] -> raise (Failure ("Unbound variable: " ^ x))
    | (y, typ) :: rest -> if x = y then typ else lookup x rest

IV) Функція синтаксичного начоного дослівного порівняння програм-речень мови містить важливі симетричні рядки

    | Lam (x, _, b), t -> equal ctx b (App (t, Var x))
    | t, Lam (x, _, b) -> equal ctx (App (t, Var x)) b

які називаються бета і ета правилами лямбда числення. Зверніть на це увагу. Інші правила анонсують змінну в контексті для порівнняння тіл функцій і предикативне кумулятивне порівняння всесвітів:

let rec equal ctx t1 t2 = match t1, t2 with
    | Var x, Var y -> x = y
    | Universe i, Universe j -> i <= j
    | Pi (x, a, b), Pi (y, a', b')
    | Lam (x, a, b), Lam (y, a', b') -> equal ctx a a' && equal ((x,a) :: ctx) b (subst y (Var x) b')
    | App (f, a), App (f', a') -> equal ctx f f' && equal ctx a a'
    | _ -> false

V) Бідірекшинал тайп чекери, це такі тайпчекери, у яких шоб перевірити чи терм відповідає типу, виводять тип цього терма і порівнюють його з типом за допомогою вбудованої дефініційної рівності.

and infer ctx t =
    let res = match t with
    | Var x -> lookup x ctx
    | Universe i -> Universe (i + 1)
    | Pi (x, a, b) -> Universe (max (universe (infer ctx a)) (universe (infer ((x,a)::ctx) b)))
    | Lam (x, a, b) -> let _ = infer ctx a in Pi (x, a, infer ((x,a)::ctx) b)
    | App (f, a) ->
      match infer ctx f with
      | Pi (x, _, b) -> subst x a b
      | t -> raise (Failure "Requires a Pi type.")
    in normalize ctx res

VI) Покрокова нормалізація це техніка яка виконує атомарні нормалізації допоки є шо нормалізувати, тобто попердній крок нормалізації і наступний відрізняються.

and reduce ctx t = match t with
    | App (Lam (x, _, b), a) -> subst x a b
    | App (Pi (x, _, b), a) -> subst x a b
    | App (f, a) -> App (reduce ctx f, reduce ctx a)
    | _ -> t

and normalize ctx t =
    let t' = reduce ctx t in
    if equal ctx t t' then t else normalize ctx t'

Це повний технічний коментар на мову Хенк від Групоїд Інфініті.
Постійне посилання твору: https://henk.groupoid.space/src/ocaml/henk.ml