Слон и кит

[thedeemon]

Забавная танцевальная битва Idris vs. Scala, где Miles Sabin пытается на Скале воспроизвести пару примеров использования зависимых типов, показанных перед этим на Идрисе:
http://www.infoq.com/presentations/scala-idris (40 минут видео)
Не очень успешно.

Comments

[xeno-by.livejournal.com]

Not enough macro power.

[xeno-by.livejournal.com]

А если серьезно, то мне показалось довольно странным, что Майлс решил один-в-один транслитерировать Идрисовый DSL на Скалу. Было бы интересно подумать, можно ли на Скале сделать что-то похожее по функциональности, используя средства, которые будут работать более удобным образом.

[xeno-by.livejournal.com]

А насчет экстравагантного способа реализации вычислений на типах (который был в презентации в части про векторы, но гораздо лучше иллюстрируется вот тут: http://lanyrd.com/2013/scalax/scrzmm/), то вот тут я уверен, что при помощи макросов можно сделать синтаксис сопоставимым по удобству с, например, type families. Мы с Майлсом хотели рассказать про что-то такое на прошлой неделе на Scala eXchange, но у него не получилось приехать, поэтому начинание пришлось отложить.

[udpn.livejournal.com]

Тю, так в Haskell всегда такое на type classes с undecidable instances делали. Там оно и синтаксисом покрасивее. Я только не понимаю, какое отношение это имеет к зависимым типам, потому что здесь просто два stage, явное отделение вычислений времени компиляции, нет проверки тотальности и всё такое.

[xeno-by.livejournal.com]

А можно пример синтаксиса из Хаскелла, который покрасивее?

К зависимым типам это имеет косвенное, но отношение, т.к. некоторые зависимые вещи (те же вектора) можно неплохо выразить при помощи вычислений на типах во время компиляции.

[udpn.livejournal.com]

http://okmij.org/ftp/Computation/lambda-calc.html
см. "Type-level call-by-value lambda-calculator in three lines"

Найти более развёрнутый пример что-то сходу не смог. Ребе thesz большой любитель такого, спрашивайте его :)

[sassa-nf.livejournal.com]

да в скале не очень получилось выразить даже факт, что Vect n a ++ Vect m a = Vect (n+m) a, т.е. что длина будет именно суммой. В итоге реализовал в конкатенации заодно и сложение.