Спасибо за отзыв. Не вся, но бОльшая часть. Про зависимые

Question

Спасибо за отзыв. Не вся, но бОльшая часть. Про зависимые

типы на чистой скале (без ProvingGround) идет речь в лекциях "Dependent pair type (Σ-type)", "Dependent function type (Π-type)". Про Shapeless я только упоминаю в последней лекции "Type-level programming. Shapeless". Ну и практика на чистой скале "Type-level programming. Part 1: number exponentiation" и "Type-level programming. Part 2: vector concatenation".
Причина - в библиотеке проще объяснять концепцию зависимых типов, чем их кодировать через type level + path-dependent на чистой скале или скале+shapeless, объяснять связь дженериков и type members, "Aux" pattern и т.д. - добавляется еще один уровень косвенности
(ну и еще причина - я помогал искать баги в ProvingGround, так что практика была фактически готова).

Этот курс вводный. Практически по любому из пяти направлений (type theory, HoTT, dependent types, type-level, theorem proving) можно написать отдельный большой курс.
Так что практика получилась не вполне сбалансированная, согласен.

Добавлять в этот курс - пока идет конкурс, вроде бы нельзя. Написать новый - не исключено, посмотрим.

"tips and tricks по реализации DT в Скале" - это Shapeless. Начинать стоит с https://github.com/underscoreio/shapeless-guide
https://www.youtube.com/watch?v=Zt6LjUnOcFQ
https://github.com/milessabin/shapeless/tree/master/examples/src/main/scala/shapeless/examples
https://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/

#programming #russian #scala

0

16.04.2017

1 ответов

17 просмотров

Alexander · Accepted Answer

Спасибо за развёрнутый ответ! В целом мой поинт в том, что изучать DT на Скале не слишком удобно, но посмотреть на интересные трюки с системой типов интересно. Напишу Вам небольшой отзыв после того как весь курс пройду (наверное, будет интересно).

169 похожих чатов

Спасибо за отзыв. Не вся, но бОльшая часть. Про зависимые

1 ответов

Похожие вопросы