@DmytroMitin здравствуйте, Дмитрий! Вчера посмотрел часть вашего курса https://stepik.org/course/ThCS-Introduction-to-programming-with-dependent-types-in-Scala-2294 Насколько я

Question

@DmytroMitin здравствуйте, Дмитрий! Вчера посмотрел часть вашего курса https://stepik.org/course/ThCS-Introduction-to-programming-with-dependent-types-in-Scala-2294 Насколько я

понял, вся практика базируется на ProvingGround, что меня сильно смутило. Честно сказать, ожидал больше tips and tricks по реализации DT в Скале. Планируете ли вы такое добавить в свой курс со временем, или, может быть, сделать отдельный?

#programming #russian #scala

0

16.04.2017

1 ответов

9 просмотров

Dmytro Mitin · Accepted Answer

Спасибо за отзыв. Не вся, но бОльшая часть. Про зависимые типы на чистой скале (без 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/

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

@DmytroMitin здравствуйте, Дмитрий! Вчера посмотрел часть вашего курса https://stepik.org/course/ThCS-Introduction-to-programming-with-dependent-types-in-Scala-2294 Насколько я

1 ответов

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