Новая статья — о простом тайп-левел представлении UUID:
https://ybogomolov.me/type-level-uuid
https://ybogomolov.me/type-level-uuid
ybogomolov.me
Compile-time validation of UUIDs
Заметка об использовании ScalaJS для написания кода под AWS-ный V8 напомнила о проекте, который позволяет нативно запускать хаскельный код в AWS:
https://theam.github.io/aws-lambda-haskell-runtime
https://theam.github.io/aws-lambda-haskell-runtime
theam
AWS λ Runtime - Home
Build fast and solid serverless applications
Forwarded from Lil Functor
Вот и пригодилась компиляция Scala → JavaScript. Только не для фронтенда.
Daniel Spiewak в концепте serverless-фреймворка предлагает компилировать код на Scala в JS, чтобы запускать его на движке V8. Таким образом получится избежать проблемы холодного старта JVM для короткоживущих функций. V8 не надо прогревать, а код для него можно писать всё на той же Scala. Не зря ведь scala.js делали и библиотеки под него кроссбилдили!
Понятно, что scala-native слишком далека от готовности к проду, но интересно, почему решили не использовать Native Image в GraalVM. Решение с js в любом случае оригинальное и может быть из него что-то вырастет.
Сам концепт: https://gist.github.com/djspiewak/37a4ea0d7a5237144ec8b56a76ed080d
Прототип библиотеки: https://github.com/typelevel/feral
Daniel Spiewak в концепте serverless-фреймворка предлагает компилировать код на Scala в JS, чтобы запускать его на движке V8. Таким образом получится избежать проблемы холодного старта JVM для короткоживущих функций. V8 не надо прогревать, а код для него можно писать всё на той же Scala. Не зря ведь scala.js делали и библиотеки под него кроссбилдили!
Понятно, что scala-native слишком далека от готовности к проду, но интересно, почему решили не использовать Native Image в GraalVM. Решение с js в любом случае оригинальное и может быть из него что-то вырастет.
Сам концепт: https://gist.github.com/djspiewak/37a4ea0d7a5237144ec8b56a76ed080d
Прототип библиотеки: https://github.com/typelevel/feral
dd if=/dev/stuff of=/dev/tg
Заметка об использовании ScalaJS для написания кода под AWS-ный V8 напомнила о проекте, который позволяет нативно запускать хаскельный код в AWS: https://theam.github.io/aws-lambda-haskell-runtime
Самое любопытное здесь — табличка с бенчмарками относительно JVM и ноды. Вопросы, конечно остаются — скажем, на код остальных примеров хотелось бы тоже взглянуть, — но значения времени холодного старта и потребления памяти вызывают заинтересованность, как минимум.
Карл фон Госсеринг потратил 76 лет на написание трактата о часах. Об одник конкретных часах — часах-фонаре Николаса Валлина. В ходе написания этот трактата он предвосхитил специальную теорию относительности, поднял вопрос о проблеме останова, и даже построил исчисление для моделирования часовых механизмов.
Насладиться прекрасным тредом:
https://threadreaderapp.com/thread/1467417990744649728.html
Насладиться прекрасным тредом:
https://threadreaderapp.com/thread/1467417990744649728.html
Threadreaderapp
Read and Share Twitter Threads easily!
Thread Reader helps you read and share the best of Twitter Threads
Язык, который привлекает мое внимание в последнее время всё больше и больше — Unison.
Из интересного:
1. наличие как структурной, так и номинальной типизации из коробки благодаря ключевым словам
2. Наличие алгебраических эффектов в виде abilities:
3. Хранение кода в виде AST — что делает кэширование/мемоизацию/рефакторинг/поиск/etc гораздо более простым и мощным, нежели в случае хранения кода в виде текста. Это позволяет делать разные интересные штуки — вроде ускорения сборки кода благодаря закэшированным результатам сборки используемых частей библиотек.
Хороший обзор Unison сделал Рунар Бьярнасон в выступлении на Lambda Jam’21: https://www.youtube.com/watch?v=DF6zt0Q-pz4. Также могу смело порекомендовать отличную статью из их блога о том, как написать распределенную Spark-like структуру данных: https://www.unison-lang.org/articles/distributed-datasets.
Из интересного:
1. наличие как структурной, так и номинальной типизации из коробки благодаря ключевым словам
structural и unique:-- одинаковые типы:
structural type Maybe x = None | Just x
structural type Option x = Nothing | Some x
> Just 5 === Some 5
⧩
true-- разные типы:
unique type Maybe x = None | Just x
unique type Option x = Nothing | Some x> Just 5 === Some 5
The mismatch is because these types differ:
Option
Maybe2. Наличие алгебраических эффектов в виде abilities:
f : '{Gen} Text
f = gen.Text.ascii
g : Text -> '{IO, Exception} ()
g txt = '(printLine txt)
-- abilities в композиции функций являются суммой abilities частей:
f_g : '{Gen, IO, Exception} ()
f_g = '(!(g !f))3. Хранение кода в виде AST — что делает кэширование/мемоизацию/рефакторинг/поиск/etc гораздо более простым и мощным, нежели в случае хранения кода в виде текста. Это позволяет делать разные интересные штуки — вроде ускорения сборки кода благодаря закэшированным результатам сборки используемых частей библиотек.
Хороший обзор Unison сделал Рунар Бьярнасон в выступлении на Lambda Jam’21: https://www.youtube.com/watch?v=DF6zt0Q-pz4. Также могу смело порекомендовать отличную статью из их блога о том, как написать распределенную Spark-like структуру данных: https://www.unison-lang.org/articles/distributed-datasets.
www.unison-lang.org
Unison | A friendly, statically-typed, functional programming language from the future · Unison programming language
A friendly programming language from the future.
Габриель Вольпе написал очень интересный пост о том, как в третьей скале можно обрабатывать ошибки без явного использования Either, используя только типы-суммы:
https://gvolpe.com/blog/error-handling-scala3
https://gvolpe.com/blog/error-handling-scala3
Gvolpe
Scala 3: Error handling in FP land • gvolpe's blog
Table of contents
dd if=/dev/stuff of=/dev/tg
Габриель Вольпе написал очень интересный пост о том, как в третьей скале можно обрабатывать ошибки без явного использования Either, используя только типы-суммы: https://gvolpe.com/blog/error-handling-scala3
А еще показали вот такой экспериментальный набор расширений для exceptions as abilities: https://docs.scala-lang.org/scala3/reference/experimental/canthrow.html
https://dotty.epfl.ch/docs/reference/experimental/cc.html эксперимент по добавлению в Scala 3 capture checking, которые мне напомнили о языке Flix, в котором разделение между чистыми и сайд-эффектящими функциями сделано на уровне синтаксиса.
dd if=/dev/stuff of=/dev/tg
https://dotty.epfl.ch/docs/reference/experimental/cc.html эксперимент по добавлению в Scala 3 capture checking, которые мне напомнили о языке Flix, в котором разделение между чистыми и сайд-эффектящими функциями сделано на уровне синтаксиса.
Чуть было не забыл вбросить ссылку на отличный разбор этой фичи от Олега Нижникова:
https://medium.com/@odomontois/several-days-ago-we-saw-the-new-experimental-feature-called-capture-checking-was-announced-in-e4aa9bc4b3d1
https://medium.com/@odomontois/several-days-ago-we-saw-the-new-experimental-feature-called-capture-checking-was-announced-in-e4aa9bc4b3d1
Medium
About capture checking
in scala 3
Forwarded from PONV Daily (Alex Gryzlov)
https://dlnext.acm.org/doi/abs/10.1145/3498886.3502201 Biri, [2022] "Dependent tagless final"
https://github.com/idris-lang/Idris2/blob/main/libs/papers/Language/Tagless.idr
https://github.com/idris-lang/Idris2/blob/main/libs/papers/Language/Tagless.idr
ACM Conferences
Dependent tagless final | Proceedings of the 2022 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation
Перевел в текстовую форму свой доклад "Making Illegal States Unrepresentable in TypeScript": https://ybogomolov.me/making-illegal-states-unrepresentable
Сам доклад, если кто-то пропустил, можно найти здесь: https://www.youtube.com/watch?v=T7i2wlCqgJk
Сам доклад, если кто-то пропустил, можно найти здесь: https://www.youtube.com/watch?v=T7i2wlCqgJk
ybogomolov.me
Making Illegal States Unrepresentable
Forwarded from AlexTCH
https://proofassistants.stackexchange.com/a/940/333
This answer is golden, it links to all of the best materials on Type Theory and related subjects.
This answer is golden, it links to all of the best materials on Type Theory and related subjects.
Proof Assistants Stack Exchange
So many data types, so little time
I find my mathematics and programming background$^*$ do not endow me with much understanding of type theory as it pertains to proof assistants. To remedy this shortcoming I don't expect a Royal Ro...