Дошли руки до лямбда-куба

[deni_ok]

Поправил в ru-Википедии своё же описание понятия зависимости одного от другого, долгое время меня раздражавшее. Поправил на более аккуратное, основанное на PTS-подходе. Что-то больно формально вышло, но проще уже слишком много профанации. Держите, вобщем. Originally posted at http://deniok.dreamwidth.org/47237.html. Feel free to comment here or

Comments

[nponeccop]

Отлично, на мой наивный взгляд.

Если говорить о статье в целом, то в разделе "поддержка языками программирования" есть профанация: cистемы GHC и ML всё-таки нетривиальным образом связаны с System F, не являясь её консервативными расширениями.

Теряются важные свойства исходной системы, вроде сильной нормализации.

[deni_ok]

Да, про языки программирования стоит кусок поправить, написав более аккуратно про связь одного с другим.

[kodt_rsdn]

Вот бы ещё поподробнее написать, с отличительными примерами, что ли? Поподробнее не в смысле ещё больше формализма.
А то получилась не ознакомительная статья, а "идите гуглить библиотеку академии наук"...
Но, в любом случае, спасибо. Пойду гуглить:-)

[deni_ok]

Там на самом деле все системы интересные и про них много чего стоит сказать. Например, половина TAPL Пирса - про левую грань куба. Надо бы написать статьи про каждую конкретную систему, начиная с простейшей - просто типизированной.
А смысл самого куба - как раз в том, что он даёт единообразный подход.