ну это такой метаязык

Судя по репе, у него только шаблонизатор https://github.com/alexander-irbis/incrust

это часть. В гиттере он говорил, что пока не хочет публиковать свой код.

можно сделать так ListF a x = Nul | Cons a x

соотвественно, если определить data Fix f = Fix (f (Fix f))

то List a ~ Fix (ListF a)

но в расте же нет HKP, поэтому такой Fix я не запишу, насколько я понимаю

это часть. В гиттере он говорил, что пока не хочет публиковать свой код.

Ок. Давно там не был, там gamedev раздел особенно интересный)

polymorphism

ну для HKP, нужно, чтобы в качестве параметра генерика можно было передать тип хотя бы * -> * , т.е. тип с дыркой

Прижилась дырка

т.е. чтобы твой генерик мог потенциально генерировать все разновидности, которые можно получить подставляя в свой параметр другие типы

без стирания типов это, насколько мне известно, не реализуется

плюс момент что раст делает имплементации параметрических типов специализированными

плюс момент что раст делает имплементации параметрических типов специализированными

да т.е. мономорфизация vs стирание, производительность vs высшие абстрации, CLR vs JVM

Товарищи, представим, что у меня есть какая-то глупая функция типа https://gist.github.com/Odomontois/2208fce3d68b3050fbf5cbc0daad5ed0

Вернись в скала чат)

в книге упоминалось существование редких ситуаций с динамической диспатчеризацией, но я в детали не вникал еще сделано только по причине того, что иногда динамическая более производительна чем статическая

не совсем так гугли про trait object, в общем, динамический диспатч есть, только тогда это уже не дженерик и не записывается как дженерик

Ок. Давно там не был, там gamedev раздел особенно интересный)

Сейчас там Кварк немножко активный, начал пилить свой движок

ну представь у тебя trait Functor <F<_>>{ fn map<A, B>(fa: F<A>, f : A -> B) -> F<B> } такая имплементация должен уметь производить любой F<B>, имя потенциально лишь B. Если B в рантайме превращён а адрес, ссылку на произвольный тип без лайфтайма и всего такого - это реализуемо. Если B может иметь варьируемый размер и содержать субструктурную информацию в типе - это уже крайне затружнительно

Сейчас там Кварк немножко активный, начал пилить свой движок

Так он же уже итак пилил GFX и Claymore. Или это что-то другое?

Знаете, чего мне не хватает?

Детектора дедлоков

Чтобы он паниковал, если все потоки залочились на мьютексах

Детектора дедлоков

а ведь эта задача очень даже реализуема, если расширить систему типов в Rust

да вроде и без типов легко реализовать - каждый поток когда ждет мьютекса ставит свой бит ожидания в "1", если биты всех потоков стоят в 1 - дедлок

да вроде и без типов легко реализовать - каждый поток когда ждет мьютекса ставит свой бит ожидания в "1", если биты всех потоков стоят в 1 - дедлок

ненене, чтобы вообще код с потенциальным дедлоком не компилился

да вроде и без типов легко реализовать - каждый поток когда ждет мьютекса ставит свой бит ожидания в "1", если биты всех потоков стоят в 1 - дедлок

ИХМО это не сделать без кастомизации стандартной библиотеки

ненене, чтобы вообще код с потенциальным дедлоком не компилился

Вот это лучше всего

Но это прямо ваще сложное колдунство На две диссертации

тут вот есть @clayrat, он представляет лучший чат в телеграмме, и он знает что с этим делать

Я знаю, что более менее теория для таких верификаций сделана для csp

там регулярно проскакивают фразу вроде "сессионные типы - это почти линейные типы"

arrow function не вызвать из себя

Если, конечно, не унести в замыкание переменную, где она лежит

Я знаю, что более менее теория для таких верификаций сделана для csp

Вплоть до того, что зная нагрузку можно точно посчитать размеры буферов для каналов

