Homoiconic C

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

Но ведь динамика только для написания такого кода и нужна. Зачем вам динамика, если вы не используете её по назначению?

Тогда да, у меня 100% покрытие ф-й/операторов. И я не представляю как можно писать код, в котором оно не 100%.

Добро пожаловать в реальный мир, Нео. Представь себе, здесь пишут код без 100%-покрытия.

Я не вижу там ни слова про STLC.

Меня не интересует STLC.

Рантайм с тайпчекером - это и есть черный ящик.

Это какой-то особый, уличный рантайм.

Все прекрасно запускается и без стенда.

Всё, что ты пишешь - возможно.

имхо всё понятно он написал.

ИМХО ты - еще не все присуствующие. Специально для серьезных людей - я имел в виду, что _я_ не понял написанного, и уже это означает, что поняли не все.

Здесь — может и нет. Ошибка будет там, где значение этой функции будет использовано.

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

Ерунду говорите.

если плюнет - то значит система типов слабенькая. С нормальной системой типов не плюнет:

> (require typed/racket)
> (: f (Number -> (U Number String)))
> (define (f x)
    (if (> (random 2) 0)
        (sin x) "abc"))
> (f 10)
- : (U Number String)
-0.5440211108893698
> (f 10)
- : (U Number String)
"abc"
> (f 10)
- : (U Number String)
"abc"
> (f 10)
- : (U Number String)
-0.5440211108893698
> 

Но ведь динамика только для написания такого кода и нужна.

Еще один классический статикобред.

Добро пожаловать в реальный мир, Нео. Представь себе, здесь пишут код без 100%-покрытия.

Реальный мир - это студенческие лабы? До релиза только у них есть шанс дойти без 100% покрытия операторов - если нерадивый студент наляпал что-то на коленке и пошел сдавать код, даже не запустив его предварительно хоть разок. В серьезных приложениях такой ситуации, конечно, быть не может.

Меня не интересует STLC.

STLC взята в качестве простого примера. Можешь привести свой - название языка, его операционная семантика, место где в этой семантике что-то говорится про рантайм.

Это какой-то особый, уличный рантайм.

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

Всё, что ты пишешь - возможно.

Не понял к чему эта фраза, поясни.

До релиза только у них есть шанс дойти без 100% покрытия операторов

Релиза? Откуда взялся релиз?

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

Ну-ну.

Все прекрасно запускается и без стенда.

Всё, что ты пишешь - возможно.

Не понял к чему эта фраза, поясни.

Поясни, чего именно ты не понял.

Пока контраргументов не предоставлено, это горькая правда.

Не нужно выдавать обыкновенную сумму типов за какое-то чудо.

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

Релиза? Откуда взялся релиз?

Что значит откуда взялся?

Поясни, чего именно ты не понял.

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

Ну-ну.

А что, может? Что же это за серьезное приложение такое, которое ни разу не запускали?

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

Это объединение, а не сумма. Факт остается фактом - все прекрасно чекается, статических ошибок в коде нет. Зачем ты его привел - не ясно.

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

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

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

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

Зачем нужно обратное?

Релиза? Откуда взялся релиз?

Что значит откуда взялся?

Это значит «почему ты вдруг заговорил о релизе?».

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

Яснее не могу. Попробуй почитать контекст - я его специально для тебя привел.

А что, может?

Да, может.

Что же это за серьезное приложение такое, которое ни разу не запускали?

Что заставило тебя подумать, будто его не запускали?

Но в реальности такого не бывает

«в void f(int) не попадает string» это тоже модель выполнения, как и «в void f(A) попадают A, B <: A и только они», «в vector<A> попадают A, B <: A и только они», или «уровень (STM a) не компонуется c уровнем (IO a) неявно и наоборот». Причём существующие языки, такие как C++, Scala, SML или Haskell, которые вполне справляются с тем, чтобы добиться _полной_ верификации по таким моделям.

А ты говоришь про что-то более сложное вроде

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

sort : List A -> OrderedList A гарантирует. Подробнее — http://www.cse.chalmers.se/~nad/repos/equality. Кстати, OrderedList — индуктивный тип, то есть, опять, сами данные и вещи вообще за собой должны следить.

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

