Лямбда-куб, статья в русской Википедии

[deniok]

Каждый должен посадить дерево, построить дом, воспитать ребенка и написать статью в Википедии.

Критикуйте, если что не так, а ещё лучше правьте прямо там.

Comments

[lomeo.livejournal.com]

Почему вы думаете, что kind - это не тип??

[migmit.vox.com (from livejournal.com)]

Гм. Видимо, потому же, почему тип - не значение.

[lomeo.livejournal.com]

Надо мне всё таки найти где я видел такие простые определения. Хорошо, тогда так. У типа тип - kind, а у kind-а?

[migmit.vox.com (from livejournal.com)]

У типа нет типа. Тип есть только у значений. Выражение "кайнд - тип типа" является метафорой, удобной для запоминания, но не более.

> У типа тип - kind, а у kind-а?

А выше по лестнице пока не ходили. Может быть, и стоит. Но, скажем, пока не появились HOT, кайнды тоже были никому не нужны.

[lomeo.livejournal.com]

В Ωмеге они называются сорта (видимо, из PTS).

Не знаю, почему я решил, что kind - это типы (я и сейчас продолжаю так думать). Я нигде про это не читал явно, но видел T::T где то точно. Причём картина получается достаточно стройной. Ведь они ничем не отличаются. kind-ы можно именовать, у них есть значения (типы), над ними применимы абстракция и аппликация, как и над типами и значениями и т.д.

kind Nat = Z | S Nat

и т.д.

Найду - отпишусь, пока закончим, наверное.

[deni-ok.livejournal.com]

Вот, кстати
http://deni-ok.livejournal.com/15168.html
см. первый коммент

[lomeo.livejournal.com]

Да, это само собой. Я просто не хотел называть kind-ы типами второго (N-го) уровня, чтобы ещё и терминологического спора не вышло.