Человеческое метапрограммирование

x in A => x in (listof* A), x in (Listof (Listof A)) => x in (Listof* A)

А (Listof (Listof (Listof A)))? Всё равно же тип будет изоморфен rose tree который я «знаю», зачем спорить.

не понял почему он должен это предскзаать?

Ну ты заявил - на входе функции 0 или 1, статика для всех аппликаций должна это гарантировать, значит, в рантайме в xor _никогда_ не попадёт что-то отличное от 0 или 1. Если попадёт - нет статики и непонятно зачем всё затевалось.

А (Listof (Listof (Listof A)))?

Он описан.

Всё равно же тип будет изоморфен rose tree который я «знаю», зачем спорить.

Конечно, изоморфен. Но это _другой тип_. Речь то шла именно об этом.

ПОЧЕМУ СТАТИКА С ОБЪЕДИНЕНИЯМИ НЕ МОЖЕТ БЫТЬ БЕЗОПАСНОЙ?

В википедии написано (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 (ты ничего про него не знаешь) и ты тупым аккессором достаёшь вариант который не совпадает с тем что использовался при конструировании, в динамике это не страшно, но в статике это плохо даже не с точки зрения типов а с точки зрения здоровья рантайма.

Ну ты заявил - на входе функции 0 или 1, статика для всех аппликаций должна это гарантировать

ну да, она и гарантирует.

в рантайме в xor _никогда_ не попадёт что-то отличное от 0 или 1.

Да, не попадет.

Если попадёт - нет статики и непонятно зачем всё затевалось.

Но оно не попадет.

не с точки зрения типов а с точки зрения здоровья рантайма.

То есть, например, кусок памяти сделанный как int и помещённый в объединение как int можно использовать как кусок памяти char*.

не попадет

То есть нужно сделать (let ([x (read)]) (print (xor (что-то x) 0)))? Чем будет это «что-то»?

Но вообще тоже - по ощущениям, тебе приходит union t (ты ничего про него не знаешь) и ты тупым аккессором достаёшь вариант который не совпадает с тем что использовался при конструировании

Так тебе тайпчекер не даст тупым аксесором и блаблабла.

То есть нужно сделать (let ([x (read)]) (print (xor (что-то x) 0)))? Чем будет это «что-то»?

Надо сделать так: (let ([x (read)]) (when (or (zero? x) (one? x)) (print (xor x 0))))

Погугли публикации. Ее не методом тыка делали.

Вот, кстати, интересно - для агды применима cut-elimination theorem, так что на вопрос о непротиворечивости можно просто закрыть глаза (это вопрос веры). Но с Racket такое явно не пройдёт.

Так тебе тайпчекер не даст тупым аксесором

В cyclone так и сделали - нельзя читать из неразмеченного объединения поля с указательным типом, так что пример выше - валиндная программа на си, но не на cyclone. С другой стороны всё ещё можно инициализировать int, прочитать поле char и получить переполнение в числах (хотя бы не сегфолт). То есть, чтобы полностью сделать их безопасными нужно вообще запретить читать. Или читать по тому полю которое инициализировали, то есть добавить тег (хм, или unoin t<номер_инициализированного_поля>, только номер_инициализированного_поля может быть неизвестен при компиляции).

Но с Racket такое явно не пройдёт.

В Racket полиморфное типизированное лямбда-исчисление с объединениями, рекурсивными типами и сабтайпингом - его непротиворечивость есть доказанный факт.Там некоторые интересные моменты только с occurence typing, variable-arity polymorphism и continuations. Про это все публикации есть.

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

Это в typed racket? Тогда понятно.

Короче, вот:

(define-type t243 243)
(define-type t478 478)
(define-type 243U478 (U t243 t478))

(: yoba (t243 -> t478))
(define (yoba x) 478)

(: x 243U478)
(define x 243)

(yoba x) ; Type Checker: Expected t243, but got 243U478 in: x

(define-predicate t243? t243)
(when (t243? x) (yoba x)) ; 478

(define-predicate t478? t478)
(when (not (t478? x)) (yoba x)) ; 478

Это в typed racket?

Да. Объединения обычные, неразмеченные. А то что каждому значению соовтетствует свой тип - это уже на систему типов и на ее противоречивость никак не влияет. Мы в рамках любой системы типов можем захардкоженные типа определять совершенно произвольным образом.

А если

(define x (if (eq? (read) 0) 243 478))

?

В си также, только предикаты неопределимы в 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
    //   переполнение иначе

(if (eq? (read) 0) 243 478)

Если ввести 0, то ветки не будут выполнены. Если что-то другое - будут, соответственно. Все корректно чекнется. А с set! как в твоем примере на сишке оно не чекнется.

Если ввести 0, то ветки не будут выполнены.

То есть наоборот, конечно :)

