JavaScript надежность

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

Через явный typecase:

(defun flatten (x)
  (etypecase x ;; тут from top
    (null ())
    (atom `(,x))
    (list `(,@(flatten (first x)) ,@(flatten (rest x)))))) ;; тут to top

И во что превратились полиморфные id, map, compose и т.п.?

В лямбда-исчислении никаких id,map,compose нету. Есть только лямбда-термы. Берем лямбда-терм и убираем из него все типы.

Но вообще согласен, можно назвать такое «стиранием типов» (стирание же).

А ты что изначально подразумевал под «стиранием»?

Ну хорошо, вот точно _тот_ терм, насколько это возможно:

Так надо не насколько это возможно, а _точно тот_. (с точностью до синтаксиса, понятное дело). То есть надо убрать fromDynamic и toDyn.

Понятно же, что если пытаться делать так в списках forall a. a -> [a], без top и кастов (в лиспе-то у нас тоже top и поднятия / опускания типов, но из коробки, то есть автоматически), то это будет просто бред, а никакой не «тот же терм в лоб».

Почему бред? Это будет точно тот же терм. И он в соответствии с семантикой хаскеля (если бы она была) вполне корректно будет применяться к спискам и делать на них flatten с вполне корректным результатом (тем же, что в Scheme). Проблема только одна - система типов хаскеля слишком слаба и невыразительна, чтобы доказать корректность этого терма. То есть терм корректный - но средств доказательства нам не хватает. В идеале (если система типов эквивалентна пруверу) можно доказать корректность любого корректного терма, то есть такой флаттен напишется.

А вариант для гомогенного контейнера или списков с подтипированием [T] <: T в контексте для гетерогенности всё равно круче. По крайней мере, сигнатура Tree a => [a] или (a :> [a]) => [a] -> [a] более явная чем any -> [any] (или даже any -> any, или вообще any).

При чем тут сигнатура крутость и явность? Речь была о том, что есть синтаксически и семантически корректные термы, которые в слабой системе типов не чекаются, а в более сильной (те же термы) чекаются. Ты попросил пример - я привел пример.

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

Ну и что что он для них не работает? Мы же рассматриваем ULC, STLC, SystemF (<=2 rank). Там все работает (для ULC не работает, но там и типов нет и работать нечему, ясное дело).

Еще раз - разговор начался с того, что я констатировал очевидный факт - современные системы типов построены по «допускающему» критерию, то есть они могут отвергать корректные программы. Ты попросил пример таких корректных программ, я привел пример. (множество примеров). А теперь ты начал какие-то непонятные виляния жопой о том, что вот если бы рекурсивные типы, или если бы подтипы или еще какая-то хуйня. Так о том речь - ЕСЛИ БЫ ОНО БЫЛО. НО если этого нет - то терм не чекается. Хотя это правильный, хороший, годный терм. Любая система типов это ни что иное как некоторая теория в рамках которой можно доказывать корректность термов. Если теория хуевая - то есть много корректных термов, корректность которых в ней не доказывается (то есть система сильно неполна). Если теория лучше (полнее), то таких термов меньше. Если она совсем пиздатая - то их самый минимум.

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

А кого ебет твое мнение? Это по факту терм STLC с выводом типов. Он им является в соответствии с синтаксисом STLC с выводом типов, что формально строго доказывается. А думать ты себе что угодно можешь. Мы о фактах речь ведем, а не о чьих-либо мокрых фантазиях.

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

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

В лямбда-исчислении никаких id,map,compose нету.

Я имею в виду комбинаторы, которые by definition. Вот в System F:

id ≡ λ x : (∀ a . a) . x
id′ ≡ Λ a . λ x : a . x
compose ≡ Λ a . Λ b . Λ c . λ f : (b → c) . λ g : (a → b) . λ x : a . f (g x)

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

composeℕ ≡ ((compose ℕ) ℕ) ℕ

composeℕ
  def ⇒
((compose ℕ) ℕ) ℕ
  def ⇒
(((Λ a . Λ b . Λ c . λ f : (b → c) . λ g : (a → b) . λ x : a . f (g x)) ℕ) ℕ) ℕ
  Λ-β-reduction ⇒
λ f : (ℕ → ℕ) . λ g : (ℕ → ℕ) . λ x : ℕ . f (g x)

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

Берем лямбда-терм и убираем из него все типы.

И как из большой лямбды убрать типы?

А ты что изначально подразумевал под «стиранием»?

Тотальное синтаксическое соответствие. Оно есть для STLC → ULC, но нет для SystemF → STLC. То есть нельзя написать тотальную функцию SystemFTermRep → STLCTermRep, не добавив сюда контекст компиляции (чтобы проводить специализацию) или не обогатив STLCTermRep обобщёнными функциями (то есть представлениями типов, то есть рефлексией).

То есть надо убрать fromDynamic и toDyn.

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

На самом деле, если динамика моделируется как CCC с единственным объектом-доменом (причём, домен не может быть просто множеством, а термы функциями, то есть модель не может быть функтором из категорию Set, это должен быть функтор CPO → CCC), то в статике, где в CCC много объектов (которые перечисляются посредством теории типов как внутреннего языка этой категории), для «тех же термов» (динамических) необходимо и достаточно иметь среди объектов уникальный тип Top и уникальную коммутативную для всех типов диаграмму

∃₁ Top, ∀ A, ∃₁:

 Top

  ↓  ↖

1 + A ← A

(интересно, такая CCC как-то называется?)

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

Ты просто хочешь так думать, а на приведённый код на Scala/Haskell закрываешь глаза :)

То есть терм корректный - но средств доказательства нам не хватает

flt :: forall a. [a] -> [a]
flt [] = []
flt (x:xs) = flt x ++ flt xs

это не корректный терм, а форменный бред. Доказывается тем, что для каждого монотипа a (например flt_Int :: [Int] -> [Int]) это бред. _На самом деле_ у тебя тут

flt :: (a :> [a]) => [a] -> [a]
flt [] = []
flt (x:xs) = flt `wtf` x ++ flt xs

или, в частном случае:

flt :: [Dynamic] -> [Dynamic]
flt [] = []
flt (x:xs) = maybe [x] flt (fromDynamic x) ++ flt xs

(fromDynamic, toDyn и Just это три стрелки из той диаграммы, maybe - copairing) что статическая система типов с top типами (и безопасными подтипами вообще) позволяет _понять_ (я надеюсь).

В идеале (если система типов эквивалентна пруверу) можно доказать корректность любого корректного терма, то есть такой флаттен напишется.

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

