LINUX.ORG.RU

Об отсутствии кота

 ,


5

5

(cons cat (cons other-cat nil))

Как можно заметить, отсутствие коробки с котом не является ни коробкой, ни котом, но одновременно и тем, и тем.

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

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

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

Отсюда:

Третья Теорема Лавсана (о бесполезности статической типизации)

Статическая типизация не добавляет ничего действительно полезного и только лишь отбирает время.

Дискач.

★★★

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

В лиспе :литералы cons-cell и пара примитивов еще, поверх всей этой радости выражающейся как адт сделана «система типов» как ты описывал, но это «система типов» абсолютно не видна в терминах обычной системы типов. А вся ее функциональность определяется построением правильной структуры. Если хочется больше гарантий и радостей и вытащить сеты функций в нормальный type level то это тоже можно, хоть и не будет выглядеть красиво и абсолютно точно является темой отдельного разговора.

В общем если после предзащиты у меня будет время, то я смогу сделать proof-of-concept.

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

Того чтобы было известно в compile time каким предикатам удовлетворяет выражение, например и какие операции с ним возможны (впрочем я это и выше писал).

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

Того чтобы было известно в compile time каким предикатам удовлетворяет выражение, например и какие операции с ним возможны (впрочем я это и выше писал).

Ну и как мне в компайлтайме узнать разрешимо ли данное у-е, например?

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

Ну и да, не совсем понятно какой это имеет юзкейс. Зачем нам может в компайлтайме понадобиться определять какие-то предикаты?

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

В общем случае не знаю. Но если вы относите себя к последователям принципа all-or-nothing то разговор дальше смысла не имеет.

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

Ну вон лавсан описывал «систему типов» лиспа там это была одной из возможностей, можешт спросить у него про юзкейсы.

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

Действительно, не беда, если нельзя проверять _все_ предикаты. Достаточно,чтобы можно было проверять какие-то полезные. Можно привести пример таких полезных предикатов и соответствующих проверок?

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

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

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

Ну я это тут упомянул т.к. тут же прибежит куча народу и скажут, что мол зачем типизация если проверки в рантайме. Соотвественно я сразу указал что возможно пострить систему так, чтобы эту информацию хранить и использовать, добавив фантомные теги. Зачем нужно это в компайл тайме: за тем же чтобы повышать корректность программы и /автоматически доказывать справедливость утверждений на которые полагаешься/ и т.д. как и все доводы про типы в целом.

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

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

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

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

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

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

Ну и кроме того асбстракция, ООП и подобные вещи со статикой не связаны, но решают задачи получения гарантий корректности лучше статики.

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

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

Зачем тебе с динамикой теги? Их смысл чтобы к информации о типе бесплатно прибавлять информацию о свойствах.

Тут вообще несколько тредов разговора, конкретно этот о том, что динамика это частный случай статики, где сущесивует один universal type, описывающий физическую структуру значения/ркфлексивный обьект, называй как хочешь, а система типов в этом динамическом языке реализуется поверх этого обьекта (как и сделано в RTS этого языка).

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

У меня не было опыта с созданием систем требующих нетривиальных доказательств, а игрушечный пример приводить не хочется. Всякий порядок локов, да реализация байндингов к рантайму динамического языка с вытаскиванием информации в type level же не в счёт (доказывается тип возвращаемого значения исходя из входящих и убираются лишние рантайм проверки)?

Ну и кроме того асбстракция, ООП и подобные вещи со статикой не связаны, но решают задачи получения гарантий корректности лучше статики.

Не уверен.

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

Зачем тебе с динамикой теги? Их смысл чтобы к информации о типе бесплатно прибавлять информацию о свойствах.

Ну так ты в статике не может добавлять никакой информации о свойствах. У тебя только тип. А я в лиспе чего захочу - того и добавлю.

