Есть research plugins для nightly версий компилятора dotty.epfl.ch/...res/compiler-plugins.html
Буду проводить оффлайновый тренинг по Shapeless 29 февраля 2020 г. в Киеве. dou.ua/calendar/31318
Те, що Shapeless зникне з появою Scala 3 — занадто сильне припущення :)
Shapeless — це не тільки deriving тайпкласів, це ще й купа написаних тайпкласів для роботи з HList’ами, Poly тощо (тобто не тільки для дерайвінга тайпкласів для типів даних, але й трансформації типів даних). Чому вони мають зникнути? Можливо, їх частково перенесуть в стандартну бібліотеку, але повністю — малоймовірно. Наразі бранч Shapeless для Скали 3 активно розробляється
github.com/...hapeless/tree/shapeless-3
github.com/...-build/community-projects
Если же параметров одного типа на место одного неявного параметра претендует больше одного, это вызывает ошибку компиляции diverging implicit expansion.
«diverging implicit expansion» — это другая ошибка. Когда подходит больше одного имплисита, то это ошибка «ambiguous implicit values».
Начал апдейтить свой курс «Introduction to programming with dependent types in Scala» на Степике: stepik.org/course/49181
Пока что готов первый урок о булевом типе: stepik.org/...186371/step/1?unit=160906
По сравнению со старой версией почистил звук, немного отредактировал видео и заменил практику на проверяемую auto-grader’ом. Раньше надо было ставить софт локально и вывод проги отправлять на Степик как стрингу, сейчас можно просто писать код онлайн и он будет компилироваться/запускаться на сервере, так что надеюсь, что теперь практикой будет пользоваться удобнее.
Мой пост на Хабре: habrahabr.ru/post/329176
Специализация платная www.coursera.org/specializations/scala
а курсы вроде бесплатные (включая практику)
www.coursera.org/learn/progfun1
www.coursera.org/learn/progfun2
www.coursera.org/learn/parprog1
www.coursera.org/…earn/scala-spark-big-data
Ура. Топик начал опускаться, но пришел ты и его бампнул.
Хочу посмотреть формальное определение окружности в скале и ее рекурсорПо-видимому, надо начинать, как здесь:
@ 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, тебе не хватает побольше высших индуктивных типов.
Или ты показываешь или признаешь...Давай-ка ты, Максимка, сбросишь обороты.
Нехорошо обманывать людей. Помни о славе Ивана Головача!
...но пожалею тебя...
Днем недолгое время выдавал 503 vk.com/…099769_32900966?post=1309
Сейчас вроде работает (включая логин, логинюсь через фейсбук). В случае проблем можно там спрашивать.
Все более применимое начинается сначала с менее применимого)
А по Idris есть курс у Виталия Брагилевского compsciclub.ru/…sprogramming/2017-spring
Идея была в том, чтобы написать что-то вводное по Скале и зависимым типам.
Привет. Планируется ли выкладывать видео с курса «Машинное обучение (R и Spark)»? Спасибо.
В тему.