(Number -> (U Number String)

T -> T и потом падающий downcast T -> Integer (T ~ Integer — ок, T !~ Integer — exception).

Это объединение, а не сумма

Которое всё равно fiber сумма в самом топосе и обычная сумма в категории частичного порядка подъобъктов.

Racket выезжает за счёт того что lispobject-ы и так тегированы — нетегированное объединение тегированных значений ~ тегированное объединение нетегированных значений, ну и monic-и ещё «расставляет» (то есть — нет, так как теги уже есть), в ML-ях их руками пишут (вводя теги), например:

data a :+ b = L a | R b deriving Show
class b :> a where sup :: a -> b
instance a :+ b :> a where sup = L
instance a :+ b :> b where sup = R

sin_ :: Integer -> Double
sin_ = sin . fromInteger

f :: Integer -> Double :+ String
f x = if odd x then sup $ sin_ x else sup "abc"

(правда такой sup в полиморфизм совершенно не умеет). И дальше главное, чтобы a + b -> a и a + b -> b не производились — они epic-и, но не monic-и, так что об автоматических преобразованиях не может быть речи — статика предполагает что их нет, есть только a + b -> c если есть a -> c _и_ b -> c, какая-то статика может их допускать в виде non-exhaustiveness с compile-time предупреждениями и расставлением исключений. Но динамика отличается тем, что допускает вообще любые top -> some и, как следствие, anything -> anything', так как anything -> top -> anything', так что звучит это либо в мире где только top (а нам в любом случае нужны примитивные типы и операции, так что ULC это не вариант), либо если семантика выполнения предполагает наличие _|_.

Зачем нужно обратное?

Есть две причины:

1. Спецификации типов - это много бойлерплейта.

2. Применяемые сейчас системы типов очень слабы и примитивны, по-этому они часто не позволяют выразить нужные Х и Y.

3. И, наконец, главное - а зачем нужно _не_ обратное? То есть если и без типов все хорошо, нафиг типы добавлять? Не надо ломать то, что работает.

Это значит «почему ты вдруг заговорил о релизе?».

А о чем еще говорить? Приложение нужно за тем, чтобы его использовали. А используют релиз, ога.

Яснее не могу. Попробуй почитать контекст - я его специально для тебя привел.

Но твоя фраза никак с контекстом не связана. Это просто рандомная фраза, которая никак не соотносится с предметом разговора. В этом и проблема. Переформулируй. Не надо «яснее». по-другому.

Да, может.

Это ложь.

Что заставило тебя подумать, будто его не запускали?

Ты же сам сказал, что покрытие <100%. То есть есть функции, которые не отрабатывали. ИРЛ такого не бывает. Потому что как только функция написана - она сразу запускается на тестовых данных.

Причём существующие языки, такие как C++, Scala, SML или Haskell, которые вполне справляются с тем, чтобы добиться _полной_ верификации по таким моделям.

Тут есть два возражения:

1.Таких языков не существует. Упомянутые языки не позволяют добиться верификации. Потому что добиться верификации принципиально невозможно.

2. Зачем вообще добиваться верификации? Ну зачем, например, требовать, чтобы уровень STM не компоновался с уровнем IO, если задача требует обратного? В данном случае если не компонуется - значит задача решена НЕ ПРАВИЛЬНО. Зачем нам нужны средства, которые запрещают нам получать правильные решения?

sort : List A -> OrderedList A гарантирует.

Что, прошу прощения? Это некий набор букв, что он гарантирует и каким образом, можно узнать?

Или — кто гарантирует интелу или амд, что их модели _действительно_ имеют отношения к железкам которые они разрабатывают?

никто, коненчо же. Ведь никаких гарантий получить невозможно.

И тем не менее известно

Конечно, неизвестно.

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

И что? Тестами тоже отлавливаются тысячи багов.

T -> T и потом падающий downcast T -> Integer (T ~ Integer — ок, T !~ Integer — exception).

Что еще за T -> T? Я тип указал, вполне конкретный: (Number -> (U Number String). Никаких T -> T тут и близко нет.

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

Но твоя фраза никак с контекстом не связана. Это просто рандомная фраза, которая никак не соотносится с предметом разговора.

Забавно. Я то же самое думаю о том, что пишешь ты.

Которое всё равно fiber сумма в самом топосе и обычная сумма в категории частичного порядка подъобъктов.

Всем очевидно, что ЛЮБОЙ ОБЪЕКТ является суммой в подходящей категории. Что дальше-то? Называть суммой все что угодно? Ну давай уберем все существительные и оставим только одно - «сумма».

Racket выезжает за счёт того что lispobject-ы и так тегированы

Это низкоуровневые детали реализации. Они никак не связаны с семантикой. Это кстати особенность статикопетухов - кроме подмены понятий (которая была сделана в предыдущем пункте с суммой) они еще любят рассматривать любое явление ЛИБО с формальной точки зрения ЛИБО с точки зрения практической реализации. Но никак не с обеих! Так как иначе их точка зрения будет фейлить.

либо если семантика выполнения предполагает наличие _|_.

То есть во всех применяющихся на данный момент ЯП. Спасибо, что подтвердил мою правоту.

так будет неудобно.

А это DSL. Лисперов функциональные проблемы не волнуют.

Спецификации типов - это много бойлерплейта.

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

Применяемые сейчас системы типов очень слабы и примитивны, по-этому они часто не позволяют выразить нужные Х и Y.

Так ли уж часто?

То есть если и без типов все хорошо, нафиг типы добавлять?

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

Не надо ломать то, что работает.

А тут соглашусь. Ломать динамику не нужно, она сама сломается.

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

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

Так ли уж часто?

Очень часто.

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

Ага, ну вот она суть. Напоминаю, что мы как раз и обсуждаем ПОЧЕМУ без типов что-то плохо. Так что из ваших слов можно понять - плохо потому что плохо. А объективных причин нет.

А тут соглашусь. Ломать динамику не нужно, она сама сломается.

Она как раз не ломается.

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

Ну то есть то что std::vector<std::string>{«1», «2», «3»}.push_back(4); не компилируется мне приснилось. И (Data.List.length 5) тоже.

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

Data.List.length от чисел уже попадает в бинарники?

Зачем вообще добиваться верификации?

Относительно ПО? Чтобы писать правильные программы без _|_, ну или хотя бы по возможности более правильные.

зачем, например, требовать, чтобы уровень STM не компоновался с уровнем IO, если задача требует обратного?

Затем что (write-to-chan a (f (read-from-chan b))) в io не будет работать атомарно. STM блок задаёт вычисления которые, будучи явно смешанными/скомпонованными с IO с помощью atomically, выполнятся атомарно/разом в конкурентом окружении на расшаренных данных. Ну и обратно — IO не должно попадать в STM из-за особенностей работы самой STM (сбрасываемые транзакции, например, приведут к повторениям IO действий — в некоторых случаях это ок, делают unsafeIOtoSTM).

Что, прошу прощения? Это некий набор букв, что он гарантирует и каким образом, можно узнать?

Это сигнатура на агде, ссылку я привёл. После можно писать любые my-sort : List A -> List A и доказывать my-sort ≡ canon-sort, где canon-sort = Ordered-to-List ∘ sort.

Выше есть более простой пример про то что определённая функция copy для дерева действительно копирует дерево, то есть ничего не путает и эквивалентна id денотационно, хотя операционно она работает иначе (требует памяти для копии).

Ты сомневаешься в том что взяв алгоритм сортировки можно построить конструктивное формальное (CZF, допустим) математическое доказательство того что это действительно сортировка? Или что это доказательство можно перенести в теорию типов (MLTT, соответственно)?

Я тип указал, вполне конкретный: (Number -> (U Number String)

Так мы про статика vs динамика или уже статика vs _typed_ racket? Если всё ещё первое, то никаких typed racket — изволь принимать во внимание T и даункасты.

ЛЮБОЙ ОБЪЕКТ является суммой в подходящей категории

Я не говорил про любой объект и подходящую категорию, я говорил про fiber sum (pushout) в «той самой» категории (в которой объекты — типы и обычная сумма — размеченное объединение или «сырое» объединение размеченных) и про обычную сумму в другой конкретной и весьма важной категории образуемой как poset категория из подъобъектов (объект + monic = подтип + инъекция на надтип) Top (то есть подтипов его же).

То есть во всех применяющихся на данный момент ЯП

Как будто что-то хорошее :)

Это низкоуровневые детали реализации

А этот U может быть не disjoint? Не disjoint для неравных типов?

Ну то есть то что std::vector<std::string>{«1», «2», «3»}.push_back(4); не компилируется мне приснилось. И (Data.List.length 5) тоже.

Как из того, что не компилируются два частных случаях, следует, что возможна верификация в общем?

Data.List.length от чисел уже попадает в бинарники?

Это к чему?

Относительно ПО?

Конечно. Или мы о чем-то другом говорим?

Чтобы писать правильные программы без _|_, ну или хотя бы по возможности более правильные.

Огромный класс программ (наверное, даже большинство программ) _|_ by design. А если будет не _|_ - то это будет неправильная программа. Так что _правильные_ программы ваша верификация только мешает писать, как выяснилось.

Затем что (write-to-chan a (f (read-from-chan b))) в io не будет работать атомарно.

А нам это и надо. Выходит ваша верификация снова не позволила напистаь правильную программу?

Это сигнатура на агде, ссылку я привёл. После можно писать любые my-sort : List A -> List A и доказывать my-sort ≡ canon-sort, где canon-sort = Ordered-to-List ∘ sort.

Замечательно. Вы написали некоторую последовательность символов и из нее по определенным правилам получили другую последовательность символов. Каким образом это гарантирует тот факт, что ваша программа _действительно_ сортирует? Да никаким.

Выше есть более простой пример про то что определённая функция copy для дерева действительно копирует дерево, то есть ничего не путает и эквивалентна id денотационно

Но никто не гарантирует, что это ф-я _действительно_ копирует дерево. На самом деле, эта функция может делать что угодно.

Ты сомневаешься в том что взяв алгоритм сортировки можно построить конструктивное формальное (CZF, допустим) математическое доказательство того что это действительно сортировка? Или что это доказательство можно перенести в теорию типов (MLTT, соответственно)?

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

Так мы про статика vs динамика или уже статика vs _typed_ racket? Если всё ещё первое, то никаких typed racket — изволь принимать во внимание T и даункасты.

T и даункасты - это чиста незамутненная динамика. При чем тут тогда статика неясно вовсе.

Я не говорил про любой объект и подходящую категорию, я говорил про fiber sum (pushout) в «той самой» категории (в которой объекты — типы и обычная сумма — размеченное объединение или «сырое» объединение размеченных) и про обычную сумму в другой конкретной и весьма важной категории образуемой как poset категория из подъобъектов (объект + monic = подтип + инъекция на надтип) Top (то есть подтипов его же).

А я говорю про то, что, еще раз, ЛЮБОЙ ОБЪЕКТ является суммой в подходящей категории. И когда тебе говорят: «объединение типов - не сумма» - то имеется в виду какое-то конкретное определение суммы типов (общепринятое) в какой-то конкретной категории, а не ЧТО-ТО в КАКОЙ-ТО категории, которую ты выбрал, чтобы сделать объединение суммой. Ясно, нет?

Как будто что-то хорошее :)

Конечно, хорошее. Нам нужно писать программы с _|_, у нас есть языки, которые позволяют писать программы с _|_. Это хорошо. Вот если бы не было таких языков, это было бы плохо.

Спецификация типов позволяет обойтись без документации

убивать, убивать, убивать.

Как из того, что не компилируются два частных случаях, следует, что возможна верификация в общем?

Про в общем никто не говорил. Речь была про «эти функции (kmalloc) нельзя вызывать из этих функций (обработчики прерываний)» что я назвал моделью и верификацией по ней. (Нам бы определённых артиклей сюда).

Огромный класс программ (наверное, даже большинство программ) _|_ by design

Например? Термы EventLoop : Type не есть то что населяет _|_, термы бесконечного Stream : Type -> Type — тоже.

Ты наверно думаешь, что non-termination обязательно населяет _|_? Необязательно.

А нам это и надо.

Если надо, то используем контейнеры IO. Если зачем-то надо (хотя перекинуть значение между каналами без thread-safety это что-то специальное) STM трогать не атомарно, то достаём по atomically read-from-chan, обрабатываем f и пишем с помощью atomically write-to-chan, то есть write-to-chan-io a =<< f <$> read-from-chan-io b.

На самом деле, эта функция может делать что угодно.

Баг в реализации языка? Зачем сводить всё к абсурду? Доказательства математических фактов и свойств программ вообще на агде вполне правильны, постольку-поскольку.

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

А, вопросов нет. Непротиворечивость ZFC или PA (trolling intended) тебе никто не докажет.

При чем тут тогда статика неясно вовсе.

dmfd рассказывал про случай когда фабрика генерирует недетерминированным образом значения типов A, B, C, ..., то есть либо вариант, либо T, а другой потребитель даункастит это к конкретному A — падение не наступает при запуске программы, как ты говоришь, а лишь тогда когда фабрика соберёт значение по отношению к которому потребитель частичен. Статика тут станет ещё не просто статическими проверками против даункастов, но и инструментом разработки/рефакторинга — утверждение A + B + C + ... для фабрики вынудит потребителей покрывать все ветви, а при изменении типа фабрики потребуется привести в порядок всех её потребителей.

Ясно, нет?

Да, просто это звучит, с точность до дуальностей, как «зависимое произведение это не произведение» (там pullback, то есть co-pushout, как обобщение product, то есть co-sum).

Нам нужно писать программы с _|_

Тебе нужно писать абсурдные программы? Зачем? :)