Если ввести 0, то ветки не будут выполнены.

А откуда compile-time чекер знает что будет введено в runtime (ввод должен быть в runtime, если я что-то не так написал)?

А откуда 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) ; х тайпчекается и все хорошо)

http://blog.racket-lang.org/2010/09/extending-typed-racket-part-1.html

http://www.ccs.neu.edu/racket/pubs/icfp10-thf.pdf

http://www.ccs.neu.edu/racket/pubs/popl08-thf.pdf

http://www.ccs.neu.edu/racket/pubs/popl08-thf.pdf

«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»

Епт, здравомыслящие лисперы O_o

Всё это значит - 1) оба when отрабатывают в _рантайме_, то есть статический тайпчек плавно переходит в динамические проверки, 2) объект x имеет _тэг_, иначе ни один из when не сможет узнать где что. Первое не плохо, потому что только так можно решить проблему с проверкой недетерминированных значений, второе тоже хорошо и примерно так же нужно сделать в си (добавить тэг в union). Только это всё-таки размеченные объединения и проверки в рантайме.

объект x имеет _тэг_

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

В примере твоего кода ты когда определяешь новую операцию у меня это выглядит как квадратик :cry: видимо, у меня со шрифтами проблема :)

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

Чё? Статический тип всегда один.

минимальный — да, обычно один, но и в обоих примерах normal_if и crazy_if он тоже один — Grandfather

вообще, ты неправильно защищаешься :-) мог бы сказать, скажем, что верификация может быть сделана поверх твоей системы

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

епрст, минимальный конечно не Grandfather, а Grandson

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

Новые узлы и связи появляются при каждом вызове функции. При каждом сработавшем if'е.

Ты вообще программист? Этим решением ты просадишь производительность на порядки.

Ну так каковы не верхушки? ИтаК, мы выяснили, что твой алгоритм имеет в основе своей вычислительную модель реактивного программирования (то что ты выше описывал - оно и есть). Теперь напиши отличия.

Мы в очередной раз выяснили, что ты разговариваешь с голосами в своей голове.

http://www.ccs.neu.edu/racket/pubs/icfp10-thf.pdf

Насколько я понимаю, в Typed Racket: 1) проверка типов выполняется самим макросом при раскрытии; 2) после раскрытия макроса код не тайпчекается вообще, несмотря даже на наличие в нем конструкций, которые на неверных типах имеют UB (unsafe-fl+), так что ошибки в макросах приведут к молчаливым глюкам в время исполнения. Если я понял статью правильно, то N2 выглядит однозначно лучше.

1) оба when отрабатывают в _рантайме_

Ну да он отрабатывает в рантайме.

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

Не понял, каким образом? Тот факт, что внутри ветки х имеет соовтетствующий тип гарантируется _статически_. Именно потому что там выполняется предикат :)

Ты все понял с точностью до наоборот. Тем не «статический тайпчек переходит в динамические проверки», а, наоборот, из кода с динамическими проверками (то есь из обычного кода в динамическом ЯП) чекер выводит статические гарантии.

