deniok: (typed lambda)
deniok ([personal profile] deniok) wrote2013-01-26 08:11 pm
  • Add Memory
  • Share This Entry
Entry tags:

Система F

Обогатил ру-Википедию стать ей про это дело. Ловите. Надо бы ещё, конечно, понаписать про точное определение и всякие свойства, но пока лень.

UPD: Понаписал про формальности.

UPD2: Добавил типизацию по Карри с классическим примером, демонстрирующим, что System F богаче просто-типа-лямбды. И готовящим читателя к рассуждениям про импредикативность и ограниченные версии System F.

UPD3: Уф. Доделал-таки.

Flat | Top-Level Comments Only

[identity profile] nponeccop.livejournal.com 2013-01-26 05:05 pm (UTC)(link)
Из свойств нужно как минимум ранг и предикативность.

[identity profile] deni-ok.livejournal.com 2013-01-26 05:42 pm (UTC)(link)
Да, тут вообще много чего нужно. Сейчас доделаю технические формальности, а про свойства надо на свежую голову.

[identity profile] nponeccop.livejournal.com 2013-01-28 07:58 am (UTC)(link)
http://maxim.livejournal.com/394327.html?thread=2231639&style=mine#t2231639

Вот кстати живая иллюстрация того, почему я хотел именно ранг и предикативность: они нужны всем, а не только тем, кто не имеет общего представления об Ф-системе и случайно зашёл.

[identity profile] deni-ok.livejournal.com 2013-01-28 11:59 am (UTC)(link)
Ну я чего-то понаписал, но, по-моему, ранг и предикативность больше подходят статье <<Параметрический полиморфизм>>, которую кто бы перевёл с довольно приличной английской
http://en.wikipedia.org/wiki/Parametric_polymorphism

[identity profile] kodt-rsdn.livejournal.com 2013-01-26 07:26 pm (UTC)(link)
Мнэээ. Не вчитываясь, просто сравнил объём с объёмом статьи на английском языке. Удручающе :(

[identity profile] deni-ok.livejournal.com 2013-01-26 07:27 pm (UTC)(link)
а теперь как? (на самом деле французская лучше:)

[identity profile] kodt-rsdn.livejournal.com 2013-01-26 07:32 pm (UTC)(link)
Что-то я великой разницы между несколькими минутами назад и сейчас не заметил.
Или ты что имел в виду под "теперь как"? Инглиш и франсэ существенно богаче русской. Либо ты случайно грохнул свою свежайшую правку?

[identity profile] deni-ok.livejournal.com 2013-01-26 07:40 pm (UTC)(link)
Я не грохал, это у тебя, небось, из кэша.

[identity profile] kodt-rsdn.livejournal.com 2013-01-26 07:50 pm (UTC)(link)
Хм, действительно! Залез в редактирование - там свежее и полновесное.
Только почему-то я не могу сбросить кэш.
Что за фигня? Может, это мегафон у себя кэширует и мне старьё отдаёт.

...

О чудо! А вот теперь и кэш сбросился! СПАСИБО!

[identity profile] nivanych.livejournal.com 2013-01-27 03:39 am (UTC)(link)
Надо его по-русски называть "Фсистема"!

[identity profile] kodt-rsdn.livejournal.com 2013-01-27 07:43 am (UTC)(link)
Это наше Фсё!
Flat | Top-Level Comments Only