Речь была про «эти функции (kmalloc) нельзя вызывать из этих функций (обработчики прерываний)» что я назвал моделью и верификацией по ней.

Но ведь никто не гарантирует, что нельзя вызывать.

Например? Термы EventLoop : Type не есть то что населяет _|_

Они и есть.

Ты наверно думаешь, что non-termination обязательно населяет _|_?

Это не я так думаю, это факт такой.

Если надо, то используем контейнеры IO.

А нам не надо в IO, нам надо в STM.

то достаём по atomically read-from-chan, обрабатываем f и пишем с помощью atomically write-to-chan, то есть write-to-chan-io a =<< f <$> read-from-chan-io b.

А нам надо без бойлерплейта.

Баг в реализации языка?

Именно.

Зачем сводить всё к абсурду?

А я не свожу все к абсурду. Вы же считаете что в вашем приложении могут быть баги? Почему же их в реализации языка быть не может?

А, вопросов нет. Непротиворечивость ZFC или PA (trolling intended) тебе никто не докажет.

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

dmfd рассказывал про случай когда фабрика генерирует недетерминированным образом значения типов A, B, C, ..., то есть либо вариант, либо T, а другой потребитель даункастит это к конкретному A — падение не наступает при запуске программы, как ты говоришь, а лишь тогда когда фабрика соберёт значение по отношению к которому потребитель частичен. Статика тут станет

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

