Весь lambda cube в одном флаконе

[deniok]

Нашел ссылку на блестящий пост Lennart Augustsson в его блоге о зависимых типах и не только.

Спасибо asviraspossible.

Comments

[kurilka.livejournal.com]

Можно чувак задвинул :)
А почему несмотря на дублирование в System F в GHC используется именно она?
Лямбда куб делает компиляцию труднее/дольше?
И ещё дурацкий вопрос - а почему в кайндах (как кстати по-русски?) звёздочка используется, откуда термин? Насколько я уяснил эт что-то типа "типа типов"? А что тогда за странные записи я видел типа *->*, одинаковые кайнды различать нам не надо?

[deni-ok.livejournal.com]

Я сам пост внимательно не успел прочитать. Но в других системах есть свои подводные камни, да и потом язык вышел бы не Хаскелл, а совсем другой.

Про кайнды (я их, вроде, перевёл как "виды" в gentile intro).
Это арность конструкторов типов (не данных!) - то есть кол-во типовых параметров, которые мы передаём в тип:

data Int -- kind *
data List a -- kind * -> *
data Either a b -- kind * -> * -> *

Ну и, скажем, class Monad m требует, чтобы тип m имел kind * -> *.

[kurilka.livejournal.com]

О как...
Значит я чтот недопонял, спасибо :)
А есть что-то когда в этих видах один из аргумента конструктора будет зависеть от другого? Или это ересь и тогда надо делать 1 аргумент конструктора?
(просто тут на яве есть на генериках есть в коде одно решение, где есть тип ИД компонента и тип самого компонента, а контейнер этих компонентов имеет параметром оба предыдущих типа, ну и ясное дело что они должны соответствовать друг другу)
А KArrow получается такой "стрелкой из стрелок в стрелки"?
Или -> в видах это ни разу не стрелки?
Как-то пока с натягиванием ТК на хаскель у меня не совсем хорошо :)

[deni-ok.livejournal.com]

Я похоже тебя запутал - убегал утром и спешил ответить.

Kinds - это действительно типы над типами. Просто конструкторы типов - штука очень простая - это то, что стоит слева в определении типа и имеет вид:

data Имя_типа полиморфный_типовый_парам1 ... полиморфный_типовый_парамN = ...

например:

data List a     = Nil | Cons a (List a)
data Either a b = Left a | Right b	

Все зависимости, задающие алгебраическую структуру типа (конструкторы данных) находятся справа от равенства. Так что kindы напрямую программисту не нужны (кое-где в GADT полезно их указывать). Они элементарно выводятся тайпчекером.

И стрелки в * -> * -> * - это не стрелки функций над данными, а стрелки функций над типами. То есть

Prelude> :kind Either
Either :: * -> * -> *

означает, что, чтобы получить замкнутый тип Either, мы должны передать туда 2 типовых параметра:

Prelude> :kind Either Int
Either Int :: * -> *
Prelude> :kind Either Int Bool
Either Int Bool :: *

[kurilka.livejournal.com]

Только вот одного не пойму - почему там есть лишь один исходный тип типов звёздочка?
Примера вида подобного (чтоб были зависимости между входными и выходными типами) правда я чтот привести не могу.

[deni-ok.livejournal.com]

А на уровне конструктора типов у нас есть только одна операция - аппликация. Ничего сложнее чем

data T a b c d e f g = ...

не выйдет. То есть звёздочки достаточно.

Правда для GADT при явной кайндизации можно наворотить что-нибудь типа

data Foo :: * -> (* -> *) -> *  where
 Bar :: a b -> c b -> Foo (a b) c

но выше группировок * всё равно не прыгнешь

[kurilka.livejournal.com]

Ну да, видимо "типы типов типов" это уже перебор, а многоэтажные генерики да шаблоны - заморочки языков, в которых они используются.