Мы же рассматриваем ULC, STLC, SystemF (<=2 rank)

Я - нет, просто привёл первые попавшиеся примеры (причём с > 2 rank) подразумевая и «всё остальное». Привёл к тому что синтаксисы отличаются (как и прочие вещи).

множество примеров

id, Y и flatten?

что вот если бы рекурсивные типы, или если бы подтипы

Так это всё обычно и так есть.

Любая система типов это ни что иное как некоторая теория в рамках которой можно доказывать корректность термов.

В конструктивной теории типов любой существующий терм корректен с точки зрения этой теории, при этом является гражданином своего типа. Например, в каком смысле корректен flatten (если мы его таки написали)? В том что он доказывает (своим гражданством) что из дерева можно построить отображение в список? Вот если взять flatten населяющий тип {A : Set} {d n : ℕ} {_ : n ≤ 2 ^ d} → Tree d A → List n A, то такой flatten свидетельствует о том, что из бинарного дерева данной глубины можно построить список длины меньшей чем 2 ^ глубина, то есть всегда корректный (прошедший проверку типов) терм свидетельствует о своём утверждении, но и только, никто не гарантирует, что это не может быть неправильный flatten который, тем не менее, свидетельствует о том же утверждении. Чтобы доказать правильность flatten нужно целую теорию порядков городить.

Мы о фактах речь ведем, а не о чьих-либо мокрых фантазиях.

Ага, «о систем эф с зависающими программами».

Я имею в виду комбинаторы, которые by definition.

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

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

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

И как из большой лямбды убрать типы?

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

Тотальное синтаксическое соответствие.

А ну так оно как раз и есть между SystemF, STLC и ULC. Это уже мы обжевали, это математически доказанный факт, и больше к этому вопросу мы не возвращаемся.

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

Так я о том и говорю. Тот же самый терм - но не чекается в другой системе типов. Вот ты и сам пример привел.

Странно, что ты не понимаешь, что в статике нужны именно fromDynamic и toDyn

Так о том и идет речь, что в статике они нужны. И из-за этого тот корректный терм, который чекается в динамике, не чекается в статике.

На самом деле, если динамика моделируется

Вообще забудь про модели. Это все лишнее.

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

Но их нет. :(

Ты просто хочешь так думать, а на приведённый код на Scala/Haskell закрываешь глаза :)

Глаза ты закрываешь. Еще раз, о чем разговор - существуют корректные термы, которые чекаются в одной системе и не чекаются в другой. Я привел пример таких термов. Ты зачем-то взял, переписал эти термы и начал мне совать эти переписанные в лицо, говоря «смотри, вот эти другие термы чекаются!». Ну да, эти, ДРУГИЕ термы, чекаются. Но как это связано с предметом обсуждения? Ведь оригинальные - НЕ чекаются! А то, что КАКИЕ-ТО (никак не связанные с оригинальными) чекаются - ну в этом никто не сомневался. Ты мог бы привести например терм lambda x . x - он к flatten имеет точно такое же отношение, как и твои нелепые экзерсисы с toDyn.

это не корректный терм, а форменный бред. Доказывается тем, что для каждого монотипа a (например flt_Int :: [Int] -> [Int]) это бред.

Доказывается? Ну так докажи. Интересно будет посмотреть, как ты будешь опровергать экспериментально наблюдаемый факт (корректность флаттена - как раз таковой факт и есть). Давай-давай, доказывай, а я посмеюсь :)

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

Пруверы при том, что, еще раз, с прувером можно доказать корректность _любого_ корректного терма. Нам известно, что терм flatten корректен - значит с прувером его корректность доказывается. Что тут непонятного? flatten : (Forall (A) (Rec (X) (U X (Listof X))) -> (Listof A) where (not (A = (Listof B) for any B))) вот тебе типа для flatten.

Я - нет

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

id, Y и flatten?

А сколько тебе надо? десять? сотню? Тысячу? Очевидно, можно написать генератор, который тебе нагенерит любое количество примеров автоматом. Ну на базе того же flatten'а.

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

Например, в каком смысле корректен flatten (если мы его таки написали)? В том что он доказывает (своим гражданством) что из дерева можно построить отображение в список?

Конечно, нет. Тем фактом, что он редуцируется. А «из дерева можно построить список» - это уже про типы, это лишнее. Любой редуцируемый тип - корректен. Вот терм 2+«2» не редуцируется. Он некорректен. И 1/0 - не редуцируется. Он некорректен (но система типов его не отвергает). А вот flatten - редуцируется. Он корректен. Но система типов его отвергает.

Чтобы доказать правильность flatten нужно целую теорию порядков городить.

Исключительно в твоих мокрых фантазиях. У нормальных людей доказательства в две строки, безо всяких «теорий порядков».

Убираем всю большую лямбду

Выразительность теряется же.

Мы же типы выводим.

Собеседника не слушай @ одно и то же пиши :)

ну так оно как раз и есть

Так я о том и говорю.

Ээ... На два утверждения о том что тотального соответствия нет ты говоришь «да» и «нет».

Так о том и идет речь, что в статике они нужны.

flatten x =
  (cond (not (pair x))
        (list x)
        (cond (null x)
              nil
              (append (flatten (car x)) (flatten (cdr x)))))

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

При этом все динамические функции тут тотальны, это можно контролировать, в отличии от (хотя всё равно - нафига так неспецифично писать, когда любая штука это T или T -> T).

Но их нет. :(

Зря мужики скалу пилили, получается.

Я привел пример таких термов.

Ты повсюду выдаешь программы на «js» за программы на «си», подразумевая, что типы появятся сами чудесным образом (а типы высших порядков тебе просто не нужны и ты их синтаксис не считаешь за синтаксис).

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

Жду flatten на Agda2.

определения функций не привожу

Кстати, а quote нет. И eval с макросами. «Корректные термы» не чекаются!1 ;)

Вот терм 2+«2» не редуцируется.

Не факт.

И 1/0 - не редуцируется

Тоже не факт.

У меня есть ощущение что большинству лоровцев функциональные языки мозг съели, так что они даже не способны почитать о чем тема. Превратили обсуждение в очередной лиспо-хацкеля срач. Жалко ЛОР толком не модерируется(

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

Любой топик, косвенно задевающий типизацию, гарантированно скатывается в лиспосрач. Местные обыватели это прекрасно знают и сразу переходят к лиспосрачу, пропуская обсуждение непосредственно топика.

Жалко ЛОР толком не модерируется(

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

Выразительность теряется же.

С чего вдруг?

Собеседника не слушай @ одно и то же пиши :)

Ну да, вот вы не слушаете собеседника и ему приходится раз за разом писать одно и то де :)

