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

[deniok]

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

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

Comments

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

В type families, например

Когда объявляется что-нибудь вроде (сорри, могу спутать синтаксис)

class C a where type T a
instance C Int where type T Int = String

То это расшифровывается как

T :: * -> *
axiom CTInt :: T Int ~ String

Здесь T Int ~ String - это кайнд, а CTInt (имя уж наверняка неправильно указал) - тип, относящийся к этому кайнду.

[lomeo.livejournal.com]

Для меня это что-то вроде

type family T a
class C a where ... :: T a -- зависит от T a

type instance T Int = String
instance C Int where ... :: T Int ~ String

и тогда T Int ~ String - это просто тип от GADT, а не kind.

[lomeo.livejournal.com]

"Тип от GADT" - имеется в виду тип одного из конструкторов данных GADT.

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

Почитай, как устроена система типов в новом ghc. Где-то в статьях Пейтон-Джонса это было, как всегда. Примерно так, как я и сказал.

[lomeo.livejournal.com]

Ага, обязательно почитаю, спасибо!

[lomeo.livejournal.com]

Type Checking with Open Type Functions - оно?

[deni-ok.livejournal.com]

Не, по-моему не то. System F with Type Equality Coercions

http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/fc-tldi.pdf

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

Ага, кажется, оно самое.

[lomeo.livejournal.com]

Спасибо!

[deni-ok.livejournal.com]

Да, точно, чего-то такое я читал в статье. Надо будет еще раз глянуть.