LINUX.ORG.RU

Ответ на: комментарий от anonymous

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

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

Он описан.

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

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

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

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

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

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

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

anonymous ()
Ответ на: комментарий от quasimoto

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

не попадет

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

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

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

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

anonymous ()
Ответ на: комментарий от quasimoto

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

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

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

quasimoto ★★★★ ()
Последнее исправление: quasimoto (всего исправлений: 1)
Ответ на: комментарий от quasimoto

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

Короче, вот:

(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

вот так оно работает.

anonymous ()
Ответ на: комментарий от quasimoto

Это в typed racket?

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

anonymous ()
Ответ на: комментарий от anonymous

А если

(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
    //   переполнение иначе
quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от anonymous

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

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

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

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

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

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

tailgunner ★★★★★ ()
Ответ на: комментарий от quasimoto

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

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

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

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

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

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

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

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

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

anonymous ()
Ответ на: комментарий от tailgunner

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

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

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

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

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

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

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

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

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

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

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

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

anonymous ()
Ответ на: комментарий от anonymous

«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 рассматривается как библиотека.

tailgunner ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

korvin_ ★★★★★ ()
Ответ на: комментарий от anonymous

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

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

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от tailgunner

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

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

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

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

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

anonymous ()
Ответ на: комментарий от anonymous

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

Любитель premature optimisation?

anonymous ()
Ответ на: комментарий от korvin_

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

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

anonymous ()
Ответ на: комментарий от quasimoto

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

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

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

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

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

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от quasimoto

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

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

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

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

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

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

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

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

anonymous ()
Ответ на: комментарий от www_linux_org_ru

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

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

anonymous ()
Ответ на: комментарий от www_linux_org_ru

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

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

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

anonymous ()
Ответ на: комментарий от quasimoto

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

Почему нет?

anonymous ()
Ответ на: комментарий от anonymous

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

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

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

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

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

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

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от quasimoto

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

anonymous ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.