Ээ... На два утверждения о том что тотального соответствия нет ты говоришь «да» и «нет».

Где я говорил «нет»? Нигде не говорил. Между рассматриваемыми системами (ULC, STLC, SystemF<2) тотальное соответствие синтаксиса и семантики есть. А вот соответствия типов - нет. Корректность терма зависит только от семантики (от того можно ли редуцировать терм), но не от системы типов, вот и получается что множества корректных термов для этих систем совпадают, а вот множества чекаемых термов - нет.

определения функций не привожу

Без определения соответствующих ф-й это НЕ терм ни одной из рассматриваемых систем. Вы просто написали потом символов, который (чисто случайно) совпадает с потоком символов, которым мы кодируем тот же терм в лиспе, но поскольку семантика символов совершенно иная, ваше утверждение не имеет смысла. Повторяю, подобного рода утверждения не более содержательны, чем утверждения о том, что чекаются КАКОЙ-НИБУДЬ терм. Потому что приведенный вами терм имеет отношение к flatten не боле чем любой другой. Например терм «2+2». Он чекается? Чекается. Но как это относится к предмету разговора?

Зря мужики скалу пилили, получается.

Почему же зря? Вообще flatten ни в одной из распространенных систем не чекается, для его чека нужно три вещи: 1. рекурсивные типы, 2. подтипирование с объединениями, 3. not-типы (если взять occurence typing из Racket и разрешить его произвольное расширение за счет деклараций - оно и будет). Первые два пункта в сущности штуки простые и распространенные, а вот с третим - беда.

Кстати, с точки зрения модели, категория для типов с объединениями и подтипированием ведь будет топосом? Тут надо правда отметить еще одну вещь - предикат идет на тип с кайндом * -> * (List), то есть, вообще говоря, топосом должна быть не только категория монотипов, но и высшие категории.

Ты повсюду выдаешь программы на «js» за программы на «си», подразумевая, что типы появятся сами чудесным образом

(а типы высших порядков тебе просто не нужны и ты их синтаксис не считаешь за синтаксис).

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

Жду flatten на Agda2.

Зачем агда? Агда это язык с зависимыми типами, а не прувер. То есть в качестве прувера его использовать _можно_ но зачем надевать штаны через голову? Можно же взять полноценный динамически-типизированный прувер на полноценном динамически-типизированном лиспе - ACL2.

С чего вдруг?

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

Между рассматриваемыми системами (ULC, STLC, SystemF<2) тотальное соответствие синтаксиса и семантики есть.

Соответствие тотально если функция его задающая тотальна, то есть определена для всех элементов своего домена. По крайней мере ULC -> STLC/SystemF (пример - Y) и SystemF -> STLC/ULC (примеры - большие лямбды) не тотальны.

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

Корректность терма зависит только от семантики (от того можно ли редуцировать терм), но не от системы типов

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

Возможно, в заблуждения вводят реальные языки вроде Haskell, которые синтаксически настолько богаты, что достаточно далеки от формальных STLC или SystemF и позволяют писать термы которые похожи на, скажем, термы лиспа. Но только похожи, это _не те_ термы. _Те_ это с использованием top type. Поясняется просто - flatten в лиспе это _хорошая_ функция именно на уровне редукций, она не пытается, например, конкатенировать числа или доставать car из числа, такие у неё свойства. Однако, если писать flatten в Haskell для гомогенных списков каких-то простых монотипов, то получится функция обладающая _плохими_ свойствами (1 ++ [], например, то есть прямо на уровне редукций), то есть _другими_, то есть не _та_. Функция обладающая _теми же_ свойствами, то есть _та_, это функция на гетерогенных списках - Dynamic, [Dynamic] или a :> [a] => [a] -> [a]. То есть либо с универсальным типом (в отличии от «простых» монотипов), либо со сложным контекстом (фактически, как раз SystemFCшная фича) задающим правило для подтипов (и универсальный тип со своими списками как первый очевидный инстанс такого правила).

Или вот агда. Язык должен быть строго-нормализирован. На практике это приводит к необходимости решать проблему останова не для строго-нормализированного языка (для которого она разрешима), а для субстрата на котором пишется программа, то есть для языка для которого эта проблема неразрешима. В итоге termination cheker (чтобы не зависать) ограничивает возможную рекурсию до структурной (гарантированно терминируемой, доказуемо за конечное время) и отбрасывает вместе с нетерминируемыми программами и некоторые терминируемые, но не WF рекурсивные - например, quicksort или depth и flatten для деревьев общего вида. Так что flatten там пишется нетривиально (если конечно, просто не отключить termination cheker, что тоже можно сделать).

Потому что приведенный вами терм имеет отношение к flatten не боле чем любой другой.

Можешь поверить на слово - это именно _тот_ терм.

Почему же зря?

Просто для перевода один в один любого кода, в том числе flatten, с изначального лиспа МакКарти (за исключением quote) на Haskell(GHC)/Scala (C/C++, в конце концов) достаточно Dynamic/Any (void*/lispobj / any/superclass). Всё. Остальное может и интересно в контексте Racket и того чем его разработчики занимаются, но не имеет к теме «динамические термы в статике» отношения.

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

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

так же как это в хаскеле сделано, например.

В хаскеле никто не использует чистый H98. Даже ST нужны rank-2-types. С активным использованием прочих расширений (а они используются) типы выводятся через раз. В Scala ещё хуже выводятся.

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

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

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

Так я и пытаюсь вам это объяснить, а вы все никак не поймете. Множества синтаксически корректных термов у ULC, SystemF<2+TI, STLC+TI _совпадают_.

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

Нет, соответствие синтаксиса и семантики есть только в том случае, если совпадает грамматика и операционная семантика. У ULC, STLC+TI, SystemF<2+TI грамматика и операционная семантика совпадают.

Ну то есть Y для тебя «корректный» терм в STLC и SystemF

Естественно. А какие причины считать его некорректным?

Но только похожи, это _не те_ термы. _

Так я это и талдычу уже сколько - это _не те_ термы. Ваш флаттен - это _не тот_ терм.

получится функция обладающая _плохими_ свойствами (1 ++ [], например, то есть прямо на уровне редукций), то есть _другими_, то есть не _та_... Функция обладающая _теми же_ свойствами, то есть _та_, это функция на гетерогенных списках - Dynamic, [Dynamic] или a :> [a] => [a] -> [a].

