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

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

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

1 ответов

9 просмотров

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

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

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

Всем привет, написал код ниже, но он выдает сегфолт, в чем причина? #include <stdio.h> #include <stdlib.h> #include <string.h> struct product { char *name; float price; };...
buzz базз
70
Всем доброго дня, ребят подскажите пожалуйста, если в курсе по ассемблеру используется MASM32, могу ли я использовать FASM? В чем явная разница и будет ли у меня все работать?
Botsman
17
Хотел бы спросить у знающих, правильную ли я выбрал книгу для начала изучения ассемблера Юрова В.И ? Или есть более лучшие книги для начала обучения?
Botsman
25
Книга Юрова В.И пойдёт для обучения?
Botsman
24
$params = [ 'formid' => 'feedbackForm', 'formTpl' => '@CODE: <form class="form-validate" data-id="ajax_form"> <fieldset class="margin-bottom-md"> ...
Pathologic
1
Люди добрые, помогите с идеями, потому что свои закончились. У клиента падает софтина в момент инициализации модуля OtlEventMonitor на RegisterWindowMessage('Gp/OtlTaskEvents/...
Михаил Усков
7
> Примечательно, что новый владелец удаляет из GitHub любые жалобы, указывающие на подозрительную активность или смену владельца, и, видимо, рассчитывает на то, что пользовате...
Alex Sherbakov
2
GridView fully ignored first parent(SizedBox), and take width from second parent(Container). How can I constrain GridView by first parent? Widget build(BuildContext context) {...
Hamster
1
Коллеги, добрый день. Есть такой вопрос: Есть модуль, который надо запустить через супервизор как дочерний процесс. Пока инстансов было нужно 8, всё было окей, но когда их ст...
Δημήτηρ
4
Hey there Which is the best Linux destro for developers (coding)? To my research on reddit, they said Linux mint is good for mid level spec and Ubuntu for high Lev hardwar...
Wiz 🪄
11
Карта сайта