Channel: dd if=/dev/stuff of=/dev/tg
Реализация STLC на хаскеле с использованием индексов/уровней де Брёйна: https://hirrolot.github.io/posts/how-to-keep-lambda-calculus-simple.html 🔥
hirrolot.github.io
How to Keep Lambda Calculus Simple
Шахматы на тайп-левеле, причем с реализацией не только на TypeScript, но и на Rust:
https://github.com/Dragon-Hatcher/type-system-chess
Программа на Rust более чем в пять раз длиннее, чем на TS. Любопытные выводы автора:
• TS — писать на тайп-левеле почти приятно, но не хватает математики и let-байндингов (о да!).
• Rust — больше никогда!!1, очень медленно и многословно.
https://github.com/Dragon-Hatcher/type-system-chess
Программа на Rust более чем в пять раз длиннее, чем на TS. Любопытные выводы автора:
• TS — писать на тайп-левеле почти приятно, но не хватает математики и let-байндингов (о да!).
• Rust — больше никогда!!1, очень медленно и многословно.
GitHub
GitHub - Dragon-Hatcher/type-system-chess: Chess implemented entirely in the Rust and TS type systems.
Chess implemented entirely in the Rust and TS type systems. - Dragon-Hatcher/type-system-chess
Old, but gold: при определенных условиях компилятор раста генерировал имя типа размером 350 мегабайт. Хорошо все-таки, когда система типов Тьюринг-полна 🤤
TLA+, но с человеческим синтаксисом:
https://github.com/informalsystems/quint
Quint is inspired by TLA+ but provides an alternative surface syntax for specifying systems in TLA. The most important feature of our syntax is that it is minimal and regular, making Quint an easy target for advanced developer tooling and static analysis.
https://github.com/informalsystems/quint
Quint is inspired by TLA+ but provides an alternative surface syntax for specifying systems in TLA. The most important feature of our syntax is that it is minimal and regular, making Quint an easy target for advanced developer tooling and static analysis.
GitHub
GitHub - informalsystems/quint: An executable specification language with delightful tooling based on the temporal logic of actions…
An executable specification language with delightful tooling based on the temporal logic of actions (TLA) - informalsystems/quint
Начало новой серии статей о Effect:
https://ybogomolov.me/01-effect-intro 🔥
Рассказываю, что такое
https://ybogomolov.me/01-effect-intro 🔥
Рассказываю, что такое
Effect<R, E, A>
, как создавать, комбинировать, и интерпретировать эффект-выражения. Плюс небольшой бонус — функция effectify
для конвертации Node-style callbacks в эффект-выражения.ybogomolov.me
Intro To Effect, Part 1: What Is Effect?
В твиттере показали красивое: https://github.com/gvergnaud/hotscript
Вторая статья из серии “Intro to Effect”: https://ybogomolov.me/02-effect-handling-errors ✨
Рассказываю о способах обработки ошибок в Effect и механизмах организации повторяемых вычислений (retry policies).
Рассказываю о способах обработки ошибок в Effect и механизмах организации повторяемых вычислений (retry policies).
ybogomolov.me
Intro To Effect, Part 2: Handling Errors
Typed Design Patterns for the Functional Era
This paper explores how design patterns could be revisited in the era of mainstream functional programming languages.
https://arxiv.org/abs/2307.07069
This paper explores how design patterns could be revisited in the era of mainstream functional programming languages.
https://arxiv.org/abs/2307.07069
Третья статья из серии "Intro to Effect": https://ybogomolov.me/03-effect-managing-dependencies 🔥
Сегодня рассказываю про сервисы, слои (layers), и способ сделать DI без IoC-контейнеров.
Сегодня рассказываю про сервисы, слои (layers), и способ сделать DI без IoC-контейнеров.
ybogomolov.me
Intro To Effect, Part 3: Managing Dependencies
Четвертая статья из серии "Intro to Effect": https://ybogomolov.me/04-effect-concurrency ✨
Продолжаю цикл статей про Effect рассказом о конкурентном выполнении задач и fiber-based runtime.
Продолжаю цикл статей про Effect рассказом о конкурентном выполнении задач и fiber-based runtime.
ybogomolov.me
Intro To Effect, Part 4: Concurrency in Effect
Пятая статья из цикла “Intro to Effect”:
https://ybogomolov.me/05-effect-stm ✨
Разбираю тему software transactional memory (STM).
https://ybogomolov.me/05-effect-stm ✨
Разбираю тему software transactional memory (STM).
ybogomolov.me
Intro To Effect, Part 5: Software Transactional Memory in Effect
https://nostarch.com/learn-physics-functional-programming — изучение ньютоновской физики при помощи Haskell. Признаться честно, я чуть удивлен, что используется не какой-нибудь язык с завтипами вроде Agda, Lean, или Idris.
Nostarch
Learn Physics with Functional Programming
Deepen your understanding of physics by learning to use the Haskell functional programming language.
Замечательное эссе «TypeScripting The Technical Interview» — оммаж не менее прекрасному циклу эссе Aphyr’а. Очень рекомендую.
Richard-Towers
Richard Towers | Typescripting the technical interview
An homage to Aphyr's Typing the technical interview
https://morph.so/blog/the-personal-ai-proof-engineer/ — первый релиз LLM-проекта Morph, нацеленного на помощь в написании доказательств с помощью Lean.
https://twitter.com/zack_overflow/status/1715042340514017559 — Flappy Bird на тайплевеле тайпскрипта.
Это стало возможным благодаря кастомному рантайм, написанному на Zig.
A work of pure art 🖼️
Это стало возможным благодаря кастомному рантайм, написанному на Zig.
A work of pure art 🖼️
X (formerly Twitter)
zack (in SF) (@zack_overflow) on X
I wrote a 2D game, entirely in type-level Typescript.
Yes, you read that right. This is flappy bird, written only in Typescript types.
How did I do it? It involves a lot of type magic, and a new type-level Typescript runtime I made in Rust + Zig.
Let me…
Yes, you read that right. This is flappy bird, written only in Typescript types.
How did I do it? It involves a lot of type magic, and a new type-level Typescript runtime I made in Rust + Zig.
Let me…
dd if=/dev/stuff of=/dev/tg
https://twitter.com/zack_overflow/status/1715042340514017559 — Flappy Bird на тайплевеле тайпскрипта. Это стало возможным благодаря кастомному рантайм, написанному на Zig. A work of pure art 🖼️
И чуть более развернутый пост от автора: https://zackoverflow.dev/writing/flappy-bird-in-type-level-typescript
zackoverflow.dev
Flappy Bird Implemented in Typescript types
The ultimate type-level trickery
Design Guidelines for Domain-Specific Languages
Очень хороший пейпер, предлагающий 26 гайдлайнов, которыми следует руководствоваться при проектировании DSL.
Очень хороший пейпер, предлагающий 26 гайдлайнов, которыми следует руководствоваться при проектировании DSL.
Слайды доклада Томаса Микулы «Monads Are Not About Sequencing»: https://continuously.dev/presentations/Monads-not-about-sequencing_20231201.pdf
Видео доклада пока не выложили, но слайды стоят того, чтобы их прочесть, особенно если вы думаете, что понимаете монады 🙃
Видео доклада пока не выложили, но слайды стоят того, чтобы их прочесть, особенно если вы думаете, что понимаете монады 🙃
Моделирование доменных типов на расте: https://mmapped.blog/posts/25-domain-types.html
mmapped.blog
Universal domain types
A guide to domain-specific types that make sense.
HTML Embed Code: