Ну ты заявил - на входе функции 0 или 1, статика для всех аппликаций должна это гарантировать, значит, в рантайме в xor _никогда_ не попадёт что-то отличное от 0 или 1. Если попадёт - нет статики и непонятно зачем всё затевалось.
ПОЧЕМУ СТАТИКА С ОБЪЕДИНЕНИЯМИ НЕ МОЖЕТ БЫТЬ БЕЗОПАСНОЙ?
В википедии написано (Because of the limitations of their use, untagged unions are generally only provided in untyped languages or in an unsafe way (as in C)). Но вообще тоже - по ощущениям, тебе приходит union t (ты ничего про него не знаешь) и ты тупым аккессором достаёшь вариант который не совпадает с тем что использовался при конструировании, в динамике это не страшно, но в статике это плохо даже не с точки зрения типов а с точки зрения здоровья рантайма.
Но вообще тоже - по ощущениям, тебе приходит union t (ты ничего про него не знаешь) и ты тупым аккессором достаёшь вариант который не совпадает с тем что использовался при конструировании
Так тебе тайпчекер не даст тупым аксесором и блаблабла.
Вот, кстати, интересно - для агды применима cut-elimination theorem, так что на вопрос о непротиворечивости можно просто закрыть глаза (это вопрос веры). Но с Racket такое явно не пройдёт.
В cyclone так и сделали - нельзя читать из неразмеченного объединения поля с указательным типом, так что пример выше - валиндная программа на си, но не на cyclone. С другой стороны всё ещё можно инициализировать int, прочитать поле char и получить переполнение в числах (хотя бы не сегфолт). То есть, чтобы полностью сделать их безопасными нужно вообще запретить читать. Или читать по тому полю которое инициализировали, то есть добавить тег (хм, или unoin t<номер_инициализированного_поля>, только номер_инициализированного_поля может быть неизвестен при компиляции).
В Racket полиморфное типизированное лямбда-исчисление с объединениями, рекурсивными типами и сабтайпингом - его непротиворечивость есть доказанный факт.Там некоторые интересные моменты только с occurence typing, variable-arity polymorphism и continuations. Про это все публикации есть.
В Racket полиморфное типизированное лямбда-исчисление с объединениями, рекурсивными типами и сабтайпингом - его непротиворечивость есть доказанный факт.
Да. Объединения обычные, неразмеченные. А то что каждому значению соовтетствует свой тип - это уже на систему типов и на ее противоречивость никак не влияет. Мы в рамках любой системы типов можем захардкоженные типа определять совершенно произвольным образом.
В си также, только предикаты неопределимы в compile-time (так как инициализация может зависеть от IO), а в runtime нет необходимой информации:
union int_char { int i; char c; };
char fun(int i) { return i >= 0 && i < 100 ? i : 0; }
union int_char x = { .i = 300 };
// fun(x);
// ^ passing 'union int_char' to parameter of incompatible type 'int'
if (getchar() == '0')
x.c = 100;
printf("%d\n", x.c);
// ^ 100 при вводе 0
// переполнение иначе
Если ввести 0, то ветки не будут выполнены. Если что-то другое - будут, соответственно. Все корректно чекнется. А с set! как в твоем примере на сишке оно не чекнется.
А откуда compile-time чекер знает что будет введено в runtime (ввод должен быть в runtime, если я что-то не так написал)?
А какая ему разница что будет введено в рантайм? Один фиг форма вернет или 243 или 478. Главное что в точке вызова (yoba x) лежать 478 не может, потому что предикат t243 выполнен. То есть
(: x 243U478)
(define x (if (eq? (read) 0) 243 478))
;здесь х имеет тип 243U478
(define-predicate t243? t243)
(when (t243? x)
;t243 внутри этой ветки #t, поэтому внутри х имеет тип t243.
(yoba x) ; соответственно х тайпчекается и все хорошо)
(define-predicate t478? t478)
(when (not (t478? x))
; известно что х имеем тип 243U478 = (U t243 t478), но не может быть типом t478, значит она имеет тип (U t243 t478) / t478 = t243.
(yoba x) ; х тайпчекается и все хорошо)
«A lack of types in typical scripting languages means that programmers must (re)discover critical pieces of design information every time they wish to change a program»
Всё это значит - 1) оба when отрабатывают в _рантайме_, то есть статический тайпчек плавно переходит в динамические проверки, 2) объект x имеет _тэг_, иначе ни один из when не сможет узнать где что. Первое не плохо, потому что только так можно решить проблему с проверкой недетерминированных значений, второе тоже хорошо и примерно так же нужно сделать в си (добавить тэг в union). Только это всё-таки размеченные объединения и проверки в рантайме.
Хотя на 64 машине можно спокойно откусить от слова целый байт и получить тегированный указатель для объединений вплоть до 256 типов, но всё равно тегированный.
В примере твоего кода ты когда определяешь новую операцию у меня это выглядит как квадратик :cry: видимо, у меня со шрифтами проблема :)
у тебя (и) с браузером проблема, так как когда ты этот значок копипастишь, он выглядит для меня как квадратик, в то время как все символы quasimoto я вижу нормально
минимальный — да, обычно один, но и в обоих примерах normal_if и crazy_if он тоже один — Grandfather
вообще, ты неправильно защищаешься :-) мог бы сказать, скажем, что верификация может быть сделана поверх твоей системы
это будет достаточно сильный аргумент, если у тебя система будет достаточно модульна и будет реализовывать вещи по-порядку, не навязывая своего чего-то
Это не проблема, просто сортировка делается каждый раз при появлении нового узла.
Новые узлы и связи появляются при каждом вызове функции. При каждом сработавшем if'е.
Ты вообще программист? Этим решением ты просадишь производительность на порядки.
Ну так каковы не верхушки? ИтаК, мы выяснили, что твой алгоритм имеет в основе своей вычислительную модель реактивного программирования (то что ты выше описывал - оно и есть). Теперь напиши отличия.
Мы в очередной раз выяснили, что ты разговариваешь с голосами в своей голове.
Насколько я понимаю, в Typed Racket: 1) проверка типов выполняется самим макросом при раскрытии; 2) после раскрытия макроса код не тайпчекается вообще, несмотря даже на наличие в нем конструкций, которые на неверных типах имеют UB (unsafe-fl+), так что ошибки в макросах приведут к молчаливым глюкам в время исполнения. Если я понял статью правильно, то N2 выглядит однозначно лучше.
то есть статический тайпчек плавно переходит в динамические проверки
Не понял, каким образом? Тот факт, что внутри ветки х имеет соовтетствующий тип гарантируется _статически_. Именно потому что там выполняется предикат :)
Ты все понял с точностью до наоборот. Тем не «статический тайпчек переходит в динамические проверки», а, наоборот, из кода с динамическими проверками (то есь из обычного кода в динамическом ЯП) чекер выводит статические гарантии.
2) объект x имеет _тэг_, иначе ни один из when не сможет узнать где что.
Зачем нам нужен тэг, чтобы узнать, что объект - единица? Достаточно просто применить к объекту предикат (= 1). В моем примере нету никаких тегов.
Только это всё-таки размеченные объединения и проверки в рантайме.
Да нет, это неразмеченные объединения и проверки в компайлтайме :) Тегов никаких нет - значит объединения неразмечены. Чекер выводит статические гарантии - значит проверки в компайлтайме.
так что ошибки в макросах приведут к молчаливым глюкам в время исполнения.
1) проверка типов выполняется самим макросом при раскрытии;
Нет, сперва выполняется раскрытие, потом - проверка.
так что ошибки в макросах приведут к молчаливым глюкам в время исполнения.
Нет, не приведут. Сам тайпчекер, собственно, и заменяет обычные операции на unsafe (например если чекер видит, что операция car применяется не к list, а к pair, то он меняет ее на unsafe-car). И гарантируется что семантика программы останется прежней.
«2.2 Manipulating Syntax Objects», проверка на то, что аргумент - лямбда.
Не понял, о чем ты.
Ты это называешь «раскрытие, потом проверка»?
Я не знаю, что «это», и о чем ты вообще говоришь. Я знаю, что сперва раскрываются пользовательские макросы, а потом чекается код. Если хочешь - можешь проверить сам, у тебя на это уйдет 5 минут, не больше.
Этот тайпчекер - стандартная библиотечная функция, которую (обычно) не требуется ни дорабатывать, ни вызывать руками?
Нет, нету такой библиотечной функции. Руками ничего не дорабатывается и не вызывается, потмоу что нечего дорабатывать и вызывать.
Я знаю, что сперва раскрываются пользовательские макросы, а потом чекается код.
На самом деле не только пользовательские - for (типизированная форма) тоже. Я не знаю как это работает, не спрашивай (учитывая что unsafe-операции подставляются сразу при раскрытии for...).
То есть ыт не в состоянии описать свой алгоритм? Так и запишем. Собственно, от упоротой немерлебляди ничего иного и не ожидалось.
Объяснять что-то упоротой лиспобляди из подворотни, которая настолько тупа, что не может подружиться с тайпчекером и, не моргнув глазом превращает линейный алгоритм в квадратичный, объяснять что либо бесполезно.
Ну ты до запуска программы не знаешь в какую ветку попадёшь, так как x зависит от ввода (после запуска).
Зачем нам нужен тэг, чтобы узнать, что объект - единица?
Сделай вместо чисел сложные структуры. И вообще, попробуй скомпилировать (в уме) свой пример в си или ассемблер наиболее оптимальным образом - сразу станет понятно, что такое в принципе не может работать без динамических проверок и тайптегов. Правда, можно сделать объединение неразмеченным при условии, что все поля объединения боксированы/тегированы и содержат всю информацию о своих типах в рантайме (как и полагается в динамике), тогда с такими неразмеченными (формально) объединениями можно безопасно работать - есть type-of, typecase, можно поднять такие предикаты времени выполнения. В статике такого нет, поэтому неразмеченные объединения никак не помеченных (в рантайме) типами значений небезопасны - нужно добавить тайптег и работать с размеченными объединениями с помощью switch/case/match с гарантией покрытия по ветвям (компиляторы C/C++ умеют такое для перечислимых типов в switch).
В статье весь Typed Racket рассматривается как библиотека.
Ну вообще любой #lang это библиотека (collection). Вообще в любом ЯП тайпчекер можно сказать библиотека. Но сами функции тайпчека нигде не импортируются, оно все вызывается неявно и доступа к внутренностям нет (если ты конечно не перепишешь исходники этой «библиотеки»).
Правда, можно сделать объединение неразмеченным при условии, что все поля объединения боксированы/тегированы и содержат всю информацию о своих типах в рантайме
есть еще как минимум один случай, когда можно сделать объединение неразмеченным и нигде, повторяю — нигде в рантайме не хранятся тайптеги или что-то им эквивалентное
это тебе загадка
подсказка — решение дается одним словом — в union надо положить ************
Ну ты до запуска программы не знаешь в какую ветку попадёшь, так как x зависит от ввода (после запуска).
Ну да, не знаю. А зачем мне это знать? Мне надо знать что в точке вызова yoba тип будет t243, тайпчекер мне это _статически_ гарантирует, что еще?
Сделай вместо чисел сложные структуры.
У меня в примере были сложные структуры? нет, не было.
И вообще, попробуй скомпилировать (в уме) свой пример в си или ассемблер наиболее оптимальным образом - сразу станет понятно, что такое в принципе не может работать без динамических проверок и тайптегов.
Но оно работает без динамических проверок и тайптегов. И в си можно скомплиировать так, что будет работать без динамических проверок и тайптегов. Ты снова выдумываешь несуществующие проблемы.
В статике такого нет, поэтому неразмеченные объединения никак не помеченных (в рантайме) типами значений небезопасны - нужно добавить тайптег и работать с размеченными объединениями с помощью switch/case/match с гарантией покрытия по ветвям (компиляторы C/C++ умеют такое для перечислимых типов в switch).
Ты все фундаментально неверно понимаешь. У тебя все еще дедовское представление о типах, навязанное примитивными системами типа хаскелей и агд. Еще раз - у нас есть множество значений. Любое подмножество этого множества является типом. Все. Изначально типы бывают у значений (не у термов). Но _доказав_, что терм может принимать значения лишь из множества Х, мы считаем его термом типа Х (по определению). Хотя на самом деле у термов нету типов и быть не может - это нонсенс. Ты фундаментально перепутал причину и следствие - давным-давно надо было доказывать, что в той или иной точке программы тот или иной терм мог принимать значения из того или иного множества и только из него. Но системы типов были неразвиты, алгоритмов чекера/инференса не знали, по-этому вид и способы построения этих множеств были фундаментально ограничены (очевидно, что в идеальном случае все должно соответствовать ZFC, как и требует практика и исходная задача). Но мы сейчас живем в 21 веке, те теории, которые были хороши 50 лет назад, стоит выкинуть на свалку, наука на месте не стоит. Так что на данный момент мы уже постепенно можем возвращаться к правильному представлению о типах.
и содержат всю информацию о своих типах в рантайме
Собственно это ключевой момент. _любое_ значение _всегда_ содержит полную информацию о своем типе в рантайме. Потому что тип значения - это любое множество, которому это значение принадлежит.
Если мы в юнион положили нечто, что позволяет различить что там внутри него хранится, то это что-то (по определению) тайптег :)
Как он закодирован - нам непринципиально.
ок, в первоначальном моем варианте все же можно было различить, если постараться, но во втором моем варианте, похоже, уже невозможно
т.е. не только там тайптега *нет*, но и вычислить его мы *не можем*, если нам доступно только само значение юниона, все типы ветвей юниона и все, что оттуда доступно по указателям (то есть недоступна, скажем, *история* того, что происходило с программой раньше)
однако все равно значения из данного юниона типобезопасны при операциях с ними
да, эти операции существуют (тривиальный случай «в юнион положен объект класса без публичных методов» исключается)
Вообще, кстати, учитывая тот факт, что имея неразмеченные объединение и пары можно выразить размеченные, а вот вот имея размеченные - неразмеченные не выразишь, очевидно, что неразмеченные объединениы должны быть.