утверждение A + B + C + ... для фабрики вынудит потребителей покрывать все ветви

А мы просто неявно подставим для непокрытых ветвей ексцешены. Делов-то.

Да, просто это звучит, с точность до дуальностей, как «зависимое произведение это не произведение» (там pullback, то есть co-pushout, как обобщение product, то есть co-sum).

Важен контекст утверждения. Особенно если мы говорим о теоркате - где абсолютно любой объект можно сделать абсолютно чем угодно, достаточно лишь выбрать подходящую категории. То есть в рамках теорката утверждения вида «А есть Х» вообще не являются синтаксически корректными утверждениями рассматриваемой формальной теории (если бы являлись - теоркат был бы очевидно противоречив).

Тебе нужно писать абсурдные программы?

Зачем абсурдные? Просто нетерменируемые. Сервер, например.

Но ведь никто не гарантирует, что нельзя вызывать.

Начнём с простого — std::vector<std::string> гарантирует что в него не поместят int? Теперь — есть ли гарантия что IO не будет вызвано из STM (используется флаг -XSafe)? Ситуация с kmalloc и прерываниями это в точности ситуация с IO и STM.

Они и есть.

Это не я так думаю, это факт такой.

Зачем абсурдные? Просто нетерменируемые. Сервер, например.

Прежде чем это станет фактом — возьми агду, попробуй населить тип _|_ (Data.Empty) — написать терм absurd : _|_, узнай про ко-индуктивные данные и ко-рекурсивные программы, убедись в возможности написать таким образом «сервер» и любые non-terminations вообще которые, тем не менее, не населяют тип _|_, то есть не ломают логическую структуру языка.