Какие еще функции? Я не говорил ни о каких функциях. Речь шла исключительно О ТЕРМАХ ЯЗЫКА. Совпадать или не совпадать могут лишь термы, а как вы вообще пытаетесь рассуждать о функциях? Лисповый flatten - это никакая не функция, это просто терм, который может определенным образом редуцироваться (то есть задана операционная семантика). Для того чтобы изучать его на уровне ф-й нам надо рассматривать денотационную семантику, но поскольку задать ее можно всегда произвольным образом, она не несет никакого смысла, мы ее и не рассматриваем. Так что никаких функций - только термы и редукции. Условно говоря, flatten в лиспе и хаскеле не такой еще и из-за ленивой семантики, так что мы тут рассматирваем либо условно-ленивый лисп, либо условно-энергичный хаскель (но до этого я сей аспект не упоминал, т.к. он не существенен в рамках нашего обсуждения).

Так что flatten там пишется нетривиально

Если там нет not-типов, он вообще не пишется.

Можешь поверить на слово - это именно _тот_ терм.

То есть я должен поверить на слово, что «2+2» - это тот же терм, что и flatten? С какой такой стати?

Просто для перевода один в один любого кода

Так это не перевод один в один. Если это перевод один в один, то после обратного перевода должен получиться оригинал. А у нас оригинала не получится. Или у вас тогда получится что ваша функция перевода неинъективно.

Топос может быть достаточен для чего угодно

Это ясно. Я просто говорю о том, будет ли по факту указанная категория топосом (ну если строить ее по такой же схеме, как строим категорию Hask, например)?

В хаскеле никто не использует чистый H98.

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

Так он существует только на уровне типов.

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

Значит выразительность строго совпадает.

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

Так я и пытаюсь вам это объяснить, а вы все никак не поймете.

И как определена тотальная функция ulc2stlc на терме Y которого нет в STLC? Или systemF2ulc на терме (bigLambda x . ...)?

Множества синтаксически корректных термов у ULC, SystemF<2+TI, STLC+TI _совпадают_.

Я понимаю что ты в данном случае хочешь сказать (суффиксы <2+TI и +TI намекают), но это просто какое-то нехорошее представление о том что такое синтаксис. Это просто свидетельствует о существовании у этих систем общего субстрата (лямбда без типов) относительно которого типизированные лямбды отбрасывают логически ущербные конструкции (самоприменение, fix, зависающие термы и т.п.), но и добавляют разные формы рассуждения (язык типов) о корректности позволительных конструкций. Любая типизированная лямбда + общая рекурсия + top так и вовсе ничем не слабее нетипизированной (так как допускает и общую рекурсию, и динамические программы over top type).

если совпадает грамматика

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

А какие причины считать его некорректным?

Он не пишется. Его существование противоречило бы свойству строгой нормализации данных систем. Он пишется только в нетипизированном субстрате из которого можно попытаться получить типизированный вариант, и, что характерно, это не получится (придётся разрешать уравнение a = a -> a).

Какие еще функции?

flatten - рекурсивная функция. В лиспе тоже. Поэтому (_define_ (flatten x) ...). Точно так же flatten x _=_ ...

Лисповый flatten - это никакая не функция, это просто терм

То есть хочется извратиться и написать flatten через голую лямбду? Через Y? Как? Ну и не вижу проблемы сделать то же самое в хаселе.

То есть я должен поверить на слово, что «2+2» - это тот же терм, что и flatten? С какой такой стати?

Там не «2+2», а вполне конкретный flatten. Это ещё не понятно? А почему? Потому что ты не знаешь хаскеля (или особенностей Data.Dynamic)? Что тогда вообще обсуждать?

А у нас оригинала не получится.

Почему, получается.

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

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

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

Я просто говорю о том, будет ли по факту указанная категория топосом

Если интерпретировать подтипы по аналогии с подмножествами в Set, то нужны power object-ы, но не обязательно топос. Например, топос - CCC, но CCC (как доктрина для простой лямбды) + power object-ы - не топос. Топос - LCCC, и в LCCC (как доктрине для зависимых типов) есть все конечные пределы, так что LCCC + power object-ы - топос.

Если там нет not-типов, он вообще не пишется.

А что такое not-типы?

type Not a = a -> Void

? Конечно, в хаскеле бессмысленно, так как Void можно населить любой ерундой. В агде

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ P = P → ⊥

Ну ок, с полиморфной лямбдой ещё можно так обходиться.

Ну и хорошо :)

С любым языком в котором типы не умирают и продолжают работать в рантайме - уже нет.

Но поскольку мы не такой язык рассматривали - это и не важно.

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

Мы же говорим об интерпретации, а не о компиляции, т.к. операционная семантика задает именно правила интерпретации. Нету никакого машинного кода.

И как определена тотальная функция ulc2stlc на терме Y которого нет в STLC?

Так он есть в STLC+TI.

Или systemF2ulc на терме (bigLambda x . ...)?

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

Это просто свидетельствует о существовании у этих систем общего субстрата

Это уже софистика. Смотри на факты - берем STLC с выводом типов и видим, что множества термов будут совпадать с множеством термов ULC.

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

Да.

Он не пишется.

Он пишется.

Его существование противоречило бы свойству строгой нормализации данных систем.

С чего вдруг? Система типов ведь этот терм не пропустит. Хотя он _пишется_. Пишется - значит является синтаксически корректным.

flatten - рекурсивная функция. В лиспе тоже.

Да нет, никакая это не функция. Это терм языка. А то что он _может_ обозначать функция - ну так надо сперва задать денотационную семантику.

То есть хочется извратиться и написать flatten через голую лямбду? Через Y? Как? Ну и не вижу проблемы сделать то же самое в хаселе.

Да не важно как. Важно что в языке функций нет. Есть только термы. А функций - нет. Ну нет и все. Функция - это математический объект, бинарное отношение блаблабла. А у нас - последовательность символов некоторого алфавита. Ну каким местом последовательность символов является бинарным отношением? Чепуха же.

Там не «2+2», а вполне конкретный flatten.

Там нечто имеющее отношение к лисповому flatten точно такое же, как и «2+2». Если вы хотите доказать, что то, что вы написали, - это лисповый flatten, то докажите, что «2+2» - лисповый flatten. Задачи совершенно аналогичные.

Почему, получается.

