Вхід і реєстрація
Навчання · 6 квітня 2017, 12:11 5352
Dmytro Mitin, КНУ

Новый бесплатный курс по Scala

Всем привет.
Записал новый курс по Scala.
Introduction to programming with dependent types in Scala
stepik.org/2294 stepik.org/course/49181
Курс бесплатный. Сертификаты планируются. Курс на английском.

This course is an introduction to type theory, homotopy type theory (HoTT), dependent-type programming, type-level programming, and theorem proving using Scala.

It consists of video lectures (more than 8 hours of video), presentations (more than 130 slides), and more than 50 programming exercises (some in pure Scala — to be tested online on Stepik’s servers, and some in Scala + ProvingGround library from Github — to be performed in local computer and tested online).

The course is adaptive: student can press button “Continue” and system will try to recommend next exercise for this student.

The course is for people who are interested in functional programming (Scala, Haskell), programming with dependent types (Idris), type-level programming (Shapeless).

Теми: Scala, курси
👍ПодобаєтьсяСподобалось0
До обраногоВ обраному1
LinkedIn
Дозволені теги: blockquote, a, pre, code, ul, ol, li, b, i, del.
Ctrl + Enter
Дозволені теги: blockquote, a, pre, code, ul, ol, li, b, i, del.
Ctrl + Enter
Dmytro Mitin Працює в КНУ 17.02.2020 13:09

Буду проводить оффлайновый тренинг по Shapeless 29 февраля 2020 г. в Киеве. dou.ua/calendar/31318

Відповісти
Підтримати
Dmytro Mitin Працює в КНУ 02.11.2018 15:09

Начал апдейтить свой курс «Introduction to programming with dependent types in Scala» на Степике: stepik.org/course/49181
Пока что готов первый урок о булевом типе: stepik.org/...​186371/step/1?unit=160906
По сравнению со старой версией почистил звук, немного отредактировал видео и заменил практику на проверяемую auto-grader’ом. Раньше надо было ставить софт локально и вывод проги отправлять на Степик как стрингу, сейчас можно просто писать код онлайн и он будет компилироваться/запускаться на сервере, так что надеюсь, что теперь практикой будет пользоваться удобнее.

Відповісти
Підтримати
vlodko 24.05.2017 08:08

Теоремы доказывать собираетесь?

Відповісти
Підтримати
Grez 09.04.2017 19:59
dependent types in Scala
фигасе, надо брать.
Відповісти
Підтримати
Namdak Tonpa 09.04.2017 18:34
homotopy type theory (HoTT),
Scala
Хочу посмотреть формальное определение конструкции Хопфа окружности в скале и ее рекурсора. Или ты показываешь или признаешь, что немного натянул козу на баян и меняешь текст в описании убирая оттуда HoTT.

Люди всем академическим сообществом Coq пропатчили, чтобы это было возможно, т.е. даже в самом современном прувере современности — это не работает из коробки. А тут так просто, берем скалу и HoTT. Нехорошо обманывать людей. Помни о славе Ивана Головача!

Я бы и на завтипы набросил, сказав, что скала не для этого, но пожалею тебя, из-за того, что ты защищался в НАН Украины.

Відповісти
Підтримати
Dmytro Mitin Працює в КНУ 10.04.2017 00:41

Ура. Топик начал опускаться, но пришел ты и его бампнул.

Хочу посмотреть формальное определение окружности в скале и ее рекурсор
По-видимому, надо начинать, как здесь:
@ val Circle = "S" :: Type  Circle: Typ[Term] with Subs[Typ[Term]] = S : 𝒰 _0 @   val base = "base" :: Circle  base: Term with Subs[Term] = base : (S : 𝒰 _0) @   val loop = "loop" :: (base =:= base)  loop: Term with Subs[Term] = loop : (base : (S : 𝒰 _0) = base : (S : 𝒰 _0)) @   val X = "X" :: Type  X: Typ[Term] with Subs[Typ[Term]] = X : 𝒰 _0 @   val a = "a" :: X  a: Term with Subs[Term] = a : (X : 𝒰 _0) @   val l = "l" :: (a =:= a)  l: Term with Subs[Term] = l : (a : (X : 𝒰 _0) = a : (X : 𝒰 _0)) @   val recS = "rec_S" :: X ~>: (a ~>: (l ~>: (Circle ->: X)))  recS: FuncLike[Typ[Term] with Subs[Typ[Term]], FuncLike[Term with Subs[Term], FuncLike[Term with Subs[Term], Func[Term, Term]]]] with Subs[FuncLike[Typ[Term] with Subs[Typ[Term]], FuncLike[Term with Subs[Term], FuncLike[Term with Subs[Term], Func[Term, Term]]]]] = rec_S : (X : 𝒰 _0 ~> a : (X : 𝒰 _0) ~> l : (a : (X : 𝒰 _0) = a : (X : 𝒰 _0)) ~> (S : 𝒰 _0) → (X : 𝒰 _0))
даже в самом современном прувере современности — это не работает из коробки
Так никто и не сравнивает что-то с Coq.