Тип «нетерминируемые вычисления-серверы» населяют конкретные программы-серверы, никакого отношения к значению _|_ из теории вычислимых функций / теории доменов они не имеют — в тех теориях _|_ как значение означает «зависающие алгоритмы» (которые ненужны), если в языке есть полиморфизм и намёки на CH, то эти значения, к тому же, _|_ : forall a. a и _|_ (= absurd) : _|_, где _|_ как тип это уже соответствующий тип «канонической лжи» из теории типов (тоже не имеет отношения к значению _|_).

Вопрос в том как _запретить_ «зависающие алгоритмы» — согласно проблеме останова это невозможно сделать, можно только _разрешить_ примитивную < структурную < well-founded рекурсии. Цена — сохранение CH и логической структуры языка.

А сервер — не алгоритм, с ним никаких проблем.

А нам не надо в IO, нам надо в STM.

А нам надо без бойлерплейта.

УМВР :) Не знаю чего ты хочешь. Хотя, да, можно не вводить уровни — сделать thread-safe примитивы в io и компоновать их явно:

fn(...)
{
    ...
    { // <- atomically
        scoped_lock { mutex }
        ...
    } // <- unlock

// можем верить что deadlock-ов не будет?

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

Именно.

Почему же их в реализации языка быть не может?

Вот когда будут — откроешь issue / исправишь. А пока ссылок на серьёзные баги в системах типов статически типизированных языков которые ломают гарантии нет — говорить не о чем.

Как только в твоем языке появились даункасты

Я и говорю — если запретим даункасты, будет статика и какие-то бОльшие ограничения. Если нет — будет прецедент с простыми ошибками несовпадения типов которые появляются в произвольно далёкое время от начала работы программы.

А мы просто неявно подставим для непокрытых ветвей ексцешены.

Ок, возможно что это и динамика вообще — именно то что надо (есть же приложения для которых такое поведение именно предпочтительно). Но может быть нужно и обратное.

Важен контекст утверждения.

Скажи какие правила type formation, term introduction / elimination и computation у U из Racket.

scoped_lock { mutex }

Хотя — как взять больше одного мьютекса? Как не забыть взять всё что участвует в «транзакции»?

возможно что это ... именно то что надо

И если говорить про case / match, то хаскель со скалой тоже расставляют такие исключения, просто они говорят об этом.

Начнём с простого — std::vector<std::string> гарантирует что в него не поместят int?

Нет.

Теперь — есть ли гарантия что IO не будет вызвано из STM (используется флаг -XSafe)?

Нет.

Прежде чем это станет фактом — возьми агду, попробуй населить тип _|_ (Data.Empty) — написать терм absurd : _|_, узнай про ко-индуктивные данные и ко-рекурсивные программы, убедись в возможности написать таким образом «сервер» и любые non-terminations вообще которые, тем не менее, не населяют тип _|_, то есть не ломают логическую структуру языка.

Ну так попробуй написать и убедись, что не получится.

Тип «нетерминируемые вычисления-серверы» населяют конкретные программы-серверы, никакого отношения к значению _|_ из теории вычислимых функций / теории доменов они не имеют — в тех теориях _|_ как значение означает «зависающие алгоритмы»

А сервер - это и есть классический зависающий алгоритм, согласно определению. (let loop () *body* (loop)) - вот тебе евент луп, в частном случае: (let loop () (loop)), давай, типизируй без _|_.

Вопрос в том как _запретить_ «зависающие алгоритмы»

Но нам не надо их запрещать. Подавляющее большинство программ - зависающие (по формальному определению «зависающих» программ, то есть они возвращают _|_). Наоборот - нам надо уметь писать такие программы.

А сервер — не алгоритм, с ним никаких проблем.

Что значит не алгоритм? А что это?

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

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

Вот когда будут — откроешь issue / исправишь. А пока ссылок на серьёзные баги в системах типов статически типизированных языков которые ломают гарантии нет — говорить не о чем.

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

Я и говорю — если запретим даункасты, будет статика и какие-то бОльшие ограничения. Если нет — будет прецедент с простыми ошибками несовпадения типов которые появляются в произвольно далёкое время от начала работы программы.

И?

Скажи какие правила type formation, term introduction / elimination и computation у U из Racket.

Посмотри в их работе, там система типов typed/racket описана. Однако при чем тут разговор о суммах?

Нет.

Нет.

Приведи два куска кода которые это продемонстрируют — один поместит число в вектор строк, а другой выполнит IO из STM.

Ну так попробуй написать и убедись, что не получится.

Написать absurd : ⊥ и сломать агду — не получится. А написать non-termination и не сломать — получится:

module NT where

open import Coinduction
open import Function
open import Data.Empty
open import Data.Unit
open import IO

loop : IO ⊤ → IO ⊥
loop body = ♯ body >> ♯ loop body

main = run $ loop $ putStrLn "..."

-- $ agda -i /usr/share/agda-stdlib -i . -c NT.agda
-- $ ./NT
-- ...

или из Category.Monad.Partiality:

open import Coinduction

data _⊥ {a} (A : Set a) : Set a where
  now   : (x : A) → A ⊥
  later : (x : ∞ (A ⊥)) → A ⊥

never : ∀ {a} {A : Set a} → A ⊥
never = later (♯ never)

или Data.Stream:

open import Coinduction

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

repeat : ∀ {A} → A → Stream A
repeat x = x ∷ ♯ repeat x

касательно Coinduction и его конструкторов — с точки зрения системы типов нормальными формами будут _описания_ нетерминируемых вычислительных процессов (так же как для системы типов нормальные формы IO — рассказы рантайму про то как делать IO).

В первом случае ⊥ (bottom type) совсем не про то и нужен чтобы из loop нельзя было попытаться достать результат (там ничего нет так как loop ничего никогда не возвращает) — можно и любой другой тип поставит, просто с пустым более правильно, во втором — про то, так как partiality monad это и есть модель вычислений с зависающими программами, в третьем — вообще ничего про тот или иной ⊥ нет.

Но нам не надо их запрещать.

В моём понимании алгоритмы финитны по времени и памяти по определению. Собственно, big O нотация про это. Поэтому именно алгоритмы которые виснут это что-то странное. Остальные программы — да, могут выполняться потенциально сколько угодно долго (но лучше чтобы всё ещё компактно), но их можно писать и типизировать без всяких ⊥.

Что значит не алгоритм?

http://en.wikipedia.org/wiki/Algorithm

More precisely, an algorithm is an effective method expressed as a finite list[1] of well-defined instructions[2] for calculating a function.[3] Starting from an initial state and initial input (perhaps empty),[4] the instructions describe a computation that, when executed, will proceed through a finite [5] number of well-defined successive states, eventually producing «output»[6] and terminating at a final ending state.

То есть как минимум 1) финитное вычисление, 2) имеет вход (будем считать пустой вход разновидностью), 3) имеет выход (не пустой), 4) реализует (является эффективным методом) какую-то _функцию_, точно и детерминировано или приближённо.