Нет :( Если ваш терм перевести, то там будут toDyn fromDyn, которых не было в оригинале. Ну и структура Dynamic появится, который в оригинале тоже не было.

Конечно, так может быть.

Ну и все о чем разговор тогда?

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

Естественно. Это очевидный факт.

Что странно, потому что обычной динамике кроме top ничего и не нужно.

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

Если интерпретировать подтипы по аналогии с подмножествами в Set, то нужны power object-ы, но не обязательно топос.

А чем она собственно НЕ топос?

А что такое not-типы?

Ну что-то такое: (not String) = Top / String. То есть «что угодно, но не строка».

Так он есть в STLC+TI.

Где?

y = \f -> (\x -> f (x x)) (\x -> f (x x))

это терм ULC который TI не разрешает в терм STLC, ещё при том, что надо бы писать

y = \(f :: ?) -> (\(x :: ?) -> f (x x)) (\(x :: ?) -> f (x x))

то есть непосредственно терм STLC, тогда вообще плохо становится.

А такого терма нигде нет

Он есть в SystemF. Хочется построить тотальное отображение _из_ SystemF - нужно считать все её термы, а не только те которые хочется считать, конвенционально. TI это отображение _в_ SystemF. Большую лямбду можно только выкинуть, если делать _из_, то есть это будет частичное отображение.

Видим одно и то же?

Да.

Число множественное. Я вижу разницу в грамматике этих трёх систем, ты - нет. Итого - нет, не видим одно и то же. Но правда же одна, правда? ;)

Система типов ведь этот терм не пропустит. Хотя он _пишется_. Пишется - значит является синтаксически корректным.

Для меня «терм теории» это хороший с точки логики (теории типов) данной теории терм. То есть не важно что там «пишется», 1 + «2» тоже «пишется», так же как и ,!k@l#;$f%l^, это термы типизированной лямбды с числами, строками и сложением чисел или нет? Также не важно какие есть _другие_ теории в которых есть _подобные_ термы и из которых, _возможно_, существуют частичные или тотальные отображения в данную теорию. Имеет значение синтаксис с логикой только лишь рассматриваемой теории.

Да не важно как.

Нет кода - нет перевода.

Там нечто имеющее отношение к лисповому flatten точно такое же, как и «2+2».

Там нечто, что склеивает вложенные списки в плоские и работает по такому же принципу как работает лисп (и вообще динамический язык). «2+2» не склеивает списков и никак не демонстрирует особенностей работы динамики.

там будут toDyn fromDyn, которых не было в оригинале.

Всё есть в оригинале, и под капотом, и явно.

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

А зачем что-то эмулировать? Тупо вводим top с кастами и пишем как в динамике какой-то динамический код.

А чем она собственно НЕ топос?

Если отсутствуют какие-то пределы, например.

То есть «что угодно, но не строка».

Зачем так жить? Противоречивая система же получится, в конце концов (так как эта штука не является типом, а является классом, но при этом используется как тип).

это терм ULC который TI не разрешает

Так тот факт, что TI его не разрешает, как раз говорит о том, что это синтаксически корректный терм STLC+TI :)

То есть терм пишется. Но не чекается (т.к. TI его не разрешает). Пишется = терм можно подать на вход TI, чекается = TI выводит тип (корректно отрабатывает).

то есть непосредственно терм STLC, тогда вообще плохо становится.

Да, становится, но мы и не говорим о «непосредственно термах STLC».

Он есть в SystemF. Хочется построить тотальное отображение _из_ SystemF - нужно считать все её термы

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

, а не только те которые хочется считать, конвенционально.

А почему, собственно? Я могу выбрать такую систему типов, какую мне хочется, вот я выбрал именно выводимое подмножество SystemF (то есть SystemF<2).

Число множественное. Я вижу разницу в грамматике этих трёх систем, ты - нет. Итого - нет, не видим одно и то же. Но правда же одна, правда? ;)

Ну так мы не те системы сравниваем. Я беру системы c TI, вы - без TI.

Для меня «терм теории» это хороший с точки логики (теории типов) данной теории терм. То есть не важно что там «пишется», 1 + «2» тоже «пишется», так же как и ,!k@l#;$f%l^, это термы типизированной лямбды с числами, строками и сложением чисел или нет?

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

Имеет значение синтаксис с логикой только лишь рассматриваемой теории.

Но мы то как раз рассматриваем одни и те же термы в ЯП с разными теориями. И речь идет именно о том, что терм осмысленно в одной теории, но неосмысленен - в другой.

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

Нам надо определиться, что мы считаем «переводом терма». Я думаю, логично считать А переводом Б, если при обратном переводе Б мы получаем терм эквивалентный (в смысле отношения эквивалентности по редукции к одному терму) А. В случае с твоим флаттеном в хаскеле мы НЕ получаем терм эквивалентный исходному флаттену лиспа.

Всё есть в оригинале, и под капотом, и явно.

Явно там уж точно никаких toDyn fromDyn нету, а под капотом ничего нету ровно потому, что мы ведем речь о ТЕРМАХ. Не о том, во что они компиляруются, а о самих термах и только о них (возможно, они вообще никуда не компилируются а лишь интерпретируются) и никакого «под капотом» там просто НЕТ.

А зачем что-то эмулировать?

Ну если чего-то в системе типов нет, то приходится эмулировать это имеющимися средствами (вот твои fromDyn toDyn - это и есть эмуляция).

Тупо вводим top с кастами и пишем как в динамике какой-то динамический код.

Если мы введем топ с кастами - это будет другая система типов. Ну и рекурсивные типы все еще нужны (либо fix, либо возможность записать явную рекурсию f x = f .., что эквивалентно).

Если отсутствуют какие-то пределы, например.

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

Зачем так жить? Противоречивая система же получится

С чего вдруг?

(так как эта штука не является типом, а является классом, но при этом используется как тип)

С чего вдруг она не является типом? Тип - это множество значений. Строка - множество значений, то есть это тип, топ - тоже тип, значит (не строка) = (топ / строка) - это тоже тип. При чем тут классы вообще непонятно, т.к. в рассматирваемой системе вообще нету никаких классов. Ну и в любом случае чтобы написать в статике flatten нам _нужны_ not-типы (т.к. для того чтобы чекер все пропустил он должен знать, что в одной из веток условия переменная не может быть парой, то есть имеет тип (not pair)). Если любая теория с not-типами противоречива, значит флаттен пишется только в противоречивой теории, да :)

Пишется = терм можно подать на вход TI, чекается = TI выводит тип

