?

Log in

No account? Create an account

Why not be dependently typed? - Excelsior

Jun. 25th, 2013

12:01 am - Why not be dependently typed?

Previous Entry Share Next Entry

МакБрайд про зависимые типы в Хаскелле: http://stackoverflow.com/questions/12961651/why-not-be-dependently-typed/13241158#13241158 + свежая папера его же на ту же тему: http://www.reddit.com/r/haskell/comments/1gz03w/hasochism_the_pleasure_and_pain_of_dependently/.

Еще понравилась цитата: "Dependent types make a lot of people nervous. They make me nervous, but I like being nervous, or at least I find it hard not to be nervous anyway" :)

Comments:

From:ex_juan_gan
Date:June 24th, 2013 10:50 pm (UTC)
(Link)
Wow. Не то чтобы я всё понял... но понял главное... time to move on.
(Reply) (Thread)
[User Picture]
From:xeno_by
Date:June 24th, 2013 10:58 pm (UTC)
(Link)
Мне работу было очень тяжело читать, поэтому я на пока что отложил, но к счастью вспомнил про этот ответ на SO, который я читал вчера. А на stack overflow МайБрайд, как оказалось, довольно доступно объяснил базовые вещи, которые, как я понял, легли в основу работы.
(Reply) (Parent) (Thread)
[User Picture]
From:xeno_by
Date:June 24th, 2013 11:01 pm (UTC)
(Link)
Еще вот на StrangeLoop будет совместный доклад Майлса и Эдвина Брэди. Жду с нетерпением! Надо прошариваться в зависимых типах, это точно.
(Reply) (Parent) (Thread)
From:ex_juan_gan
Date:June 24th, 2013 11:25 pm (UTC)
(Link)
Да... я как-то неудачно пролетел со стрейджлупом.
(Reply) (Parent) (Thread)
[User Picture]
From:thedeemon
Date:June 25th, 2013 08:57 am (UTC)
(Link)
У Бреди есть небольшой видеокурс, на базе его Идриса:
http://idris-lang.org/archives/253
(Reply) (Parent) (Thread)
[User Picture]
From:nponeccop
Date:June 25th, 2013 09:44 am (UTC)
(Link)
а) В Х-е понимание Хиндли-Милнера дает возможность писать простейшие программы. Нужна аналогичная базовая система для сокращения порога входа. Я пока нашёл www.andres-loeh.de/PiSigma/PiSigma.pdf . Мне нравится, например, как их сигма-типы унифицированно описывают и независимые суммы, и независимые произведения.

б) Нужно больше реализаций или одна, но зрелая и с человеческим лицом. У ATS и Coq это лицо недостаточно хорошее. Агда мне нравится как язык, но не нравится идеей установки в систему гигабайт говна, когда для того, чтобы пощупать язык, достаточно только agda.exe, стандартной библиотеки и десятка примеров. Это весьма отпугивает щупающих, учитывая что уровень развития сообщества не позволяет пока сделать это говно качественным. В результате приходится бороться с глюками в установщике емакса и потом учиться пользоваться емаксом. За это время вполне можно отчаяться и плюнуть. В то время, как можно было поставить компилятор и в ноутпаде проходить туториал.

Coq в этом плане производит очень хорошее впечатление, но он мне не нравится как язык. ATS и Idris Unix-only.

Edited at 2013-06-25 09:54 am (UTC)
(Reply) (Thread)
[User Picture]
From:thedeemon
Date:June 25th, 2013 10:29 am (UTC)
(Link)
Idris у меня нормально в винде живет, с Haskell Platform и MinGW.
(Reply) (Parent) (Thread)
[User Picture]
From:dmytrish
Date:June 25th, 2013 06:05 pm (UTC)
(Link)
Немного оффтоп, но интересно: ленивости-by-default в Idris не хватает, или наоборот, ее отсутствие — плюшка?
(Reply) (Parent) (Thread)
[User Picture]
From:thedeemon
Date:June 26th, 2013 02:14 am (UTC)
(Link)
Немножко не хватает, я в связи с этим сейчас собрался сделать библиотечку ленивых энумераторов (по мотивам range'й из D). Но чаще всего пофиг, т.к. когда программа тотальная, ее результат от ленивости не зависит.
(Reply) (Parent) (Thread)