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

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

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

1 ответов

8 просмотров

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

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

Обсуждают сегодня

@Aiwan что такое база образца?
Alexey
27
Не многие знают, а кто знает, тот уже успел забыть, что в далёком 2004 году эта игра произвела настоящий фурор, настолько революционной была технология, применяемая для её соз...
ICCID
4
коллеги, добрый вечер! А никто не знает как модальная форма может себя закрыть? Ну допустим модальная форма определила, что смысла ей работать нет и хочет вернуть modalResult...
Михаил
83
Короче я тут узнал полный пиздец Что кучу постов которые я создавал через posted Спустя время не могу редактировать и менять Мол телега возвращае ошибку Это реально так ...
inc.
13
Хотя у меня сейчас есть более сложная задача, вот её думаю: как объяснить челу переходного возраста противоположного полу, обучающегося в польском колледже (а-ля наш техникум)...
Вячеслав Кузьменко
15
а сколько всего в IT умерло? Где флеш-игры, их было туча, где они все? Сегодня технология есть, а завтра вжух и мёртвая. Этот wasm сильно напоминает джавовские апплеты, silver...
Constantin F.
5
Добрый день Хочу начать обучение языку, не являюсь представителем it, буду благодарна за помощь, совсем пока не понимаю ничего) Подскажите, пожалуйста, где можно начать первы...
Sara Lala
30
а вы в курсе, что Initialize() не работает? var arr123: array[0..123] of Byte; ... Initialize(arr123, SizeOf(arr123));
Iluha Companets
8
что читать по делфи?вообще 0 в нем
fd dsds
9
верно что я могу удалить эти addq и subq т.к. со стеком никакого взаимодействия нет (исключая call)?
Michael
16
Карта сайта