На вход как раз подаётся терм ULC, в котором никаких типов вообще нет. На выходе может получиться терм STLC (= с явными типами). Причём для Y на входе не может получиться корректный терм на выходе (частичность отношения вывода).

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

Это не интересно, такое подмножество отличается от STLC только наличием возможности сделать один единственный forall, то есть просто объединить семейство мономорфных функций в одну полиморфную (практически сахар - макросы с шаблонами так могут делать).

А вот из полной SystemF будет частичное отношение стирания в STLC с отбрасыванием всей type level экспрессии. Из STLC в ULC - будет уже тотально.

Ну да именно так, все эти термы «пишутся» - то есть соответствуют грамматике.

Это такая приЯПшнутая точка зрения, то есть, да, если взять грамматику

term ::= integer | string | variable | apply term term | ...

то есть общую часть ULC, STLC и SystemF с числами и строками, то соответствующий парсер будет разбирать строки вида

(apply 1 "2")

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

Явно там уж точно никаких toDyn fromDyn нету

А если я перегружу числа и строки, так чтобы писать просто 1 и «2» вместо toDyn 1 и toDyn «2», допущу возможность перегрузить списки (в GHC этого нельзя сделать, но можно писать (cons 1 (cons «2» (cons ... nil))) или (cons 1 «2»)), а fromDynamic спрячу за функциями которые будут соответствовать лисповым специальным формам и примитивным функциями (и то и другое дано «как есть»)? Некий лисп (некий = без quote) переводится в хаскель с такими функциями, хаскель с такими функциями переводится в некий лисп. В чём проблема?

Если мы введем топ с кастами - это будет другая система типов.

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

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

Простое LC без развитой квантификации (читай, без зависимых типов) будет интернализироваться в доктрине CCC, то есть в категории бедной на конечные пределы.

топ - тоже тип

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

{-# OPTIONS --type-in-type --injective-type-constructors #-}

module Russell where

open import Data.Empty
open import Data.Unit
open import Relation.Nullary

data J (F : Set → Set) : Set where
  j : F ⊤ → J F

data R : Set → Set where
  r : {F : Set → Set} → ¬ F (J F) → R (J F)

self : ¬ R (J R)
self (r f) = f (r f)

absurd : ⊥
absurd = self (r self)

--type-in-type --injective-type-constructors

Без инъективных конструкторов self типизируется но не пишется. Без больших типов self вообще не типизируется (R (J R)), так как R хочет быть классом (Set → Set₁).

Это не интересно, такое подмножество отличается от STLC только наличием возможности сделать один единственный forall, то есть просто объединить семейство мономорфных функций в одну полиморфную (практически сахар - макросы с шаблонами так могут делать).

Так собственно все интересное что есть в SystemF - это как раз и есть возможность сделать этот forall. Любая система типов - не более чем сахар над UTLC :)

Это такая приЯПшнутая точка зрения

Так мы о языках программирования и говорим.

Но в логике

Мы говорим не о логике, мы говорим о ЯП.

А если я перегружу

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

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

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

Да, это будет динамика встроенная в статику.

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

Вот я и не понимаю чем такой язык плох и что в нём «пишется, но не чекается».

Например, flatten пишется, но не чекается :)

Простое LC без развитой квантификации (читай, без зависимых типов) будет интернализироваться в доктрине CCC, то есть в категории бедной на конечные пределы.

то есть для пределов обязательно нужны зависимые типы? Почему? Можно где-то увидеть доказательство этого факта?

Топ, по идее, тоже плохой тип, так как является «множеством всех множеств» (включает термы всех типов).

Он является объединением множеств некоей совокупности, не вижу тут никакой проблемы. В конце концов, он даже счетен.

В «достаточно богатой» теории это приведёт к противоречиям, так как такое «множество» слишком большое и должно быть классом.

С чего бы оно большое? Оно вообще счетное у нас.

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

Не тип всех типов, а тип всех термов :))

Можно где-то увидеть доказательство этого факта?

Нужно где-то достать книжку про слоника (Sketches of an Elephant: A Topos Theory Compendium), там есть пара небольших отступлений про то почему CCC - не Lex (и CCC которые Lex специально обзывают properly CCC, + PO = будет топос, также LCCC). Ну и можно задаться вопросом о том как строить PO не в Lex.

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

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

В конце концов, он даже счетен.

Как он может быть счётен когда полно простых несчётных типов?

Ну или может быть теорема «такой-то тип несчётен» (а такие типы есть, так как есть множества с мощностью > |ℕ|), в «достаточно богатом» языке эта теорема должна доказываться, а сам тип - быть элементом universal setproper class.

С чего бы оно большое?

Почему universal set as set приводит к парадоксам (вроде Russell) и как с этим борются ZF/NBG/SEAR/ETCS/теории типов/etc.? Такой вопрос?

Это динамика и есть

Ну вот. Только ещё любой терм (статического) типа автоматически превращается в (динамический) терм типа Any. То есть некий кусок статики «универсально пропускается» через Any, а на уровне Any чекать почти нечего. То есть, например, add : Any -> Any -> Any, что тут проверять? Можно сделать add(1, «2») => exception или add(1, «2») => None (типа Any).

flatten пишется, но не чекается

А напиши тогда на Scala или Haskell, чтобы было понятно, что не нравится (что не чекается). На Haskell нужно сначала задаться вопросом что такое гетерогенные вложенные списки (явно _не_ forall a. [a]), для Scala это будет просто

> List(1, List(Some('2'), null), "2")
res1: List[Any] = List(1, List(Some(2), null), 2)

Даже тип выводится. В Haskell, в принципе, будет то же самое, но с явными кастами в Dynamic (кроме чисел и строк).

Такой вопрос?

Видимо, совсем другой. Зря я про Top как про «плохой» тип заговорил ─ перепутал с универсумом типов как типом. Последнее действительно может приводить к парадоксам, только универсум U это _класс_ содержащий как населённые так и ненаселённые типы, тогда как Top ─ _тип_ содержащий только термы (населённых типов):

  U                              Top
  +---------------------------+  +--------------------------+
  | inhabited types / truth   |  | union of inhabited types |
  +---------------------------+  +--------------------------+
  | uninhabited types / false |
  +---------------------------+

  Martin-Löf impredicativity:    (U, ⊆) as (preordered) directed universum

    U : U                          ⇓

    ⇓                              Subtyping + top type (Top : U, the top element of the preorder).

    Girard's (Russell's, etc.) paradoxes.

Сам Top несчётный и всё такое, но вполне обычный тип. Большие типы большие не своей мощностью, а местом в кумулятивной иерархии, например, может быть пустой класс:

