Objective Caml - Вторник, 19 июня 2012

Objective Caml

ocaml@conference.jabber.ru

Вторник, 19 июня 2012< ^ >

Конфигурация комнаты

Участники комнаты

GMT+4
[00:01:28] <Kakadu> # type t = [ `Int of int | `Bool of bool ];;
type t = [ `Bool of bool | `Int of int ]
# let and_ (`Bool x) (`Bool y) = `Bool (x & y);;
val and_ : [< `Bool of bool ] -> [< `Bool of bool ] -> [> `Bool of bool ] =  <fun>
# let plus (`Int x) (`Int y) = `Int (x+y);;
val plus : [< `Int of int ] -> [< `Int of int ] -> [> `Int of int ] = <fun>
[00:02:14] <Kakadu> Надо что-т1 на4у42ит0
[00:02:20] <gds> хорошо.  Добавим
value eval : t -> .. ? в какой тип вычисляем выражение ? ..
[00:02:20] <Kakadu> тьфу
[00:03:01] ermine вышел(а) из комнаты
[00:03:07] <Kakadu> однозначно не сказать
[00:03:11] <Kakadu> смотря как написать
[00:04:04] <gds> чтобы было не так скучно с Int и Bool, можно добавить `If : t -> t -> t -> t (который `If val_cond val_then val_else).
Про val_cond не сможешь гарантировать, что оно булевое, про val_{then,else} -- что они имеют одинаковый тип.
[00:04:56] <gds> гарантировать -- статически, имею ввиду.
[00:05:21] <gds> а в HM-типизации подобные гарантии легче всего делаются параметризацией типа.
[00:06:05] <Kakadu> НМ?
[00:06:32] <gds> хиндли-милнер
[00:06:45] <Kakadu> а
[00:09:03] <Kakadu> так?
type 'a t =    [ `Bool of bool | `If of [ `Bool of bool ] * 'a * 'a | `Int of int ]
# `If (`Bool false,`Int 0,`Int 1);;
- : [> `If of [> `Bool of bool ] * [> `Int of int ] * [> `Int of int ] ] =`If (`Bool false, `Int 0, `Int 1)
[00:14:04] <gds> вот, что-то наподобие этого.  Но в `If условие может быть не только `Bool of bool, но и `And of bool t * bool t.  Или, что интереснее, вызовом функции, про которую знаем, что она возвращает bool.
[00:16:19] <Kakadu> Ну а с гадами как будет?
[00:21:26] <gds> Kakadu: например, как-то так:
type 'a t =
  Bool of (bool, 'a) eq * bool
| If of bool t * 'a * 'a
| And of (bool, 'a) eq * bool t * bool t
| Plus of (int, 'a) eq * int t * int t
и при матче значения с типом 'a t в каждой из веток, где есть ('a, 'b) eq, можно получить гарантию того, что это конкретное значение имело тип bool t или int t, например.
[00:22:47] <gds> то есть, если x = And eq b1 b2, то знаешь, что x имеет тип bool t.
[00:25:40] <Kakadu> какая-то магия
[00:25:55] <Kakadu> eq это видимо заклинание для равенства типов
[00:28:21] <gds> не заклинание, а трюк.  Но можно его сделать заклинанием с магией (эффективнее, но не все доверяют Obj, поэтому олег сделал и без магии).
[00:29:13] <Kakadu> > x = And eq b1 b2
ты имел ввиду x = And (eq, b1, b2)
?
[00:29:45] <gds> lf
[00:29:49] <gds> lflflf
[00:31:07] <gds> по сути, да, eq можно сделать типом, для которого наружу вытащено, в том числе,
type ('a,'b) eq
val refl : ('a,'a) eq
то есть, там, где знаешь, что два разных типа на самом деле равны, можно сделать такое вот "свидетельство" их равенства.  И можно от одного типа "перейти" к другому:
val apply_eq : ('a,'b) eq -> 'a -> 'b
[00:31:50] Kakadu нервно смеется
[00:57:01] <Kakadu> любопытно однако. Оно компилируется
[01:06:40] f[x] вышел(а) из комнаты
[01:22:21] Kakadu вышел(а) из комнаты
[01:32:33] bobry вышел(а) из комнаты
[01:49:15] ludovik вышел(а) из комнаты
[01:50:31] ftrvxmtrx вышел(а) из комнаты
[02:19:19] tilarids вышел(а) из комнаты: Computer went to sleep
[02:38:58] Typhon вошёл(а) в комнату
[03:31:51] Typhon вышел(а) из комнаты
[03:33:48] Typhon вошёл(а) в комнату
[04:23:26] Typhon вышел(а) из комнаты
[04:45:01] letrec вошёл(а) в комнату
[07:19:20] Sun][ вошёл(а) в комнату
[08:12:44] klapaucius вышел(а) из комнаты
[08:28:58] Sun][ вышел(а) из комнаты
[08:33:18] tilarids вошёл(а) в комнату
[09:20:38] ermine вошёл(а) в комнату
[09:36:59] Vinzent вошёл(а) в комнату
[09:38:06] Sun][ вошёл(а) в комнату
[09:51:38] bobry вошёл(а) в комнату
[10:28:00] bobry вышел(а) из комнаты
[11:22:19] klapaucius вошёл(а) в комнату
[11:39:54] Kakadu вышел(а) из комнаты
[11:42:19] ftrvxmtrx вошёл(а) в комнату
[11:44:01] Kakadu вошёл(а) в комнату
[11:45:46] Kakadu вошёл(а) в комнату
[11:52:04] tilarids вышел(а) из комнаты: Computer went to sleep
[12:03:34] Sun][ вышел(а) из комнаты
[12:03:38] Sun][ вошёл(а) в комнату
[12:04:38] letrec вышел(а) из комнаты
[12:12:59] <f[x]> хм, камлобилд не пробрасывает cflags при компиляции стабов?
[12:23:36] Vinzent вышел(а) из комнаты
[12:29:33] <Kakadu> Sun][: привет
[12:29:45] <Kakadu> давай бросай свои кресты, занимайся камлом
[12:29:56] <Kakadu> и вообще ты обещал ocaml-qml запилить)
[12:33:28] Sun][ вышел(а) из комнаты
[12:34:36] <Kakadu> всё-таки revised синтаксис выглядит как-то стрймно
[12:34:46] <Kakadu> стрёмно*
[12:35:00] letrec вошёл(а) в комнату
[12:35:03] <Kakadu> а Sun][ опять сбежал
[12:35:20] <Kakadu> такое ощущение, что он --- студент, а я --- его научник
[13:10:43] tilarids вошёл(а) в комнату
[13:12:19] tilarids вышел(а) из комнаты: Computer went to sleep
[13:20:01] <Kakadu> gds: А можно вернуться к гадтам? Я вот думал, что понял, но оказывается, что не понял.  Вот я взял вчерашний пример http://paste.in.ua/4411/raw/. Оно компилится и на 4.00 и на 3.12.1 и один результат. Следовательно я не понял как их использовать
[13:22:49] <Kakadu> или погодите, refl это трюк чтобы сэмулировать гадты там где их нет?
[14:08:32] <gds> Kakadu: refl -- это гадты, где свидетельство типов протаскивается в рантайме.
[14:08:52] <gds> вот потому я и говорю, что гадты в окамле уже стопиццот лет есть.
[14:09:42] <gds> с другой стороны, гадты не очень-то и полезны по сути.  Где они полезны -- в дсл, точнее, в их evaluators.  Остальные случаи не часты.
[14:13:09] <Kakadu> Ура, я понял
[14:16:18] <gds> ну вот, я ж говорил, ничего сложного тут нет.  А приём прикольный, насчёт равенства типов.  Наверняка можно применить и для более сложных отношений.
[14:16:59] <Kakadu> Не, я понял что такое гадты в 4.00, а про равенство типов надо ещё подумать
[14:17:35] <Kakadu> А, уже понял
[14:39:04] tilarids вошёл(а) в комнату
[14:47:27] Typhon вошёл(а) в комнату
[14:51:51] <klapaucius> Как можно понимать что такое GADT и не понимать - что такое равенство типов? Ведь GADT это rank n полиморфизм + равенство типов.
[15:05:08] <Kakadu> klapaucius: я вот не помню уже что такое rank-b полиморфизм
[15:05:16] <Kakadu> И нет, я этим не горжусь!
[15:16:09] Kakadu вышел(а) из комнаты
[15:16:23] Kakadu вошёл(а) в комнату
[15:26:18] <akovbovich> зря я в школе алгебру не учил :(
[15:28:09] Kakadu вышел(а) из комнаты: Replaced by new connection
[15:28:09] Kakadu вошёл(а) в комнату
[15:29:11] <Kakadu> akovbovich: а не поможет школа. Я тоже в универе зря алгебру не лююил. Но даже с тройкой я могу вспомнить что такое группы, кольца и гомомрфизмы
[15:30:24] <akovbovich> да у меня это было во втором или 3ем семестре, и я даже эту штуку сдавал, но блин место зубрежки нифига не помогает сейчас
[15:32:19] <akovbovich> может кто знает, есть в москве очные курсы (годовые например) по матре?
[15:33:17] <Kakadu> Может походить на пары гденить в МГУ? вольным слушателем?
[15:33:53] <akovbovich> а пустят?
[15:34:23] <Kakadu> думаю в СПбГУ можно было бы договориться. МГУ --- хз
[15:35:32] <Kakadu> я вот всё хочу осилить Маклейна. Но одному мне будет не подсилу и скучно, наверное
[15:36:38] <Kakadu> но ёлки-палки, если бы я не сдавал алгебру в универе --- я бы совсем умер
[15:36:57] <Kakadu> а вот матан и геометрия думаю бесполезные будут в большнстве случаев
[15:37:40] <f[x]> Kakadu: подружку заведи, Маклейн на ура пойдёт
[15:38:38] <Kakadu> f[x]: проще уж маклейна дочитать
[15:41:21] komar вышел(а) из комнаты: Replaced by new connection
[15:41:21] komar вошёл(а) в комнату
[15:43:31] tilarids вышел(а) из комнаты: Computer went to sleep
[15:45:50] <Kakadu> а-ля бандинг генератор ещё один: http://130.203.133.150/viewdoc/download;jsessionid=816AC8D2DAD52D9376780BD54024D7F7?doi=10.1.1.187.8759&rep=rep1&type=pdf
[16:14:56] komar вышел(а) из комнаты
[16:18:03] komar вошёл(а) в комнату
[16:34:01] tilarids вошёл(а) в комнату
[16:59:22] <gds> Kakadu: судя по вступлению -- прикольненько, буду читать.
[17:06:48] <Kakadu> gds: учти, что программноё реализации походу нет
[17:07:42] <gds> Kakadu: да тут идеи важнее.  Кроме того, отчего бы благородным донам не повелосипедить.
[17:23:18] Sun][ вошёл(а) в комнату
[17:36:00] Kakadu вышел(а) из комнаты: Replaced by new connection
[17:36:00] Kakadu вошёл(а) в комнату
[17:36:02] <Kakadu> Sun][: а вот и он нарисовался?
[17:37:46] <Kakadu> Sun][: камлом заниматься планируешь?
[17:37:54] <Kakadu> это же такой прекрасный язык растакой
[17:39:09] <Kakadu> вот запили нам генерилку из камля в ecma-script который в QMLe
[17:39:09] Kakadu вышел(а) из комнаты
[17:39:13] Kakadu вошёл(а) в комнату
[17:58:51] Kakadu вышел(а) из комнаты
[17:59:05] Kakadu вошёл(а) в комнату
[18:27:25] komar вышел(а) из комнаты
[18:27:31] komar вошёл(а) в комнату
[18:32:54] komar вышел(а) из комнаты
[18:33:00] komar вошёл(а) в комнату
[18:49:22] komar вышел(а) из комнаты
[18:49:29] komar вошёл(а) в комнату
[19:22:44] ftrvxmtrx вышел(а) из комнаты
[19:29:37] Kakadu вышел(а) из комнаты
[19:30:21] Kakadu вышел(а) из комнаты
[19:56:01] Vinzent вошёл(а) в комнату
[20:19:16] Kakadu вошёл(а) в комнату
[20:21:33] Kakadu вышел(а) из комнаты
[20:21:39] Kakadu вошёл(а) в комнату
[20:30:21] Vinzent вышел(а) из комнаты
[20:31:19] Vinzent вошёл(а) в комнату
[20:31:25] Vinzent вышел(а) из комнаты
[20:35:12] Vinzent вошёл(а) в комнату
[20:37:30] Sun][ вышел(а) из комнаты
[20:50:05] tilarids вышел(а) из комнаты
[20:51:52] ftrvxmtrx вошёл(а) в комнату
[20:53:46] tilarids вошёл(а) в комнату
[20:54:12] letrec вышел(а) из комнаты
[20:54:45] Vinzent вышел(а) из комнаты
[22:14:53] f[x] вошёл(а) в комнату
[22:25:29] tilarids вышел(а) из комнаты
[23:25:58] Typhon вышел(а) из комнаты
[23:31:58] tilarids вошёл(а) в комнату
[23:34:00] bobry вошёл(а) в комнату
[23:35:51] bobry вышел(а) из комнаты
[23:35:56] bobry вошёл(а) в комнату
[23:47:01] tilarids вышел(а) из комнаты: Logged out