Да, в курсе нет рекурсора окружности. Так и в первой главе HoTT Book его тоже нет. Если не годится название «introduction to ...», пусть будет «introduction to introduction to ...»
В курсе есть сигма- и пи-тип, identity-тип и «махание руками» на тему связи зависимых типов с расслоениями. А вообще на первой странице курса есть полное перечисление тем, так что ни у кого не должно быть недопонимания, что есть в курсе, а чего нет.
Чувакам на реддите не хватает побольше shapeless, тебе не хватает побольше высших индуктивных типов.

Или ты показываешь или признаешь...
Нехорошо обманывать людей. Помни о славе Ивана Головача!
...но пожалею тебя...
Давай-ка ты, Максимка, сбросишь обороты.
Ты знаешь, что такое расслоение Хопфа? Молодец. Запиши свой курс (если захочешь), мы будем просвещаться. И будут этот курс на скале, другой курс на Идрисе, твой курс на Coq и т.д.
Довольно глупо сравнивать бесплатный курс с платным, анонсированным и недопроведенным.
И ты мне вроде ничего не платил, чтобы от меня что-то требовать.
Кстати, раз уж ты начал мне мораль читать, кажется, это за тобой, а не за мной водится слава кидателя математиков.
Відповісти
Підтримати
Namdak Tonpa
Namdak Tonpa 10.04.2017 06:06

Код твой и с форматированием и без — - - говно на скале.

Відповісти
Підтримати
Dmytro Mitin
Namdak Tonpa 10.04.2017 06:06

Если ты напишешь мне в чем я кинул Пашу я возьму свои слова обратно. Вижу что не зря на тебя наехал. Не люблю когда не знают, не могут доказать и дофига машут рукамт у доски.

Відповісти
Підтримати
Dmytro Mitin
My Profile software engineer 08.04.2017 00:34

-

Yaroslav Zeygerman C/C++ Developer в CyberVision 07.04.2017 22:41

Спасибо огромное за отличную работу. Топик — то что надо.

Відповісти
Підтримати
Roman Gorodishcher Principal Engineer в Twilio 07.04.2017 21:37

Что-то на Степике с авторизацией проблема. А так круто, хоть и не применимо.

Відповісти
Підтримати
Dmytro Mitin Працює в КНУ 07.04.2017 22:05

Днем недолгое время выдавал 503 vk.com/…​099769_32900966?post=1309
Сейчас вроде работает (включая логин, логинюсь через фейсбук). В случае проблем можно там спрашивать.

Все более применимое начинается сначала с менее применимого)

Відповісти
Підтримати
Roman Gorodishcher
Alexander Mukhopad Software Engineer 06.04.2017 12:32

Если что, Мартин Одерски на курсере давно записал бесплатный курс по скале)

Відповісти
Підтримати
Dmytro Mitin Працює в КНУ 06.04.2017 12:42

А по Idris есть курс у Виталия Брагилевского compsciclub.ru/…​sprogramming/2017-spring
Идея была в том, чтобы написать что-то вводное по Скале и зависимым типам.

Відповісти
Підтримати
Alexander Mukhopad
Нестор Иванович 07.04.2017 04:47

который идет раз в сто лет, и упомянутые темы вообще не раскрывает

Відповісти
Підтримати
Alexander Mukhopad
Alex Koshterek погромизд 10.04.2017 10:51

хз, видел только платные от него же

Відповісти
Підтримати
Alexander Mukhopad

Підписатись на коментарі

Не підписуватись
Скористайтесь акаунтом
×
з умовами використання сайту і політикою конфіденційності.