Channel: dd if=/dev/stuff of=/dev/tg
Язык, который привлекает мое внимание в последнее время всё больше и больше — 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
Maybe
2. Наличие алгебраических эффектов в виде 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...
В эту пятницу я буду участвовать в небольшом ивенте «TypeScript. Твой код в опасности» от коммьюнити Vue.js:
https://wearecommunity.io/events/typescript-tvoi-kod-v-opasnosti
Поговорим на тему того, насколько тайпскрипт как язык может гарантировать безопасность исполняемого кода, затронем извечную холиварную в мире JS тему «типы vs. тесты», обсудим различные подводные камни той или иной позиции. Приходите, будет интересно 🙂
https://wearecommunity.io/events/typescript-tvoi-kod-v-opasnosti
Поговорим на тему того, насколько тайпскрипт как язык может гарантировать безопасность исполняемого кода, затронем извечную холиварную в мире JS тему «типы vs. тесты», обсудим различные подводные камни той или иной позиции. Приходите, будет интересно 🙂
wearecommunity.io
TypeScript. Твой код в опасности | Community platform
TypeScript. Твой код в опасности. "July 1, 2022" | Community platform | Register for the event and learn more on the main communities platform.
Новая версия ресурса для изучения прувера TLA+: https://www.learntla.com
Пост автора о мотивации создания второй версии: https://www.hillelwayne.com/post/learntla
Пост автора о мотивации создания второй версии: https://www.hillelwayne.com/post/learntla
Немного новостей.
1. Я наконец-то навсегда покинул Россию вместе с семьей. Сейчас мы в одном из крупных городов Испании, с нами всё хорошо. Впервые за многие годы я могу вздохнуть спокойно и чувствовать себя в безопасности.
2. Мои статьи на Хабре на русском более недоступны. Все материалы, которые я написал, доступны на английском языке на https://ybogomolov.me и будут только там.
И да, наконец-то я без страха могу написать то, что болело с начала войны:
Нет войне. Нет «русскому миру». Путин и его приближенные — военные преступники, которых должны судить в Гааге. Украïнцi, тримайтеся та борiться, за вами правда! 🇺🇦
1. Я наконец-то навсегда покинул Россию вместе с семьей. Сейчас мы в одном из крупных городов Испании, с нами всё хорошо. Впервые за многие годы я могу вздохнуть спокойно и чувствовать себя в безопасности.
2. Мои статьи на Хабре на русском более недоступны. Все материалы, которые я написал, доступны на английском языке на https://ybogomolov.me и будут только там.
И да, наконец-то я без страха могу написать то, что болело с начала войны:
Нет войне. Нет «русскому миру». Путин и его приближенные — военные преступники, которых должны судить в Гааге. Украïнцi, тримайтеся та борiться, за вами правда! 🇺🇦
dd if=/dev/stuff of=/dev/tg
https://www.learningtypescript.com/articles/extreme-explorations-of-typescripts-type-system
Вдогонку к этому списку — упрощенный тайпчекер TypeScript, реализованный только на уровне типов: https://github.com/ronami/HypeScript
GitHub
GitHub - ronami/HypeScript: 🐬 A simplified implementation of TypeScript's type system written in TypeScript's type system
🐬 A simplified implementation of TypeScript's type system written in TypeScript's type system - ronami/HypeScript
Forwarded from A64m AL256m qn<cores> I0
Я начинаю выкатывать первую итерацию блогпоста по истории ФП, надеюсь что у кого-нибудь будут какие-то замечания по первой главе
токо осторожно, там до первой главки по истории идет метаисторический выблев на пять экранов
https://gist.github.com/klapaucius/f0adec8a567b7bf000c8bcf99686a9bd
токо осторожно, там до первой главки по истории идет метаисторический выблев на пять экранов
https://gist.github.com/klapaucius/f0adec8a567b7bf000c8bcf99686a9bd
Gist
История применения и оценки функционального программирования
История применения и оценки функционального программирования - prehist.md
Важная тема, без понимания которой лично я не вижу развития любого разработчика или управленца. Приходите послушать:
Forwarded from Lene.spb (Arina Malevskaia)
Эмоциональный интеллект очень важный навык в нашем изменчивом мире. Его развитие откроет перед вами большое количество новых возможностей.
В четверг, 8 сентября, в 18:00 (UTC +3) я проведу вебинар «Эмоциональный интеллект и зачем он вам нужен». Вместе мы в деталях рассмотрим из чего он состоит и какие выгоды может вам дать его использование.
Трансляция пройдет тут https://youtu.be/XeilTW0vkFI
Присоединяйтесь!
В четверг, 8 сентября, в 18:00 (UTC +3) я проведу вебинар «Эмоциональный интеллект и зачем он вам нужен». Вместе мы в деталях рассмотрим из чего он состоит и какие выгоды может вам дать его использование.
Трансляция пройдет тут https://youtu.be/XeilTW0vkFI
Присоединяйтесь!
YouTube
Эмоциональный интеллект и зачем он вам нужен
Эмоциональный интеллект - краеугольный камень успешной карьеры в 21 веке. Развитый эмоциональный интеллект откроет перед вами новый уровень понимания себя и окружающих. На встрече мы в деталях рассмотрим из чего он состоит и какие выгоды может вам дать его…
HTML Embed Code: