deniok: (typed lambda)
 Ян [livejournal.com profile] oxij  написал Жёсткое введение в зависимые типы на Агде. Не могу не пропиарить. Открывайте и изучайте, свиньи вы эдакие (кроме, конечно, девушек) (c) r_l

UPD: обсуждение в Твиттере

deniok: (Default)
В Agda2 композиция двух функций с обобщённым функциональным типом типизируется так
_○_ : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
      (f : {x : A}(y : B x) -> C x y)
      (g : (x : A) -> B x)
      (x : A) -> C x (g x)
(f ○ g) x = f (g x)
Укажите теперь тип для "наиболее общей" композиции трёх таких функций
_○₁_○₂_ : ?
(f ○₁ g ○₂ h) x = f (g (h x))


Комменты не скринятся, читеры подвергаются лёгкой форме остракизма :-)

UPD. Ответившего правильно Анонима подержу немного заскриненным.
deniok: (lambda cube)
Сегодняшние вести с LtU: Certified Programming With Dependent Types
Книжка про COQ, судя по оглавлению весьма полезная. Не пропустите, кто интересуется заявленными темами.
deniok: (typed lambda)
Отталкиваясь от полученной в прошлом посту просьбы, попытаюсь рассказать о Σ-типах.

deniok: (typed lambda)
Для чего нужна Π-абстракция при наличии зависимых типов?

А вот для чего... )

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 25th, 2017 02:52 pm
Powered by Dreamwidth Studios