cafe
cafe copied to clipboard
groupoid
Pitometsu here
Вітаю!
З хороших новин: Github розщедрився розблокувати мій новий персональний акаунт https://github.com/ypytomets тож якщо ваша ласка, прошу надіслати інвайт, після чого можу не використовувати тут корпоративний.
Друге: @5HT , стало цікаво у якості тренування пописати інтерпритатори-комбінатори. Можливо SKI, CEK, tree calculus, чи щось схоже, визначусь в процесі до чого серце ляже. Думаю буде треба написати AST, та small-step семантику яка й буде інтерпритатором. Можливо захочу додати щось meta-language рівня: якісь макроси чи кодогенерацію, або розмічене AST. Також буде цікаво написати доведення якихось метотеорітичних властивостей обчислень, накшталт нормалізації, й, можливо, якісь ізоморфізми між ними. Абсолютно не претендую на повноту покриття цієї теми, то як проба пера. У зв'язку з чим @5HT хочу спитати порадити, якою мовою то краще писати? Найзнайоміше -- Haskell, якщо трохи згадати -- то OCaml теж підійде. З плюсів: швидкий рантайм та перевірка типів. Але вони дуже обмежено підходять коли справа йде про метотеоретичні твердження щодо цільової вбудованої мови. Тож може є сенс обрати одну з мов Groupoid (наразі жодна не є знайомою), чи варто обрати якусь, й яку?
Привіт, друже!
Відповідаю по пунктах:
-
@ypytomets додав.
-
SKI, CEK, TC ввжаються тупиковими навчальними методиками. Групоїд Інфініті не використовує і не радить це у якості навчальних мов. Перелік навчальних мов Групоїд Інфініті цілком фіксований, я провів 20 років колекціонуючи мови і створючи курс. В мому курсі є лише мови, які описані в томах 2 і 3. Тобто обов'язкові до імплементації наступні мови: ULC, STLC (Alonso), PI (Henk), PI-Self (Yves), PI-SIGMA, PI-SIGMA-EQU. Шоб доводити властивості які ти хочеш жодна з перелічених мов до EQU не підійде якшо не урізана версія IPL, але навіть IPL потребує 0, 1, 2 типи, яких немає в жодній з перелічених навчальних систем, і які ся вводять лише з MLTT, як базис W-рекурсії.
-
В Групоїд Інфініті ми пишемо мови ТІЛЬКИ на OCaml, в SYNRC це ше мови Erlang/Elixir/C/Rust.
Зроблено, дякую. Щодо мов:
ULC не підходить для мета-теоретичного навчання по своїм властивостям (наведено деякі тези тут https://x.com/Pitometsu/status/1940811654352318716 ). А на якій мові краще писати реалізацію та докази, щоб це було ще й для інституту корисніше? Так-то реалізацію можна на OCaml, а докази -- на Coq (або збочено вбудовувати в type-level). Або все одразу на Coq. Або використати одну з мов інституту (PI-SIGMA-EQU?), чи буде це гарна ідея?
Які мета-теоретичні властивості цікаво дослідити, наприклад (що LC не дуже підходить для них) -- можливість денотаційної тотожності термів з ідентичною операційною семантикою в мові (не певен, чи можна назвати це екстенсіональністю), без використання явного типа-рівності в мові (простими словами -- однакова поведінка відповідає строго одному унікальному терму). Чим більш синтаксично семантично-рівні терми будуть схожі, тим простіше це буде зробити (α-conversion та порядок аргументів це ускладнюють, наприклад).
Я не певен, чи має це сенс в принципі, але цікаво, й плюс нагода на практиці щось почати власне робити-просуватись.
Дуже гарні питання! Наконєц-то, дякую, hell yeah!
Якшо дуже просто відповідати і по суті, то:
-
Coq* --- це мінімальна система Групоїд Інфініті у якій можливий сучасний Equational Reasoning на J елімінаторі. Писати в Coq, доводити там властивості за допомогою рівності і екстрактити в OCaml --- це ідіоматичний workflow процес Групоїд Інфініті. Це Default. Можна в другу сторону, як в формалізаціях на Хаскелі. Спочатку пишем на OCaml а потім портуємо сигнатури в Coq/Lean/Agda і доводим там властивості (так верифікувалась L4, тільки з C). Це дефаултні моделі доведення властивостей програм (regular computer software).
-
Інша експериментальна модель доведення регулярних програм, яка дозволена і курується в Групоїд Інфініті --- це доведення об'єктного коду (тобто всіх бітфліпів), як в таких роботах як CoqAsm та Verified LISP Interpreter. Тут великий потенціал для Kind і курсових робіт Yves.
- Coq тут мінімальна система тому що це Pi, Sigma, Equ, Ind, Prop, а в Lean є до цього всього ще Quotient, таким чином там можна довести ще більше властивостей. Coq, Lean і Agda це поки шо всьо з пруверів шо дозволено. У мене просто немає капасіті курувати інші проєкти.
На Coq теж можна мови писати на coq.io, це той чувак шо тезос зробив на https://formal.land В нас навіть є репозиторій N2O для Coq https://github.com/o29/ Там приклад CLI на coq.io, це Feb 15, 2017. Можеш продовжити цей напрямок і на Coq.io написати Henk наприклад.
Require Import Coq.Lists.List.
Require Import Io.All.
Require Import String.
Require Import Io.System.All.
Require Import ListString.All.
Import ListNotations.
CoInductive Co (E : Effect.t) : Type -> Type :=
| Ret : forall (A : Type) (x : A), Co E A
| Bind : forall (A B : Type), Co E A -> (A -> Co E B) -> Co E B
| Call : forall (command : Effect.command E), Co E (Effect.answer E command)
| Split : forall (A : Type), Co E A -> Co E A -> Co E A
| Join : forall (A B : Type), Co E A -> Co E B -> Co E (A * B).
Arguments Ret {E} _ _.
Arguments Bind {E} _ _ _ _.
Arguments Call {E} _.
Arguments Split {E} _ _ _.
Arguments Join {E} _ _ _ _.
Definition ret {E : Effect.t} {A : Type} (x : A) : Co E A := Ret A x.
Definition split {E : Effect.t} {A : Type} (x1 x2 : Co E A) : Co E A := Split A x1 x2.
Definition join {E : Effect.t} {A B : Type} (x : Co E A) (y : Co E B): Co E (A * B) := Join A B x y.
Definition call (E : Effect.t) (command : Effect.command E):
Co E (Effect.answer E command) := Call (E := E) command.
Notation "'ilet!' x ':=' X 'in' Y" := (Bind _ _ X (fun x => Y))
(at level 200, x ident, X at level 100, Y at level 200).
Notation "'ilet!' x : A ':=' X 'in' Y" := (Bind _ _ X (fun (x : A) => Y))
(at level 200, x ident, X at level 100, A at level 200, Y at level 200).
Notation "'ido!' X 'in' Y" := (Bind _ _ X (fun (_ : unit) => Y))
(at level 200, X at level 100, Y at level 200).
Definition read_line : Co effect (option LString.t) :=
call effect ReadLine.
Definition printl (message : LString.t) : Co effect bool :=
call effect (Print (message ++ [LString.Char.n])).
Definition log (message : LString.t) : Co effect unit :=
ilet! is_success := printl message in
ret tt.
Definition run (argv : list LString.t): Co effect unit :=
ido! log (LString.s "What is your name?") in
ilet! name := read_line in
match name with
| None => ret tt
| Some name => log (LString.s "Hello " ++ name ++ LString.s "!")
end.
Parameter infinity : nat.
Parameter error : forall {A B}, A -> B.
Fixpoint eval_aux {A} (steps : nat) (x : Co effect A) : Lwt.t A :=
match steps with
| O => error tt
| S steps =>
match x with
| Ret _ v => Lwt.ret v
| Call c => eval_command c
| Bind _ _ x f => Lwt.bind (eval_aux steps x) (fun v_x => eval_aux steps (f v_x))
| Split _ x1 x2 => Lwt.choose (eval_aux steps x1) (eval_aux steps x2)
| Join _ _ x y => Lwt.join (eval_aux steps x) (eval_aux steps y)
end
end.
Definition eval {A} (x : Co effect A) : Lwt.t A :=
eval_aux infinity x.
CoFixpoint handle_commands : Co effect unit :=
ilet! name := read_line in
match name with
| None => ret tt
| Some command =>
ilet! result := log (LString.s "Input: " ++ command ++ LString.s ".") in
handle_commands
end.
Definition launch (m : list LString.t -> Co effect unit): unit :=
let argv := List.map String.to_lstring Sys.argv in
Lwt.launch (eval (m argv)).
Definition corun (argv : list LString.t): Co effect unit :=
handle_commands.
Definition main :=
launch corun. (* launch run. *)
Extract Constant infinity => "let rec inf = S inf in inf".
Extract Constant error => "fun _ -> failwith ""Unexpected end""".
Extraction "extraction/main" main.