Тут вообще несколько тредов разговора, конкретно этот о том, что динамика это частный случай статики, где сущесивует один universal type, описывающий физическую структуру значения/ркфлексивный обьект, называй как хочешь, а система типов в этом динамическом языке реализуется поверх этого обьекта (как и сделано в RTS этого языка).

Но ты забываешь про метарпограммирование.

У меня не было опыта с созданием систем требующих нетривиальных доказательств

Но нетривиальные предикаты не дают никакого профита.

Не уверен.

Примера монадки IO тебе мало?

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

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

В смысле, оверхед? Тот же ATS (с зависимыми типами) работает почти со скоростью C/C++ и гораздо быстрее лиспа. Или ты про что?

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

В смысле, оверхед? Тот же ATS (с зависимыми типами) работает почти со скоростью C/C++ и гораздо быстрее лиспа. Или ты про что?

Я про оверхед в смысле затрат на написание кода.

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

реально проще написать свой легковесный верификатор под задачу.

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

Думаешь? Тебе же в верификаторе придётся проверить все те же условия

sort : (xs : List A) → Sorted' A
record Sorted' (xs : List A) : Set where
  field
    ys       : List A
    isSorted : IsSorted ys
    isPerm   : IsPermutation ys xs

+ написать парсер языка, на котором ты реализовал алгоритм

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

Ну так ты в статике не может добавлять никакой информации о свойствах. У тебя только тип.

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

Но ты забываешь про метарпограммирование.

Это как-то относится к вопросу выражения динамической системы типов в рамках статической?

Но нетривиальные предикаты не дают никакого профита.

То, с чем я сталкивался профит давало, но как пример приводить это в данном разговоре не слишком показательно.

Примера монадки IO тебе мало?

Я не знаю что именно ты имеешь ввиду под примером монадки IO.

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

Думаешь? Тебе же в верификаторе придётся проверить все те же условия

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

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

Я не знаю что именно ты имеешь ввиду под примером монадки IO.

Ну вот у нас есть unsafePerformIO, но если его вызывать как захочется, то все может сломаться. Нам же надо гарантировать консистентность. Мы берем и пишем интерфейс (bind) и теперь если мы используем только bind - то наш код заведомо корректен, если корректна реализация бинда. Так задача доказательства корректности всей программы сводится к доказательству корректности 3.5 строчек. И никаких типов, заметь.

Это как-то относится к вопросу выражения динамической системы типов в рамках статической?

Напрямую.

Тут мы можем начать долгий разговор о том что такое «тип» и о чем он говорит

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

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

В этом и есть суть картинки. Только статикодебилы знают ответ на твой вопрос.

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

Как животные со строками и еще кучей типов связаны?

Это тест. Если ты видишь в этой картинке хоть какой-то смысл, у тебя проблемы. Какие именно - зависит от того, какой смысл ты увидел в этой картинке.

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

Ну вот у нас есть unsafePerformIO, но если его вызывать как захочется, то все может сломаться. Нам же надо гарантировать консистентность. Мы берем и пишем интерфейс (bind) и теперь если мы используем только bind - то наш код заведомо корректен, если корректна реализация бинда. Так задача доказательства корректности всей программы сводится к доказательству корректности 3.5 строчек. И никаких типов, заметь.

какая-то альтернативная модель реальности, в которой люди и кони смешаны очень тщательно, я даже не знаю, что на это толком ответить.

Напрямую.

я был бы рад услышать обоснование.

Ты можешь попытаться, конечно, кодировать какие-то вещи типами, но это на практике весьма неудобно.

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

Реально юзабельны только те свойства, которые уже втсроены в систему типов в иде, собственно, типов

чо? (с)

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

я не уверен, что я понял идею, ты можешь пояснить это на небольшом примере?

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

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

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

какая-то альтернативная модель реальности, в которой люди и кони смешаны очень тщательно, я даже не знаю, что на это толком ответить.

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

я был бы рад услышать обоснование.

Обоснование чего?

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

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

я не уверен, что я понял идею, ты можешь пояснить это на небольшом примере?