2) объект x имеет _тэг_, иначе ни один из when не сможет узнать где что.

Зачем нам нужен тэг, чтобы узнать, что объект - единица? Достаточно просто применить к объекту предикат (= 1). В моем примере нету никаких тегов.

Только это всё-таки размеченные объединения и проверки в рантайме.

Да нет, это неразмеченные объединения и проверки в компайлтайме :) Тегов никаких нет - значит объединения неразмечены. Чекер выводит статические гарантии - значит проверки в компайлтайме.

так что ошибки в макросах приведут к молчаливым глюкам в время исполнения.

1) проверка типов выполняется самим макросом при раскрытии;

Нет, сперва выполняется раскрытие, потом - проверка.

так что ошибки в макросах приведут к молчаливым глюкам в время исполнения.

Нет, не приведут. Сам тайпчекер, собственно, и заменяет обычные операции на unsafe (например если чекер видит, что операция car применяется не к list, а к pair, то он меняет ее на unsafe-car). И гарантируется что семантика программы останется прежней.

Новые узлы и связи появляются при каждом вызове функции. При каждом сработавшем if'е.

Да ради бога. несущественно.

Этим решением ты просадишь производительность на порядки.

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

Мы в очередной раз выяснили, что ты разговариваешь с голосами в своей голове.

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

Нет, сперва выполняется раскрытие, потом - проверка.

«2.2 Manipulating Syntax Objects», проверка на то, что аргумент - лямбда. Ты это называешь «раскрытие, потом проверка»?

Сам тайпчекер, собственно, и заменяет обычные операции на unsafe

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

+1 к Ruby.

«2.2 Manipulating Syntax Objects», проверка на то, что аргумент - лямбда.

Не понял, о чем ты.

Ты это называешь «раскрытие, потом проверка»?

Я не знаю, что «это», и о чем ты вообще говоришь. Я знаю, что сперва раскрываются пользовательские макросы, а потом чекается код. Если хочешь - можешь проверить сам, у тебя на это уйдет 5 минут, не больше.

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

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

Я знаю, что сперва раскрываются пользовательские макросы, а потом чекается код.

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

«2.2 Manipulating Syntax Objects», проверка на то, что аргумент - лямбда.

Не понял, о чем ты.

Сорри, это пример в статье «Languages as Libraries» (нашел по ссылке из блога Typed Racket): http://www.ccs.neu.edu/racket/pubs/pldi11-thacff.pdf

Вот этот код:

