?

Log in

No account? Create an account
Зависимые типы и high kind types. - Программирование с зависимыми типами [entries|archive|friends|userinfo]
Программирование с зависимыми типами

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Зависимые типы и high kind types. [Oct. 27th, 2017|11:55 am]
Программирование с зависимыми типами

ru_deptypes

[potan]
[Tags|]

Есть вполне полезные языки, не поддерживаюшие HKT - Rust, Elm. Возможно ли (и осмысленно) в подобных языках делать поддержку зависимых типов? Например, Elm справедливо требует тотальности кода, но из-за этого приходится описывать и обрабатывать невозможные ситуации, например когда пользователь еще не залогинился, а уже разлогинивается. Зависимые типы позволяют описать невозможность такого события.
LinkReply

Comments:
[User Picture]From: kouzdra
2017-10-27 09:24 am (UTC)
у меня последнее время есть подозрение, что для этих нужд хоаровская логика и проще и адекватнее
(Reply) (Thread)
[User Picture]From: thesz
2017-10-27 12:12 pm (UTC)
Ты simpler, easier читал ли?

http://augustss.blogspot.ru/2007/10/simpler-easier-in-recent-paper-simply.html

Ты можешь довольно много сделать, подняв в типы значения. HKT (которые, по сути, замыкания типов) не так, чтобы и нужны.

Но вывод типов у тебя ещё сильнее ухудшится.
(Reply) (Thread)
[User Picture]From: potan
2017-10-27 02:27 pm (UTC)
Не читал еще, оно не по русски.

Спасибо, мне тоже так казалось, теперь почти уверен. Вывод типов не критичен, все равно с зависимыми типами их лучше указывать явно.
(Reply) (Parent) (Thread)
[User Picture]From: maxim
2017-10-28 09:32 pm (UTC)
Поддержку зависимых типов можно добавлять в любые языки и тайпчекнуть все это не так уж и сложно. Можно даже в паскаль добавить квантор всеобщности и CoC типизацию в тайпчекер и получить язык не хуже современных пруверов (мне бы такой язык импониировал, вряд ли я бы такое создавал или на таком писал, конечно).

Другое дело, что добавив квантор всеобнощности как типовой примитив мы ввязываемся в очень неприятную игру с типизацией. Современные элабораторы (или инфереры, котороые выводят тип, одна из стрелок бидирекшинал тайпчекинга) элиминируют только написание некоторых компонент { A: U } и то не всегда получается это контролировать (Практики завтипов вспомнят Arguments X { E } _ _ _ _ в Coq, которые связаны как раз с этой проблемой). Поэтому в последнее время ходит мысль вообще не использовать продвинутые элабоораторы, так как они скорее мешают в процессе поиска пруфтермов чем помогают). Удобство или элиминация кванторов должны находится в плоскости подключении SMT солверов (HOL, F*, Liquid Haskell) а не в области тайпчекера. [Z3, который все они используют, кстати, написал автор нового гомотопического прувера Lean (С++).]

Покажу на примере, и каждый программист пусть сам решит, нужны ему завтипы на производстве или нет. Например вы на Haskell или PureScript пишете:

zygo g f = snd . cata (\x -> (g $ fmap fst x, f x))

А на завтипах вы должны уже будете написать:

zygo (A B: U) (F: U -> U) (g: F A -> A) (alg: F (tuple A B) -> B) (f: fix F): B
= snd A B (cata (tuple A B) F (\(x: F (tuple A B))
-> pair (g (fmap (tuple A B) A F (\(y: tuple A B) -> fst A B y) x)) (alg x)) f)

Готовы вы к такому у себя на производстве? Если да, то доброо пожаловать в количью нору :-)

P.S. В Раст если добавить Пи, то никто и не заметит, уж более анноттированого языка уж и не придумаешь. Мне кажется в Раст даже больше анотаций чем в джаве и скале.

Edited at 2017-10-28 09:38 pm (UTC)
(Reply) (Thread)