Например

% Есть вход, выход, завершаемость и функция -- алгоритм (обработки запросов).
handle(Request) -> Request + 1. % = Reply

% Нет входа, выхода, незавершаемо, нет функции -- не алгоритм, но программа
% (event-loop который дёргает уже алгоритм обработки запросов).
loop() -> receive {Client, Request} -> Client ! handle(Request) end, loop().

Задача программиста...

Это всё хорошо — разработка спецификаций (до написания кода, ага) и т.п. Но когда дело доходит до непосредственной реализации на _языке_ с определёнными свойствами, то

... может справиться обученная обезьяна на любом ЯП

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

Наличие гарантий доказать нельзя, значит гарантий нет

Ну пока компиляторы сами не верифицируются, можешь считать, что гарантией является то, что у 99% пользователей 99% времени на 99% кодовой базы разные clang, gcc и прочие scalac с ghc работают без перебоев.

И?

И запустить динамически типизированную программу на кучке тестов != покрыть всё что делает статическая система типов.

Однако при чем тут разговор о суммах?

Хочу сравнить сумму с этим U.

Приведи два куска кода которые это продемонстрируют — один поместит число в вектор строк, а другой выполнит IO из STM.

касательно Coinduction и его конструкторов — с точки зрения системы типов нормальными формами будут _описания_ нетерминируемых вычислительных процессов

