История изменений

С чего вдруг?

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

Между рассматриваемыми системами (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, 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 ещё хуже выводятся.