Я могу сделать все формы моего языка макросами, которые извлекают произвольную информацию из терма формы, произвольным образом ее модифицируют и «приклеивают» к подформам. Когда раскрывается подформа, то с ней происходит то же самое. Например, для (#%app f x) макрос #%app при раскрытии посмотрит тип сам себя (будет Y), сгенерирует «дырку» и прилепит на термы, соответственно, f: дырка -> Y, x: дырка. f - идентификатор, который тоже макрос, при своем раскрытии увидит свой тип (дырка -> Y) и сматчит его стипом из контекста (X -> Y) (заполнив дырку), а на месте х, например, какой-то литерал, который представляет макрос (#%datum . x), который опять-таки возьмет при раскрытии тип себя (Х, в который превратилась дырка) и проверит, что литерал - действительно Х.

Таким образом, можно сделать простую типизированную лямбду, например. При этом мне никто не запрещает использовать в качестве X/Y и т.п. не только какие-нибудь там Integer, String, Integer -> Boolean и т.п. - но я могу туда засунуть вообще абсолютно любой объект, а форма при раскрытии (#%app, #%datum и так далее) будут как я захочу это дело обрабатывать (типизация - простейший случай, в этом случае обработка сводится к унификации)

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

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

Гм... Какие утверждения нельзя выразить типами Агды? Можешь придумать пример?

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

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

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

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

Именно. На самом деле все это все равно игрушки, при правильной декомпозиции (см. выше примером с биндом) и ручкой не так много доказывать надо будет.

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

Я вижу бардак, а потом - такой же бардак с подписанными типами, т.е. смысл в том, что у динамикодебилов прорвало днище, и они кинулись генерировать КОНТЕНТ.

Доктор, прошу, поставьте диагноз.

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

Доктор, прошу, поставьте диагноз.

Пациент, у вас отравление динамикодебильным контентом.

tailgunner ★★★★★
()

вам нужны пара очков

обсирающие статическую типизацию смотрят слишком далеко. обсирающие динамическую типизацию смотрят слишком близко.

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

Так в том и дело что оплучится вполне осмысленная вещь.

конечно! Это даже в стандарте есть. UB называется.

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

Ну и как мне в компайлтайме узнать разрешимо ли данное у-е, например?
Таким образом, можно сделать простую типизированную лямбду, например

sentence, например

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

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

С каких пор сложение обычных чисел - UB?

цитата моих слов без купюр:

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

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

Так еще раз - при чем тут UB и «правда в результате получится хрень полная», если получится вполне однозначный, корректный и осмысленный результат?

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

как мне в компайлтайме узнать разрешимо ли данное у-е

проще всего - по построению. можешь ли ты населить тип «данное у-е разрешимо»?

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

проще всего - по построению. можешь ли ты населить тип «данное у-е разрешимо»?

И ежели тайпчек не прошел - значит неразрешимо, так?

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

И ежели тайпчек не прошел - значит неразрешимо, так?

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

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

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

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

Так чето я не понял и в каком месте мне система типов поможет тогда?

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

в C/C++ не получится, если преобразовывать class→void*→class.

Если складывать указатели, то это тем более не имеет смысла.

А вот как у тебя «получился корректный результат», мне непонятно. Можно пример кода?

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

в C/C++ не получится, если преобразовывать class→void*→class.

Зойчем чтото преобразовывать?

А вот как у тебя «получился корректный результат», мне непонятно. Можно пример кода?

typedef int rhino;
typedef int giraffe;

rhino x = 10;
giraffe y = 20;
x+y;
anonymous
()
Ответ на: комментарий от emulek

ну тогда так:

struct rhino {
    int count;
};

struct giraffe {
    int count; 
};

rhino* x = new rhino(10);
giraffe* y = new giraffe(20);
*((int*)x) + *((int*)y);

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

так работает только потому что

Какая разница почему? Главное что работает. При этом вполне осмысленно и корректно.

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