Нам не нужны описания, нам нужен сам _процесс_. Утверждение вида «описание процесса удовлетворяет условию Х» бессодержательны. Нам требуются утверждения вида «процесс удовлетворяет условию Х». Системы типов без _|_ (здесь и далее будет называть их «бесполезные системы типов») не позволяют выносить утверждения о само процессе, только об описании. Но нам нужен некий способ соотносить описание с процессом. И тут мы возвращаемся к началу - если этот способ содержатален, то это эквивалентно _|_ в системе типов, а если неэквивалентно - либо мы теряем нужную выразительность, либо просто «верим» что оно вот так. Ну так верить можно и без типов.

В моём понимании алгоритмы финитны по времени и памяти по определению.

Ну в твоем понимании оно может быть как угодно, в суровой реальности это не так. И это как бы не проблемы реальности, это проблемы твоего подхода. Если он с реальностью не соотносится - им следует подтереть жопу.

То есть как минимум 1) финитное вычисление, 2) имеет вход (будем считать пустой вход разновидностью), 3) имеет выход (не пустой), 4) реализует (является эффективным методом) какую-то _функцию_, точно и детерминировано или приближённо.

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

Но когда дело доходит до непосредственной реализации на _языке_ с определёнными свойствами, то

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

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

Обезьяны прекрасно справляются и без статических проверок.

Ну пока компиляторы сами не верифицируются

Они и не могут - вот беда-то!

можешь считать, что гарантией является то, что у 99% пользователей 99% времени на 99% кодовой базы разные clang, gcc и прочие scalac с ghc работают без перебоев.

Эти гарантии ни чем не лучше «мое приложение проходит юнит-тесты».

И запустить динамически типизированную программу на кучке тестов != покрыть всё что делает статическая система типов.

Это всем ясно давно. Мы же хотим понять - в чем именно !=. Ну то есть может это неравенство чисто формально, но на практике не существенно. Никто, например, не применяет СТО в гидродинамике. Хотя по факту СТО правильнее. Но гидродинамические уравнения и так столь сложны, что все эффекты открываются чисто экспериментально (а потом описываются), но никак не выводятся математически. И если переписать их в СТО то придет пиздец полный вообще.

тип Х нельзя использовать в выражении, где требуется Y, не являющийся его надтипом.

$ cat test.c
char f(char x)
{
    return x + 1;
}

int main()
{
    int a = 1;
    return f(a);
}
$ gcc -Wall test.c
$ ./a.out

компилируется, работает и не ругается. С/C++ — не статический? Или char надтип для int?

Нам не нужны описания, нам нужен сам _процесс_

Ну пусть описание ~ процесс.

если этот способ содержатален, то это эквивалентно _|_ в системе типов

Что такое (значение!) «⊥ в системе типов»? Например, какой _смысл_ у значения ⊥ : Bool и зачем оно нужно (я хочу вернуть значение типа Bool но всё никак не могу осилить это сделать и возвращаю какую-то хрень?)? У ко-индуктивного типа SomeProcess могут быть _неравные_ термы neverReturnDoStuff1, neverReturnDoStuff2, ... : SomeProcess составленные с помощью ко-рекурсии, так же как и термы doStuffAndReturn1, doStuffAndReturn2, ... : SomeProcess, никаких ⊥ нет, так как нет уникального least элемента в poset-е значений типа SomeProcess. Ещё можно сочинить ко-индуктивный тип у которого _все_ термы neverReturn и могут быть различны. Если у какого-то типа X (например (A ⊥) из второго примера) и есть такой least, то это ⊥ именно типа X, его poset-а, но никак не всей системы типов, то есть он инкапсулирован, никому не мешает и ничего не ломает в логике системы типов.

Там требуется

and terminating at a final ending state

Или у Кнута в первом томе — «1) конечность» как конечное число шагов и «5) эффективность» — шаги просты и выполняются за конечные промежутки времени.

Ну и http://en.wikipedia.org/wiki/List_of_algorithms.

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

Твоя реальность такая суровая, что ты называешь сервера «алгоритмами»? :) Никто их так не называет — есть алгоритмы, есть программы, всё просто.

Обезьяны прекрасно справляются и без статических проверок.

Эти гарантии ни чем не лучше «мое приложение проходит юнит-тесты».

4.2 — не говори за всех.

gcc -Wall test.c

-Wconversion нужен.

Ну пусть описание ~ процесс.

Ну пусть pi = 4, так считать удобнее. Только, боюсь, самолеты падать начнут.

Что такое (значение!) «⊥ в системе типов»? Например, какой _смысл_ у значения ⊥ : Bool и зачем оно нужно (я хочу вернуть значение типа Bool но всё никак не могу осилить это сделать и возвращаю какую-то хрень?)?

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

