×Закрыть

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

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

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).

Допустимые теги: blockquote, a, pre, code, ul, ol, li, b, i, del.
Ctrl + Enter
Допустимые теги: blockquote, a, pre, code, ul, ol, li, b, i, del.
Ctrl + Enter

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

Мой пост на Хабре: habrahabr.ru/post/329176

dependent types in Scala
фигасе, надо брать.
homotopy type theory (HoTT),
Scala
Хочу посмотреть формальное определение конструкции Хопфа окружности в скале и ее рекурсора. Или ты показываешь или признаешь, что немного натянул козу на баян и меняешь текст в описании убирая оттуда HoTT.

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

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

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

Хочу посмотреть формальное определение окружности в скале и ее рекурсор
По-видимому, надо начинать, как здесь:
@ 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 и т.д.
Довольно глупо сравнивать бесплатный курс с платным, анонсированным и недопроведенным.
И ты мне вроде ничего не платил, чтобы от меня что-то требовать.
Кстати, раз уж ты начал мне мораль читать, кажется, это за тобой, а не за мной водится слава кидателя математиков.

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

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

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

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

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

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

отлично, спасибо!

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

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

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

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

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