(define-syntax (only-λ stx)
 (syntax-parse stx
   [(_ arg:expr)
    (define c
      (local-expand #’arg ’expression ’()))
    (define k (first (syntax->list c)))
    (if (free-identifier=? #’#%plain-lambda k)
        c
        (error "not λ"))]))

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

Нет, нету такой библиотечной функции.

В статье весь Typed Racket рассматривается как библиотека.

Зачем нам нужен тэг, чтобы узнать, что объект - единица?

Для этого не нужен, а для того, чтобы определить, что результат выполнения read имеет тип number, нужен.

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

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

Не понял, каким образом?

Ну ты до запуска программы не знаешь в какую ветку попадёшь, так как x зависит от ввода (после запуска).

Зачем нам нужен тэг, чтобы узнать, что объект - единица?

Сделай вместо чисел сложные структуры. И вообще, попробуй скомпилировать (в уме) свой пример в си или ассемблер наиболее оптимальным образом - сразу станет понятно, что такое в принципе не может работать без динамических проверок и тайптегов. Правда, можно сделать объединение неразмеченным при условии, что все поля объединения боксированы/тегированы и содержат всю информацию о своих типах в рантайме (как и полагается в динамике), тогда с такими неразмеченными (формально) объединениями можно безопасно работать - есть type-of, typecase, можно поднять такие предикаты времени выполнения. В статике такого нет, поэтому неразмеченные объединения никак не помеченных (в рантайме) типами значений небезопасны - нужно добавить тайптег и работать с размеченными объединениями с помощью switch/case/match с гарантией покрытия по ветвям (компиляторы C/C++ умеют такое для перечислимых типов в switch).

Сорри, это пример в статье «Languages as Libraries»

Ну там просто проверка на лямбду, хз. Вот про Typed Racket:

http://repository.readscheme.org/ftp/papers/sw2007/01-culpepper.pdf

В статье весь Typed Racket рассматривается как библиотека.

Ну вообще любой #lang это библиотека (collection). Вообще в любом ЯП тайпчекер можно сказать библиотека. Но сами функции тайпчека нигде не импортируются, оно все вызывается неявно и доступа к внутренностям нет (если ты конечно не перепишешь исходники этой «библиотеки»).

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

Любитель premature optimisation?

Для этого не нужен, а для того, чтобы определить, что результат выполнения read имеет тип number, нужен.

И что из этого следует, собственно? К чему ты ведешь?

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

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

это тебе загадка

подсказка — решение дается одним словом — в union надо положить ************

з.ы. интересно, есть ли еще случаи

Ну ты до запуска программы не знаешь в какую ветку попадёшь, так как x зависит от ввода (после запуска).

Ну да, не знаю. А зачем мне это знать? Мне надо знать что в точке вызова yoba тип будет t243, тайпчекер мне это _статически_ гарантирует, что еще?

Сделай вместо чисел сложные структуры.

У меня в примере были сложные структуры? нет, не было.

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

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

В статике такого нет, поэтому неразмеченные объединения никак не помеченных (в рантайме) типами значений небезопасны - нужно добавить тайптег и работать с размеченными объединениями с помощью switch/case/match с гарантией покрытия по ветвям (компиляторы C/C++ умеют такое для перечислимых типов в switch).

Ты все фундаментально неверно понимаешь. У тебя все еще дедовское представление о типах, навязанное примитивными системами типа хаскелей и агд. Еще раз - у нас есть множество значений. Любое подмножество этого множества является типом. Все. Изначально типы бывают у значений (не у термов). Но _доказав_, что терм может принимать значения лишь из множества Х, мы считаем его термом типа Х (по определению). Хотя на самом деле у термов нету типов и быть не может - это нонсенс. Ты фундаментально перепутал причину и следствие - давным-давно надо было доказывать, что в той или иной точке программы тот или иной терм мог принимать значения из того или иного множества и только из него. Но системы типов были неразвиты, алгоритмов чекера/инференса не знали, по-этому вид и способы построения этих множеств были фундаментально ограничены (очевидно, что в идеальном случае все должно соответствовать ZFC, как и требует практика и исходная задача). Но мы сейчас живем в 21 веке, те теории, которые были хороши 50 лет назад, стоит выкинуть на свалку, наука на месте не стоит. Так что на данный момент мы уже постепенно можем возвращаться к правильному представлению о типах.

и содержат всю информацию о своих типах в рантайме

Собственно это ключевой момент. _любое_ значение _всегда_ содержит полную информацию о своем типе в рантайме. Потому что тип значения - это любое множество, которому это значение принадлежит.

подсказка — решение дается одним словом — в union надо положить ************

Если мы в юнион положили нечто, что позволяет различить что там внутри него хранится, то это что-то (по определению) тайптег :)

Как он закодирован - нам непринципиально.

В статике такого нет

Почему нет?

Если мы в юнион положили нечто, что позволяет различить что там внутри него хранится, то это что-то (по определению) тайптег :)

Как он закодирован - нам непринципиально.

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

т.е. не только там тайптега *нет*, но и вычислить его мы *не можем*, если нам доступно только само значение юниона, все типы ветвей юниона и все, что оттуда доступно по указателям (то есть недоступна, скажем, *история* того, что происходило с программой раньше)

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

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

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