Или у Кнута в первом томе — «1) конечность» как конечное число шагов и «5) эффективность» — шаги просты и выполняются за конечные промежутки времени.

Будьте внимательнее. Требуется, чтобы он в конечное состояние пришел за конечное число шагов. Иначе - выдал результат за конечное число шагов. Но виснуть ему никто не запрещает (в этом случае результата/конечного состояния нет, достигать за конечное число шагов нечего).

Твоя реальность такая суровая, что ты называешь сервера «алгоритмами»? :) Никто их так не называет — есть алгоритмы, есть программы, всё просто.

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

4.2 — не говори за всех.

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

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

Открою секрет - никаких строгих и четких формальных критериев «статичности» языков нет. Это вопрос соглашения.

Было уже что-то такое на SO: http://bit.ly/cux2i5

Пример оттуда:

##syntax of pfclike in clcode, start: 
  'foreach "(" [clqident]:id0 in [clexpr]:e ")" [clcode]:body0 '
{
 symbols(s1,id) {
  s1v='var'(s1);
  body = clike_renvar_code(body0, id0, id);
  .clike-code `{var \s1\ = ::expr \e\;
                do {
                  var \id\ = \s1v\->elt;
                  \body\;
                  ::lvalue \s1v\ = \s1v\->next;
                } while(\s1v\!=NULL)} `
}}

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

Ну пусть pi = 4

Отлично, то что я понимаю программу на си, например, как описание _будущего_ процесса работы процессора, памяти, системных и библиотечных вызовов это pi = 4.

более того - нам такие функции _нужны_

Ещё раз, «частичные грязные функции» это только _один из_ способов очертить всё множество полезных программ, «чистые тотальные функции» + «описания процессов» — другой возможный. Так что тут нет какой-то явной необходимости.

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

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

Будьте внимательнее.

Не вполне понял — для всех значений из ОДЗ получаются результаты за конечное число шагов (1), причём каждый шаг требует конечного времени (5). Вполне финитно по времени. Или речь об алгоритмах которые реализованы как программы (= частичные функции) которые работают как тотальные алгоритмы (= алгоритмы, собственно) на одних значениях и проявляют какое-то UB / GIGO на других? В таких случаях под ОДЗ алгоритма просто нужно понимать ровне те значения на которых он работает хорошо — эти UB и garbage нам не нужны.

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

http://www.tiobe.com/content/paperinfo/tpci/images/history_paradigm_type syst...

Или JavaScript vs. GWT, HaXe, Opa, Dart, TypeScript, Roy, Fay, etc.

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

Я не считаю что она худшая — в определённых случаях наоборот, например, примитивные веб-морды без обилия логики — о каких «ошибках» в них может быть речь? Они работают чисто номинально пока выглядят работающими, сам deploy по сути процесс тестирования. Или какая-то простая интерпретируемая скриптота — что-то не так с типам? Ну и ладно, всё равно это одноразовый однострочник который запускается сразу как был написан и либо отрабатывает как надо, либо нет.

Но как только появляется какая-то более сложная логика — даже чисто экспериментально, — попробуем поменять в большом проекте на статически типизированном языке сам тип, либо тип чего-нибудь (поля, аргумента), сдвинуть что-то в иерархии наследования, изменить саму эту иерархию — по всему проекту тут же появятся десятки несовпадений, без статических проверок все они будут отложены «до лучших времён» (то есть наоборот — ничего хорошего в перманентной ловле этих несовпадений нет).

Это песец как нечитаемо.

Отлично, то что я понимаю программу на си, например, как описание _будущего_ процесса работы процессора, памяти, системных и библиотечных вызовов это pi = 4.

То есть тот факт что самолеты падать будут тебя не смущает?

«чистые тотальные функции» + «описания процессов» — другой возможный.

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

Ничего хорошего из этого не получится — при интерпретации типов как логических утверждений

Ну и не надо. Нам ехать, а не шашечки.

В таких случаях под ОДЗ алгоритма просто нужно понимать ровне те значения на которых он работает хорошо — эти UB и garbage нам не нужны.

Замечательно. Т.о. любая частичная ф-я становится тотальной (сужением ОДЗ). А алгоритм сервера остается алгоритмом - тотальная ф-я с пустым ОДЗ.

http://www.tiobe.com/content/paperinfo/tpci/images/history_paradigm_type syst...

Ага. Так чем по-твоему объясняется взрывной рост популярности динамики в нулевых?

Я не считаю блаблабла

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

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

У меня теория другая - динамика популярна в вебе потому, что когда начался бум его развития, динамика уже _была_. Соответственно, люди могли выбрать наиболее подходящий (для реализации сложной логики) инструмент. То есть это была новая ниша и динамика ее заполнила. Потом рост закончился - т.к. в старых нишах куча статического легаси, а вытеснение инструмента из ниши на порядок сложнее, чем заполнение новой.