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

мне просто интересно как это без рантайма решается

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

просто мне кажется, что по факту это ничем не отличается от енамов

но он там как-то отношения между термами проверяет, а не реальные значения, как я понял

так нет, енам это тупо ADT, сумма-тип и произведение-тип, это притивные вещи. DT это еще пи-тип и сигма-типы

мне интересно именно на каком этапе это должно упасть. если например описал ты протокол в котором в зависимости от первого байта, возвращает значение с определенным типом. А пользователь при этом пропихнул тебе какую-то ггадость

https://t.me/kanaflow/3 - вот тут серия моих постов, где я пытался описать и ADT, и завтипы (реклама так реклама)

если забыл проверку на гадость то на этапе компиляции

если не забыл, то нигде :)

если забыл проверку на гадость то на этапе компиляции

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

правильно я понимаю?

ну так можно и к ассемблерным джампам свести

а нужно ли так сложно?)

компилятор берет на себя вычисления в компайлтайме

ну я кажись понял

это короче приблуда, чтобы матчи не писать

вот

матчи там надо писать все равно

Вечер зависимых типов в группе раста

матчи там надо писать все равно

ну так тогда не нужно

Щас кана сама пояснит вам за жизнь

да я скинул посты, где я пояснял, че мне еще писать

кто такой кана

я

известный хаскелист?

не, начинающий ток

а оно нужно?

гофер: а генерики нужны?

гофер: а генерики нужны?

Нет

Можно ж копипастить, зачем генерики?

А про зав типы я не понял плюсов кроме формальной верификации

Можно ж копипастить, зачем генерики?

а можно юзать Any и падать в рантайме

здесь также

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

кроме монад

rust-mdo же есть

Так сказали ж, что всеравно матчить надо

И падать всеравно в рантайме

что матчить

Значение

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

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

топчик

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

Если я в энам пихну - тоже

М

энам из пятиста чисел тоже будешь делать?

энам из пятиста чисел тоже будешь делать?

Я ж так понял что количество ветвей не уменьшится с зав типами, не?

суть в том, что имея тип (псевдоязык) (b : Bool, if b then String else Int) мы просто по факту не можем составить значение (True, 1), хоть в рантайме, хоть в комплайтайме. или имея функцию (a: Nat) -> (b: Nat) -> (a < b) -> Nat мы просто по факту не сможем передать в функцию такие числа, что b будет меньше a, хоть в рантайме, хоть в компайлатйме. (a < b) - это пруф, что a меньше b. Если его не передать явно, то и функцию вызывать нельзя. А передать его можно только если построив. А построив его можно только явно

Ну а если мы получили тип бул из ввода полтзователя

Как тут быть?

Ну а если мы получили тип бул из ввода полтзователя

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

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

кстати как в идрисе сделать тип с предикатом? чет сложно по сравнению с ликвидхаскелем

вот я как-то писал пример кода, который читает длину массива и работает с векторами введенной длины мы тут типизруем, что вектор с сумммой имеет именно n + m длину

кстати как в идрисе сделать тип с предикатом? чет сложно по сравнению с ликвидхаскелем

делать умные конструкторы мб

ну допустим число на интервале [0, 1]

как-то такой вопрос задвали в идрис конфе, ответ был - можно, но геморно. Fin можно использовать для 0..N

ого

думал такое там тривиально

могу предположить, что просто смарт конструктор, который требует пруфы, что a <= x <= b, но я хз вообще, нужно там спрашивать

кк

МММ

29142 segmentation fault (core dumped)

Закрутилась карусель, потекло дерьмецо то

Ну а если мы получили тип бул из ввода полтзователя

Никак, ты из ввода пользователя получаешь String, который превращаешь в Option<Bool> (или Result<Bool, String> например), а потом прокидываешь через Some корректное вычисление над Bool.

Что значит корректное вычисление?

Смысл зависимых типов же не в том, чтобы данные корректно типизировать, это фигня несложно в любом языке делается, где данные от функций изолированы. Фишка зависимых типов в доказательстве тотальности, гарантии что твой сраный алгоритм не разойдётся и не уйдёт в бесконечность на определённом входе, а завершится. Мы просто внутрь нашего ЯП'а пихает очень мощную, но тьюринг-неполную машину

А почему важно что она не полная?

Halting problem, не слышал?

Не

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

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

Это типизированный пролог какой-то получается у вас

Не

А про машину тьюринга?

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

А про машину тьюринга?

Ну что-то мельком

Ну что-то мельком

Типа смысл в том, что мы моделируем вычисление как некую машину с бесконечной лентой, одним "указателем" на ней и каким-то глобальным навсегда заданным множеством состояний. На ленте написаны нолики и единички, в каждый шаг машина может в зависимости от значения на ленте и состояния машина может поменять состояние ячейки, двинуть вправо/влево курсор и поменять состояние. Выделяют кроме того специальное состояние "а, нахуй", после которого машина перестаёт двигаться. Крутость этой штуки в том, что можно скостылить такую машину тьюринга, что мы можем на ленте "закодировать" любую другую машину тьюринга и её вход, так что если закодированная маштна тьюринга останавливается, то наша универсальная тоже, да они ещё и одинаковый результат имеют. А если закодированная не останавливается, то и универсальная будет работать бесконечно

Допустим

(я уже прочитал в Вики по тегам которые вы кинули) но интересно к чему приведет дальше

Сразу встаёт вопрос -- а чо нельзя скостылить машину тьюринга, которая на входе берёт любую другую закодированную машину и её вход, останавливается и даёт ответ 0, если закодированнвя не останавливается и работает вечно, если закодированная останавливается. А нихуя, такой машины создать нельзя

Как жить то теперь

Но! Мы можем написать такие алгоритмы, которые работают для некоторого подмножества, более узкого набора машин тьюринга. Более того, мы можем бесконечно приближаться к идеальному результату, создавать всё более и более широкие классы машин, для которых мы можем на компьютере проверять проверять завершаются ли они или нет

Но! Мы можем написать такие алгоритмы, которые работают для некоторого подмножества, более узкого набора машин тьюринга. Более того, мы можем бесконечно приближаться к идеальному результату, создавать всё более и более широкие классы машин, для которых мы можем на компьютере проверять проверять завершаются ли они или нет

👍