data ⊥₁ : Set₁ where

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

Возвращаясь к отношению подтипирования ─ его можно определить непосредственно через поднятия и опускания типов:

-- * Subtype relation via upper/lower casts.
-- 
-- If A ⊆ B:
-- 
--        ↑_
--     B  ←  A
--           
--     ↓_ ↘  ↓   ↘ f
--           
--   (just) A+1  →  C (maybe f c)
--               
--   nothing ↑   ↗ c
-- 
--           1
-- 
record _⊆_ {a} (A B : Set a) : Set a where
  field
    ↑ : A → B
    ↓ : B → Maybe A

и доказать, что (Set, ⊆) образует предпорядок вполне естественным образом (то есть без принятия каких-то дополнительных аксиом):

-- * ∀ (a : Level). (Set a, ⊆) as a level-indexed hierarchy of preordered universes.

A⊆A : ∀ {a} {A : Set a} → A ⊆ A
A⊆A = record { ↑ = id; ↓ = just }

open _⊆_

⊆-is-preorder : ∀ {a} → IsPreorder {suc a} {suc a} {a} _≡_ _⊆_
⊆-is-preorder = record
  { isEquivalence = isEquivalence
  ; reflexive = λ eq → subst₂ _⊆_ refl eq A⊆A
  ; trans = λ A⊆B B⊆C → record
    { ↑ = ↑ B⊆C ∘ ↑ A⊆B
    ; ↓ = maybe′ (↓ A⊆B) nothing ∘ ↓ B⊆C
    }
  }

⊆-preorder : Preorder _ _ _
⊆-preorder = record
  { Carrier = Set
  ; _≈_ = _≡_
  ; _∼_ = _⊆_
  ; isPreorder = ⊆-is-preorder
  }

Но до частичного или полного порядка это не обобщается:

-- * Antisymmetry (partially/totally ordered universes)?
-- 
--   ∃ (A B : Set). A ⊆ B ∧ B ⊆ A ∧ A ≢ B ?
-- 
module Non-DAG-Types where

  mutual
    record A : Set where field a : ⊤ ; b-in-a : B
    record B : Set where field b : Bool ; a-in-b : ∞ A

  open A
  open B

  just₀ : {T : Set} → T → Maybe {zero} T
  just₀ = just

  A⊆B : A ⊆ B
  A⊆B = record { ↑ = b-in-a ; ↓ = just₀ ∘ ♭ ∘ a-in-b }

  B⊆A : B ⊆ A
  B⊆A = record { ↑ = ♭ ∘ a-in-b ; ↓ = just₀ ∘ b-in-a }

кроме того, A и B не биективны.

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

-- * (Set, ⊆) as directed (via Top) universe.
-- 
--            Top
--            ...
--        X ⊆ Z    Y ⊆ Z
--          B ⊆ Y    C ⊆ Y
-- A ⊆ X    B ⊆ X
-- 
postulate
  Top : Set
  Top-⊆ : ∀ {A} → A ⊆ Top

и дальше, так что Top ведёт себя как некий терминальный объект:

open IsPreorder renaming ( refl to refl′ )

Top-⊆-Top : Top ⊆ Top × Top ⊆ Top
Top-⊆-Top = refl′ ⊆-is-preorder {Top} , Top-⊆ {Top}

open Preorder

Maximal : ∀ {c ℓ₁ ℓ₂} (p : Preorder c ℓ₁ ℓ₂) → Carrier p → Set (c ⊔ ℓ₂)
Maximal p x = ∀ (y : Carrier p) → _∼_ p x y → _∼_ p y x

Top-is-Maximal : Maximal ⊆-preorder Top
Top-is-Maximal _ _ = Top-⊆

Terminal : ∀ {a} → Set a → Set (suc a)
Terminal {a} X = ∀ {A : Set a} → A → X

-- | Top as terminal object.
Top-↑ : Terminal Top
Top-↑ = ↑ Top-⊆

FooBar : ∀ {a} → Set a → Set (suc a)
FooBar {a} X = ∀ {A : Set a} → X → Maybe A

-- Top as what?
Top-↓ : FooBar Top
Top-↓ = ↓ Top-⊆

либо искать какую-то естественную конструкцию для Top (вроде универсальной квантификации, предикатов, etc.). Её даже нужно искать, так как аксиомы чисто символические, порассуждать, например, об инъективности отображений в Top без естественных конструкций не получится.

В общем, если бинарное отношение подтипирования на универсуме и соответствующий предпорядок получаются очевидно, то частичный, тотальный, направленный порядок, существование и единственность верхнего элемента ─ всё требует отдельного обоснования.

В общем, если бинарное отношение подтипирования на универсуме и соответствующий предпорядок получаются очевидно

В quotes :)

мимопроходил

Как он может быть счётен когда полно простых несчётных типов?

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

Ну или может быть теорема «такой-то тип несчётен» (а такие типы есть, так как есть множества с мощностью > |ℕ|), в «достаточно богатом» языке эта теорема должна доказываться, а сам тип - быть элементом universal setproper class.

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

Почему universal set as set приводит к парадоксам (вроде Russell) и как с этим борются ZF/NBG/SEAR/ETCS/теории типов/etc.? Такой вопрос?

у нас же в плане термов не может быть set of set, есть вычислимые set of вычислимых set.

Каких еще несчетных типов?

К примеру, http://code.haskell.org/~dolio/agda-share/Diag.agda - последний комментарий.

А напиши тогда на Scala или Haskell, чтобы было понятно, что не нравится (что не чекается).

просто тот же терм 1в1 (с поправкой на синтаксис)

flatten [] = []
flatten (x:xs) = append (flatten x) (flatten xs)
flatten x = [x]

К примеру, http://code.haskell.org/~dolio/agda-share/Diag.agda - последний комментарий.

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

Сам Top несчётный и всё такое

Мы уже, по-моему, договорились, что Top - тип, содержащий _все термы_. Множество _всех термов_ - счетно (если только не допустить термы над несчетным алфавитом, но у нас он счетен).

Возвращаясь к отношению подтипирования ─ его можно определить непосредственно через поднятия и опускания типов:

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

Я пропустил последние 7 страниц срача, а так записать почему нельзя?

flatten [] = []
flatten (x:xs) = append [x] (flatten xs)

А… Всё понял…

Еще раз

Человек там написал такой внятный английский текст...

не счетных типов нет, т.к. любое вычислимое множество не более чем счетно.

Прочитай его.