там регулярно проскакивают фразу вроде "сессионные типы - это почти линейные типы"

Щито?!

Это параллельные вещи вообще

Щито?!

что не так?

это параллельные вещи с очень схожей типотеорной семантикой

грубо говоря, компилятор, который может делать одно, можно дописать, чтобы он мог делать оба

а ведь растопилятор может одно

Сессионные без линейных (точнее афинных) не сделать, это да, но сессионные это не отдельная система, лол

Сессионные без линейных (точнее афинных) не сделать, это да, но сессионные это не отдельная система, лол

а ведь только что говорил, что паралелльные

В том смысле, что не связанны

Сессионные это не система типов

Как линейные и прочие

Сессионные это не система типов

объясните это заявление, пожалуйста

Так он же уже итак пилил GFX и Claymore. Или это что-то другое?

Он подключился к аметистам, при этом параллельно начал писать three-rs

https://github.com/kvark/three-rs

О, шикарно!

Здесь вот http://users.eecs.northwestern.edu/~jesse/pubs/alms/tovpucella-alms.pdf говорится, что We argue that a general, practical type system based on Girard’s linear logic (1987) can naturally and directly express many of the special cases, such as region-based memory management, aliasing control, session types, and typestate.Таким образом система типов с линейной логикой может реализоваывать не только region-based memory management (rust), но и сессионные типы

Именно на основании таких утверждений я и говорю, что используя то же ядро компилятора в rust можно запихнуть и concurrency control

не валидный, о том и говорил

да, мы пришли к общему знаменателю

не предлагаю

просто говорил о HKP в расте

haskell, scala, purescript, coq, agda, idris ...

все системы построены на стирании типов и runtime dispatch для реализаций trait

В haskell\purescript type class ы В scala\idris implicit parameters

подожди, разве тот же функтор нельзя в компайл-тайме специализировать?

а, понятно то есть типа HKP со специализацией в компайл-тайме в расте всё-таки не ждать, как я понимаю(

подожди, разве тот же функтор нельзя в компайл-тайме специализировать?

проблема не в вызове метода, а в написании уже полиморфных функций вида fn foo<F<_> : Functor>

хаскель очень умный, во многих случаях он умеет мономорфизировать как rust, но есть случаи, где мономорфизация принципиально невозможна

так, стоп типы в том же х-ле ведь выводятся все равно, иначе бы не чекались, зачем их стирать тогда

яркий пример - полиморфная рекурсия

так, стоп типы в том же х-ле ведь выводятся все равно, иначе бы не чекались, зачем их стирать тогда

типы могут иметь бесконечную сложность

рассмотрим любимую в хаскеле пару структур данных для 2-3 дерева data Node a = Node2 a a | Node3 a a a data Tree a = Single a | Cons (Tree (Node a))

на уровне типов гарантируется, что любая ветвь дерева имеет одинаковую глубину

теперь представьте себе реализацию Foldable для такого типа

Она должна уметь в рантайме сгенерировать функции, которые могут работать с Node ( Node ( Node ... )) непресказуемого порядка вложенности

понял, спасибо

То же самое для HKP - попробуйте реализовать Free монаду

Которая может иметь неопределённое количество обёрток функтора

так, стоп типы в том же х-ле ведь выводятся все равно, иначе бы не чекались, зачем их стирать тогда

типы нужны для доказательства корректности кода если код на этапе компиляции получился корректный, то после компиляции тебе типы уже не сдались (за исключением костылестроения на рантайм рефлексии)

типы нужны для доказательства корректности кода если код на этапе компиляции получился корректный, то после компиляции тебе типы уже не сдались (за исключением костылестроения на рантайм рефлексии)

молодец, тред не прочитал, какую-то фигню ответил, хорош

я тред прочитал, комментарий был к "зачем их стирать"

как будто в расте у тебя в бинарнике осталось что-то кроме примитивов

плохо прочитал

стирать не в том смысле

стирать как в джаве