История изменений
Исправление quasimoto, (текущая версия) :
Пишется = терм можно подать на вход 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, но удобнее). Вот я и не понимаю чем такой язык плох и что в нём «пишется, но не чекается».
Исходная версия quasimoto, :
Пишется = терм можно подать на вход 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, но удобнее). Вот я и не понимаю чем такой язык плох (кроме того что противоречив :)) и что в нём «пишется, но не чекается».