Значит и никаких несчетных типов нет. Если какая-то модель предполагает существование таких типов - она некорректна.

you'd have similar oddities doing model theory on, say, ZF, where you can show that it has countable models, but you can prove in ZF that various sets are uncountable.

Но про счётность и несчётность разговор ты завёл. Я говорил про «большие» и «малые» коллекции. Несчётные типы и множества есть (внутренне) в любой богатой теории, будь то ZF или Теория Типов (которая Мартина-Лёфа), равно как и в любой компьютерной реализации такой теории (вот перед тобой классическое Канторовское доказательство существания несчётных типов = множеств, можно его перевести на какую-нибудь metamath количество финитных строчек в языке которой счётно :)). Но вот «большое» и «малое» относится больше к месту в кумулятивной иерархии, чем к мощности. Вот пустой класс:

data ⊥₁ : Set₁ where

но он условно большой:

⊥₁-is-quasibig : ⊥₁ → ⊥ -- ¬ ⊥₁
⊥₁-is-quasibig ()

но класс:

⊥₁-is-class : Set
⊥₁-is-class = {!!} -- ⊥₁ -- Set₁ != Set

Суть в том, что не может быть отображений

class-is-set : Set₁ → Set
class-is-set = {!!}

superclass-is-class : Set₂ → Set₁
superclass-is-class  = {!!}

-- etc.

Такая иерархия - Терм : Тип : U : U₁ : U₂ ... : {a : Level} U a : U (suc a) : ... - термы это не коллекции (по крайней мере, они не нужны как коллекции), любой x : Тип - терм, типы это коллекции (множества) термов, любой x : U - тип, U это коллекция (класс) типов, любой x : U₁ - класс, U₁ это коллекция (суперкласс) классов, любой x : U₂ - суперкласс и т.д.

Так вот, если принять U : U (или существование отображения U₁ → U, то есть сделать «большие» классы «малыми» множествами), то получится такая история. То же самое, например, в случае _класса_ функторов:

record Functor (F : Set → Set) : Set₁ where
  field fmap : ∀ {A B} → (A → B) → F A → F B

использование его как множества (типа) приведёт к противоречиям.

И это как на уровне абстрактной теории, так и на уровне реализации:

http://adam.chlipala.net/cpdt/html/Universes.html

$ agda
...
          --no-positivity-check                       do not warn about not strictly positive data types
          --no-termination-check                      do not warn about possibly nonterminating code
          --no-coverage-check                         do not warn about possibly incomplete pattern matches
          --type-in-type                              ignore universe levels (this makes Agda inconsistent)
          --sized-types                               use sized types (inconsistent with coinduction)
          --injective-type-constructors               enable injective type constructors (makes Agda anti-classical and possibly inconsistent)

использование таких флагов приведёт к тому, что можно будет доказать _любое_ утверждение, например:

{-# OPTIONS --no-termination-check #-}

you-can-prove-anything-with-me : ∀ {a} {A : Set a} → A
you-can-prove-anything-with-me = you-can-prove-anything-with-me

1≡2 : 1 ≡ 2
1≡2 = you-can-prove-anything-with-me

то же самое с --no-positivity-check (пишем Y, пишем you-can-prove-anything-with-me), то же самое с --type-in-type (Russell's - есть выше, Girard's) и --injective-type-constructors (http://thread.gmane.org/gmane.comp.lang.agda/1367). --no-coverage-check плох сам по себе. Про --sized-types не знаю.

Решением будет, конечно

loop : ∀ {a} {A : Set a} → SomeMonad A -- Partiality / IO
loop = some-lift loop

и невозможность существования функции

escape-from-the-monad : ∀ {a} {A : Set a} → TheMonad A → A
escape-from-the-monad = {!!}

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

Кстати, то что «set» of all sets (Set в Agda и Coq) это не set следует как частный случай из univalence axiom ;)

tl;dr

Существуют несчётные множества => top несчётен (в виде отступления), я зря «наехал» на top, перепутав его с U (и допуском U : U, то есть того, что большой U - малый тип). Top не большой, он тип :)

Человек там написал такой внятный английский текст...

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

Но про счётность и несчётность разговор ты завёл. Я говорил про «большие» и «малые» коллекции. Несчётные типы и множества есть (внутренне) в любой богатой теории

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

Существуют несчётные множества

где-то там внутри, что нас не интересует. А TOP состоит как раз из счетного «внешнего» множества всех термов.

Top не большой, он тип :)

то есть множество «внешней» теории.

в том то и дело, что javascript - примитив. javascript в броузере - это как ассемблер в компьютере. поэтому, создавать его без нормального «компилятора» типа гугловского GWT или питоновской пижамы - затея глупая и непрофессиональная.

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

Там определённые поднятия и опускания, а не вообще. Если типы A и B связаны отношением A <: B то можно безопасно поднять A в B, то есть подтип в супертип. Например, если A агрегирует или наследует B, то можно спокойно использовать этот подтип как супертип (то есть поднять и ожидать выполнения LSP), но обратно уже нужно опускать не из B в A, а из B в Maybe/Optional A, то есть, фактически, делать typecase по набору подтипов супертипа. Это именно статическое подтипирование в духе ООП языков (а также Data.Dynamic хаскеля и некой известной в ML техники - но тут уже сразу (и только) для топ-а). Динамика и топ появляются когда предпорядок становится directed (частичный и полный порядок я не беру, так как не хочу выбрасывать циклические данные из рассмотрения (хотя они же цикличные - это уже звоночек)).

что нас не интересует

На самом деле - не важно (счётность или несчётность). Важно поведение логики - вот U как тип плохо сказывается на таком поведении, top - вроде ничего страшного, не спорю.

просто тот же терм 1в1

Тип, пожалуйста. И append я не вижу в стандарте (я тоже выше использовал кучу самописных функций, но предполагая что очевидно, что это такое в контексте Data.Dynamic, тут я контекст уловить не могу).

Ну и как бы

def flatten(xs: Any): List[Any] = xs match {
  case Nil => Nil
  case l :: r => flatten(l) ::: flatten(r)
  case x => List(x)
}

scala> flatten(List(1, List(Some('2'), null), "2"))
res0: List[Any] = List(1, Some(2), null, 2)

Тип, пожалуйста.

По-моему речь шла как раз о том, что этот терм в хаскеле не чекается :) Тип идет как раз с not-типами, о которых я уже говорил (то есть компилятор должен знать что в третей строке НЕ пара).

И append я не вижу в стандарте

append = (++) же.