JavaScript надежность

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

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

Кэп напоминает, что в статике вместо паттерн-матчинга - кривой огрызок.

Кэп тоже любит потроллить, и это - как раз такой случай.

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

Можешь привести пару примеров готового рабочего внешнего чекера для динамического языка (любого)? Особенно интересует тайпчекер CL для SystemF.

P.S.: не факт, что анонимус еще заглянет в эту тему, поэтому cast quasimoto, если ты не против.

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

А в каком нужны?

Ну так вот, что в интерпретируемой, что в компилируемой реализации CL такой отлов опечаток предусмотрен (Lisp-N как никак).

Механизм какой?

Вот это нафлудили, отписываюсь от треда.

Хорошо хоть не забаниваешься как power.

Механизм какой?

Переменные объявлюяются явно.

Переменные объявлюяются явно.

Что это дает? Можешь привести простой пример?

Особенно интересует тайпчекер CL для SystemF.

Непонел, что? Как CL связан с SystemF?

А в каком нужны?

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

как вариант ты практически ответил на свой вопрос (jquery/jquery UI/GWT,ExtJS , etc)

>>> если у нас есть динамический ЯП, то сделать его статическим легко и просто - нам надо лишь написать внешний чекер и все
>> Можешь привести пару примеров готового рабочего внешнего чекера для динамического языка (любого)? Особенно интересует тайпчекер CL для SystemF.
> Непонел, что? Как CL связан с SystemF?

Если тайпчекер сделать «легко и просто», особенно для «такой примитивной системы типов как SystemF», его реализациями наверняка должно быть завалено пол-интернета. Вот я и попросил ссылок на реализации, раз «легко и просто». Можешь привести?

его реализациями наверняка должно быть завалено пол-интернета.

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

его реализациями наверняка должно быть завалено пол-интернета.

Не понял, почему? Он ведь никому не нужен

Хотя бы чисто академический интерес на «слабо»

Единственное исключение - в учебных целях

Ну вот! Факториалами же интернет увален по самое не хочу

в том же тапле приведена реализация - пол сотни строк.

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

Но я так и не понял, при чем тут CL?

Не обязательно CL, устроит реализация и на Scheme/Racket. Напомню контекст: было утверждение, что реализовать внешний тайпчекер «легко и просто», приведи не SystemF, любой другой пример реализации внешних типов для динамического лиспа - я не против.

Хотя бы чисто академический интерес на «слабо»

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

Ну вот! Факториалами же интернет увален по самое не хочу

Хелло ворлдами тоже. Потому что они пишутся в несколько строк, а не в несколько десятков.

А не учебные примеры есть?

А как они могут быть не учебными?

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

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

Не обязательно CL, устроит реализация и на Scheme/Racket.

На Racket будет прямой перевод кода, т.к. в Racket есть match. То есть решения на Racket и ML будут отличаться исключительно синтаксисом, чисто механический перевод будет, строка за строкой.

любой другой пример реализации внешних типов для динамического лиспа - я не против.

Я все еще не понимаю какая связь между лиспами и SystemF. Что у них общего? Или ты имел ввиду SystemF _на_ лиспе а не _для_ лиспа все-таки?

не понимаю, в чем академический интерес?

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

Алгоритм четко известен, реализуется элементарно.

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

То есть определенно в качестве тренировки-то его кто-то пишет (и даже многие, думаю, кто начинает изучать системы типов), но другое дело, что никуда не выкладывает. Ибо нафига?

Ну если все-таки «легко и просто» то хотя бы для пруфа, что это именно так.

А не учебные примеры есть?

А как они могут быть не учебными?

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

любой другой пример реализации внешних типов для динамического лиспа - я не против.

Я все еще не понимаю какая связь между лиспами и SystemF. Что у них общего?

Да ничего общего, меня SystemF вообще мало интересует. Вот на что действительно хотелось бы посмотреть - это на элегантное применение внешнего чекера и его реализацию на CL/Racket.

Или ты имел ввиду SystemF _на_ лиспе а не _для_ лиспа все-таки?

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

Да ничего общего, меня SystemF вообще мало интересует.

А зачем тогда упоминал их вместе?

Ну если все-таки «легко и просто» то хотя бы для пруфа, что это именно так.

Так пруф в том же тапле. Видишь 50 строк кода, видишь что это просто. Чего тут доказывать уже?

это на элегантное применение внешнего чекера и его реализацию на CL/Racket.

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

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

Ну, во-первых, у тебя подход фундаментально неверный. Так вышло, что статическая типизация в силу исторических причин (компьютеры раньше были большие и медленные) пошла не туда - в сторону обеспечения гарантий (чтобы байтики перекладывались правильно). Естественно, ничего такого она делать не должна, для динамических языков мы вполне может делать правильную статику - то есть чекер пропускает любой сомнительный код и не пропускает только тот код, который гарантированно сломан. А так dyalizer или pychecker например. Это из того, что практически используется, если же говорить об «академических разработках», то их, конечно, множество вот найти хоть какую-нибудь инфомрацию обычно затруднительно. Я вот знаю о Dr.Spidey (то, что было до Typed Racket) и еще одна хреновина для питона, не помню как называлась, но чекала она значительно больше чем тот же pycheker, однако все это было криво и недоделано (уровень proof of concept - самим себе доказать, что можно, да).

Да ничего общего, меня SystemF вообще мало интересует.

А зачем тогда упоминал их вместе?

Перечитай на какую реплику я отвечал изначально: «если у нас есть динамический ЯП, то сделать его статическим легко и просто - нам надо лишь написать внешний чекер и все» (с) anonymous. Или это не ты писал?

Ну если все-таки «легко и просто» то хотя бы для пруфа, что это именно так.

Так пруф в том же тапле. Видишь 50 строк кода, видишь что это просто. Чего тут доказывать уже?

System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. — т.е. пример на окамле не показателен, он сам ML и system-F, если верить википедии. Хотелось посмотреть на юзабельную system-F для лиспа, как она там смотрится - органично или угребищно. TAPL не осилил пока что.

Для лиспа (и вообще для языка с нестрогим синтаксисом и семантикой) нельзя сделать внешний чекер.

Один анонимус утверждает что нельзя, другой что можно - кому верить? :D

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

Короче, мы видимо о разной «внешности» говорим. Пусть это будет не внешний чекер, пусть будет (e)DSL, мне пофиг, но как в таком случае обеспечить проверку гарантий типов (например входных параметров edsl-функции), не переписывая рантайм, а по сути реализацию - мне пока не ясно. Т.е. пока что мне кажется, что это должен быть какой-то такой лисп (или не лисп), в рантайме которого заложен фреймворк для органичного задания опциональной статической типизации для произвольной системы типов. Ошибаюсь?

С другой стороны, благодаря наличию нужного АПИ проще сделать «внутренний» чекер.

Расскажи на пальцах как?

Так что такой подход имеет как недостатки так и достоинства (здесь также как и с ИДЕ например - правильная ИДЕ для лиспов тоже крутится внутри того же рантайма).

Эта ide «правильна» и фичаста ровно на столько, на сколько позволяет рантайм или опаньки.

Ну, во-первых, у тебя подход фундаментально неверный.

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

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

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

если же говорить об «академических разработках», то их, конечно, множество вот найти хоть какую-нибудь инфомрацию обычно затруднительно

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

dyalizer или pychecker например

Pychecker - это несерьезно. Pyflakes, pylint - тоже.

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

PyScope? Он не весь Python проверяет, и написан в 2010-211, хотя интерес к таким инструментам был гораздо раньше. Так что «легкая и простая» задача до сих пор не решена (хотя есть статья каких-то португальцев, в которой они говорят об умении статически чекать почти весь Python).

Перечитай на какую реплику я отвечал изначально: «если у нас есть динамический ЯП, то сделать его статическим легко и просто - нам надо лишь написать внешний чекер и все» (с) anonymous. Или это не ты писал?

Я. Но про SystemF же там не написано ничего.

т.е. пример на окамле не показателен, он сам ML и system-F, если верить википедии.

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

Хотелось посмотреть на юзабельную system-F для лиспа

Не понял, почему ты все время говоришь «для»? «На» лиспе же имеется ввиду?

Один анонимус утверждает что нельзя, другой что можно - кому верить? :D

Кто утверждает, что можно?

Короче, мы видимо о разной «внешности» говорим.

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

Пусть это будет не внешний чекер, пусть будет (e)DSL, мне пофиг

А, ну если без внешних - тут всякие Qi, Typed Racket, теорем пруверы на лиспе и т.п.

не переписывая рантайм, а по сути реализацию - мне пока не ясно.

Макросами вполне можно. Я же вроде даже в этом треде приводил пример как на макросах делаются недо-структуры («недо» т.к. proof of concept на два десятка строк), в которых список полей объявляется статически и потом при попытке обратится к какому-то полю статически гарантируется, что все ок. То есть если объект является структурой с полем «х», то можно попросить его значение, а если не является - то в этом месте при компиляции кинет эррор.

Расскажи на пальцах как?

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

Эта ide «правильна» и фичаста ровно на столько, на сколько позволяет рантайм или опаньки.

правильный лиспорантайм должен позволять все, что нам может понадобиться :)

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

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

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

Как-то мало информации. Я вот о том же Dr.Spidey узнал совершенно случайно, копаясь во все списке публикаций PLT team. Хотя подобные вещи и до этого уже искал.

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

Почему не решена? Нам ведь и не надо «весь». Важен вопрос «нужности» задачи. Задача даже если и простая, но никому не нужная - ее и решать никто не будет. Точнее будет вот такой вот «почти весь» в качестве proof of concept, а до конца никто доводить не будет потому что «ну понятно же что это можно, зачем тратить время?»

#lang typed/racket (http://docs.racket-lang.org/ts-guide/, http://www.ccs.neu.edu/racket/pubs/popl08-thf.pdf)? Не знаю, насколько он внешний, но пытается сохранить совместимость со схемой, при этом добавив ограничения в духе STLC с объединениями и подтипами.

Что касается CL - какой смысл в его статическом чекере, если при этом 90% (если не все 99) типичных программ на CL не пройдут его проверку?

Не знаю, насколько он внешний

Он ни на сколько не внешний, просто попросили «вообще любой».

Что касается CL - какой смысл в его статическом чекере, если при этом 90% (если не все 99) типичных программ на CL не пройдут его проверку?

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

Почему не решена?

Потому что так сказал автор PyScope.

Нам ведь и не надо «весь»

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

Задача даже если и простая, но никому не нужная - ее и решать никто не будет.

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

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

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

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

Ее решили ровно на столько, на сколько было практически целесообразно.

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

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

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

Ее решили ровно на столько, на сколько было практически целесообразно.

Доо. Все Python-IDE фейлят на выводе типов, CLI-инструменты - уровня pychecker (т.е. никакие), но «задача решена настолько, насколько практически целесообразно». Для кого целесообразно - тех, кто не пользуется Python?

И что уж говорить о Python, когда даже команда Racket (которая генерирует большую часть статей по чекерам существующего кода на динамических языках) не решила задачу статической типизации практически используемого подмножества Scheme - это как бы намекает на «легкость и простоту».

Он может пропустить некоторые корректные программы, если не может доказать их корректность.

Может, _не_ пропустить? И тогда - какие это «корректные» (в каком-то абсолютном смысле? что это за смысл?) программы не пропускает, например, тайпчекер STLC? Если с точки зрения STLC синтаксис термов и типов однозначно (индуктивно) определён, правила типизации тоже определены, а алгоритм проверки типов разрешим и имеет результатом ответ «да или нет» на вопрос «является ли данный терм правильно типизированным?» (опять же, с точки зрения STLC).

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

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

Для кого целесообразно - тех, кто не пользуется Python?

Нет, для тех, кто пользуется.

не решила

Ну для Typed Racket чекер тоже допускающий, а не отвергающий. То есть фундаментально сломанный. И некоторые моменты там не чекаются чисто из-за мнения разработчиков и семантики языка - например при переполнении фикснума бросается исключение, разработчики решили, что любое исключение связанное с типами, чекер пропускать не должен. В результате то, что пропускает чекер того же хаскеля, посчитав правильной программой, чекер TR не пропустит, считая неправильной :)

То есть функция add1 это не Fixnum -> Fixnum, а Fixnum -> Integer.

Может, _не_ пропустить?

Да, конечно.

И тогда - какие это «корректные» (в каком-то абсолютном смысле? что это за смысл?) программы не пропускает, например, тайпчекер STLC?

STLC? Ну он много какие программы не допускает, даже тьюринг-полнота теряется. Так что вот любая программа, которая чекается, например, в SystemF, но не чекается в STLC (очевидно, что такие программы есть и их много).

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

Тоже очень полезный чекер.

Ну для Typed Racket чекер тоже допускающий, а не отвергающий.

Typed Racket - это отдельный язык, с сильной статической типизацией. Причем он к разговору о чекерах для Python?

Ну он много какие программы не допускает, даже тьюринг-полнота теряется.

Тут такой момент ─ ULC и STLC это два разных языка, то есть их синтаксис отличается (если не рассматривать HM как отображение из untyped в typed, всё равно известно, что в более интересных случаях подобного отображения не существует). Программа ULC (λ i . i i) (λ i . i i) не является программой STLC вообще ─ (λ i : ? . i i) (λ i : ? . i i), то есть, если в ULC она корректна, то в STLC не то что некорректна, а просто не пишется (какая-нибудь (λ i : int → int . i i) (λ i : int → int . i i) некорректна в STLC формально и в ULC по смыслу, то есть не является переводом корректной в ULC программы).

Так что вот любая программа, которая чекается, например, в SystemF, но не чекается в STLC

Тут тем более. STLC:

Type variables      α, β, ...
Term variables      i, j, ...

Types               A, B, ... ∷= α | A → B
Terms               t, u, ... ∷= i | λ i : A . t | t u

SystemF (single-sorted):

Types               A, B, ... ∷= α | A → B | ∀ α . A
Terms               t, u, ... ∷= i | λ i : A . t | t u | Λ α . t | t A

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

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

Ещё я не понял что значит «доказывать корректность» (мочь и не мочь) и «доказывать некорректность» (тоже). Процедура проверки типов же бинарная по сути ─ либо программа хороша в данной теории, либо нет.

Афтор, почему бы просто не изучить (полностью) js и использовать динамические типы? Если так уж сложно переключить свой мозк, то можешь использовать Darcs или TypoScript. И можешь не благодарить :)

Darcs и Typoscript. лол. Если вы написали это специально, то, правда, не стоило :)

Аж самому смешно стало :) Сам я про них только слышал. Мне строгая типизация в скриптах не нужна.

Dart & TypeScript

fix

Тут такой момент ─ ULC и STLC это два разных языка

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

Программы SystemF не то чтобы отбрасываются чекером STLC, они просто не пишутся ввиду отсутствия нужных синтаксических конструкций.

Да нет, конечно же, прекрасно все пишется, достаточно добавить ТИ.

Точно так же тьюринг-полные программы STLC+fix не пишутся в STLC так как отсутствует синтаксический примитив fix вмести со своими правилами типизации и оп. семантики.

fix - это не примитив, это терм Y-комбинатора. Разница в том, что терм, который задает Y-комбинатор в SystemF, чекается, а в STLC _точно тот же самый терм_ не чекается.

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

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

Тогда как синтаксис и семантика разные

В том и дело, что одинаковые. Операционная семантика и синтаксис совпадают. Конечно, если под семантикой понимать правила типизация то разница будет - ну так это очевидно, ведь системы типов разные.

Ещё я не понял что значит «доказывать корректность» (мочь и не мочь) и «доказывать некорректность» (тоже). Процедура проверки типов же бинарная по сути ─ либо программа хороша в данной теории, либо нет.

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

Тоже очень полезный чекер.

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

Typed Racket - это отдельный язык, с сильной статической типизацией.

Нет, Typed Racket - это тот же Racket, но с добавленным чекером. На практике, да, разница в том, что надо дописать аннотаций - но формально этого можно избежать, т.к. раньше вообще-то и был полный вывод (без аннотаций). Просто ради практического удобства от этого отказались (чтобы не было как в том же хаскеле - cannot be inferred вместо человеческой ошибки типов). Аннотации кстати при желании вообще можно сложить в отдельный файл и считать их хинтами этому самому внешнему чекеру.

Причем он к разговору о чекерах для Python?

Не знаю, ты же упомянул. Я просто внес некоторые пояснения.

нам подход и наличие чекера не важно - важно «качество» этого чекера.

Да. Но «легко и просто» качественный чекер не пишется, что доказано существованием кучи никаких чекеров для Python и отсуствием чекера даже для полной Scheme.

Typed Racket - это отдельный язык, с сильной статической типизацией.

Нет,

«Typed Racket is a family of languages» (ц)

Причем он к разговору о чекерах для Python?

Не знаю, ты же упомянул.

Я упомянул не его, а результаты работы команды, стоящей за ним.

«Typed Racket is a family of languages» (ц)

И как это связано с тем, что Typed Racket - это библиотека макросов для Racket? Ну просто, по факту. Берем обычный Racket, импортируем библиотеку и получаем тайпчекер.

Да. Но «легко и просто» качественный чекер не пишется

Почему не пишется? Конечно же пишется.

что доказано существованием кучи никаких чекеров для Python и отсуствием чекера даже для полной Scheme.

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

Я упомянул не его, а результаты работы команды, стоящей за ним.

Ну а я указал на то, что ты сказал чушь. Мои слова были ответом на твои, все.

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

К STLC ─ можно (я там сказал, что HM не интересно рассматривать).

Да нет, конечно же, прекрасно все пишется, достаточно добавить ТИ.

Который для System F невозможен. А если добавить подтипы, зависимые типы и прочие неоднозначности ─ так тем более.

Ну и если я пишу код в System F с ∀ по типам и с типо-абстракциями с типо-аппликациями (которые в ней возможны на уровне термов), то как такой код может отбрасываться STLC когда он в ней вообще не пишется и не имеет смысла?

fix - это не примитив, это терм Y-комбинатора. Разница в том, что терм, который задает Y-комбинатор в SystemF, чекается, а в STLC _точно тот же самый терм_ не чекается.

Это какой-то фольклор, Y-комбинатор вполне типизируется во всех системах лямбда-куба (в STLC это будет семейство примитивов с не полиморфными типами для всех возможных монотипов, в System F ─ примитив с типом ∀ a . (a →a) → a), но не пишется ни в одной из этих систем (STLC, System F, ...) в силу строгой нормализации, поэтому в такие системы fix / общая рекурсия / рекурсивные типы добавляются непосредственно как примитивы на уровне синтаксиса и оп. и типовой семантики (на практике такова letrec форма в хаскеле / ML). А вот комбинатор само-применения не может быть даже типизирован без добавления (equi-) рекурсивных (бесконечных) типов.

Есть общий синтаксис для термов

Где он общий? Вот я привёл в пример ULC, STLC и System F ─ синтаксис разный, можно вложить программу STLC в System F, но не наоборот (типы System F не стираются так просто), можно стереть типы в STLC и получить ULC, но не каждому хорошему терму ULC будет соответствовать хороший терм STLC (хотя HM и реализует разрешимый, но частичный алгоритм такого соответствия).

Если бы у данных теорий совпадали синтаксис и семантика, то им бы соответствовали одинаковые модели, а это не так (хотя бы потому что ULC противоречива, а системы лямбда куба строго нормализированны и непротиворечивы (исходя из конструктивного подхода к противоречивости ─ «этого [противоречий] не может быть, потому что этого не может быть в принципе»)).

Операционная семантика и синтаксис совпадают.

Вот ещё пример ─ в STLC правила редукции и типизации таковы, что все программы завершаются. В STLC+gen.rec. есть дополнительная синтаксическая форма letrec (которая как раз позволяет написать в хаскеле fix f = f (fix f)) и правила редукции позволяют писать нетерминируемые программы. Синтаксис и семантика различны.

Все нынешние системы типов отвергают некоторую часть программ, которые вполне редуцируются

Как обычно ─ примеры?

Никак. Там простой синтаксический разбор:

virtuos86@sib:~$ python
Python 2.7.2+ (default, Jul 20 2012, 22:12:53) 
[GCC 4.6.1] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> def foo():
...  return bar
... 
>>> foo # объект-функция создан, значит байт-код тоже создан
<function foo at 0xb77e417c>
>>> foo.func_code
<code object foo at 0xb7858e30, file "<stdin>", line 1>
>>> foo.func_code.co_code
't\x00\x00S'
>>> foo()
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 2, in foo
NameError: global name 'bar' is not defined
>>> 

К STLC ─ можно

Ну и все, какие проблемы?

я там сказал, что HM не интересно рассматривать

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

Который для System F невозможен.

Что, простите? А НМ это что?

Ну и если я пишу код в System F с ∀ по типам и с типо-абстракциями с типо-аппликациями (которые в ней возможны на уровне термов), то как такой код может отбрасываться STLC когда он в ней вообще не пишется и не имеет смысла?

Не понял о чем ты? Это же один и тот же код. Одна и та же последовательность символов. Разница только в том, каким чекером мы его будем прогонять.

Это какой-то фольклор, Y-комбинатор вполне типизируется во всех системах лямбда-куба

Что за бред ты несешь? Ну напиши Y-комбинатор и попробуй типизировать этот терм в STLC. Успехов.

но не пишется ни в одной из этих систем (STLC, System F, ...)

В SystemF пишется. И типизируется. В STLC пишется. Но не типизируется.

Где он общий?

Ну грамматика полностью совпадает, значит общий же? терм = абстракция или аппликация, аппликация = (терм терм), абстракция = lambda переменная . терм. Это грамматика ULC, STLC, SystemF. Она совпадает для всех трех систем.

но не наоборот

Наоборот как раз.

(типы System F не стираются так просто)

Стираются. Не стираются high-kind и ad-hoc полиморфизм.

Если бы у данных теорий совпадали синтаксис и семантика

У них разная семантика - разные правила типизации же (если правила типизации включать в семантику. операционная семантика, коненчо же, совпадает).

Вот ещё пример ─ в STLC правила редукции и типизации таковы, что все программы завершаются. В STLC+gen.rec. есть дополнительная синтаксическая форма letrec (которая как раз позволяет написать в хаскеле fix f = f (fix f)) и правила редукции позволяют писать нетерминируемые программы. Синтаксис и семантика различны.

Ну так это ты сравниваешь STLC и STLC+fix. А мы сравниваем STLC, ULC, SystemF.

Как обычно ─ примеры?

Так я же тебе привел уже примеры. Любая программа, которая чекается в SystemF, но не чекается в STLC. То есть любая программа, которая зависает, например (ее можно написать в SystemF, но нельзя в STLC). Ну или если хочется конкретного - flatten в лиспе. Это вполне корректный синтаксически терм как в STLC так и в SystemF (ведь синтаксис совпадает, как мы выше убедились), при чем этот «правильный» терм - то есть он редуцируется в ULC (а любой терм, редуцируемый в ULC, редуцируется так же в STLC или SystemF или в ЛЮБОМ расширении ULC, так как правила редукции будут совпадать), и вообще соответствует «правильно работающей порграмме», но чекер его не пропускает. И таких термов (правильных, но не рпопускаемых) множество. Более того - их значительно больше, чем «правильных, но пропускаемых» (если говорить статистически, по мощности все совпадает, конечно).

Ты не читал что ли, как пиндосы спутник отлаживали по лисповому реплу? Space production, так сказать :))

«легко и просто» качественный чекер не пишется

Почему не пишется? Конечно же пишется.

Ну ты примеры приведешь наконец?

Почему это неинтересно?

Потому что TI это техническое средство которое работает только в самоочевидных случаях, чем больше типы становятся действительно утверждениями, тем меньше смысла в TI, просто потому что по виду программ (доказательств) нельзя угадать какие именно типы они имеют (какие утверждения доказывают). Это проявляется даже в хаскеле при type/data driven разработке, когда инварианты энфорсятся сверху как GADTs типы или классы с зависимостями. Например, полагаться на вывод типов при работе с перегруженными массивами или регулярными выражениями нельзя, GHC что-то вывести там просто не может (by design). И тут просто ─ по абстрактному контексту нельзя выбрать конкретную реализацию массивов или результат сопоставления с данным образцом (который просто строка, а результат может быть сложным кортежем). В случае зависимых типов ─ сложнее и тем более меньше толка от TI.

А НМ это что?

Wells' result implies that type inference for System F is impossible. A restriction of System F known as «Hindley–Milner», or simply «HM», does have an easy type inference algorithm and is used for many strongly typed functional programming languages such as Haskell 98 and ML.

(c) http://en.wikipedia.org/wiki/System_F.

HM это, с одной стороны, название определённого разрешимого алгоритма вывода типов, и, с другой, название _подмножества_ System F для которого этот алгоритм существует. Для полной System F вывод типов невозможен (неразрешим). То есть, HM как язык это, фактически, как раз тот кусок System F для которой возможен вывод типов (как одноимённый алгоритм).

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

Выписываю грамматику ещё раз.

ULC (противоречивая теория первого порядка):

Term variables      i, j, ...
Terms               t, u, ... ∷= i | λ i . t | t u

STLC (строго-нормализованная теория первого порядка):

Term variables      i, j, ...
Type variables      α, β, ...
Types               A, B, ... ∷= α | A → B
Terms               t, u, ... ∷= i | λ i : A . t | t u

System F (строго-нормализованная теория второго порядка):

Term variables      i, j, ...
Type variables      α, β, ...
Types               A, B, ... ∷= α | A → B | ∀ α . A
Terms               t, u, ... ∷= i | λ i : A . t | t u | Λ α . t | t A

Синтаксисы разные, теории разные, модели разные (с отсылкой к Дане Скотту), интернализации разные (CCC over domain / CCC / CCC+pullbacks). В ULC есть нетерминируемые программы, парадоксы (вроде Kleene-Rosser) и она противоречива, тогда как STLC и System F строго-нормализированы. STLC и System F при этом отличаются порядком. Как, например в ULC/STLC написать (Λ typeVar . typeDependentTerm[typeVar])? То есть second-order квантификацию из System F, при том, что ULC/STLC это first-order теории.

Стираются.

Смотря что понимать под стиранием. Компиляцию с устранением type level? Так я не про то. Вот в STLC типы реально стираются, то есть есть тотальное соответствие STLC → ULC (просто как (λ var : SomeType . someTerm[var]) → (λ var . someTerm[var])), потому что это теории одного (первого) порядка и ULC, кхм, «шире», а как ты собрался стирать вычисления с использованием абстракции по типам Λ и аппликацией термов зависимых от типов к типам? Во что превращать терм (Λ typeVar . typeDependentTerm[typeVar])? То есть как построить тотальное соответствие SystemF → STLC для теорий разных порядков (и при том, что тут SystemF шире)?

Ну напиши Y-комбинатор и попробуй типизировать этот терм в STLC

Как я его напишу, если я говорю «не пишется ни в одной из этих [лямбда куба] систем (STLC, System F, ...)»? Его типом в STLC _должно_ быть семейство (α → α) → α для каждого монотипа α теории, а в System F ─ полиморфный тип ∀ a . (a →a) → a. Это я имею ввиду, говоря «типизируется», то есть, нужный тип можно написать (в отличии от бесконечного типа комбинатора само-применения (тут ни тип, ни терм не написать)). Но соответствующий терм чисто физически не написать ─ ни в STLC, ни в System F.

В SystemF пишется. И типизируется.

Если ты сможешь написать fix в SystemF, то сможешь написать нетерминируемый терм (fix id). Fail.

В SystemF пишется.

В STLC пишется.

Напишешь?

fix ≡ λ f : [подставить нужное] . [подставить нужное]

Любая программа, которая чекается в SystemF, но не чекается в STLC

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

То есть любая программа, которая зависает, например (ее можно написать в SystemF, но нельзя в STLC)

То есть ты думаешь, что SystemF не является строго-нормализованной и имеет нетерминируемые термы? Это неправда. Все системы лямбда куба строго-нормализованны, с только терминируемыми термами, не тьюринг-полны, так что разрешима проблема останова и имеет место быть «локальная непротиворечивость».

ведь синтаксис совпадает, как мы выше убедились

Я с этим не соглашался. В типизированном языке мы пишем типы. λf.(λx.f (x x)) (λx.f (x x)) является термом в нетипизированной лямбде, но в типизированной мы должны писать двоеточие и тип после имени переменной в лямбда абстракции, то есть чисто синтаксически, так что считать это термом типизированной лямбды это как пытаться скомпилировать *.js с помощью gcc :) (синтаксис одинаковый, чё).

Ну или если хочется конкретного - flatten в лиспе.

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

В Scheme:

(define (flatten x)
  (cond ((null? x) '())
        ((not (pair? x)) (list x))
        (else (append (flatten (car x)) (flatten (cdr x))))))

В Scala:

def flatten(l: List[_]): List[Any] = l match {
  case Nil => Nil
  case (head: List[_]) :: tail => flatten(head) ::: flatten(tail)
  case head :: tail => head :: flatten(tail)
}

В Haskell:

flatten [] = []
flatten (x:xs) = maybe (x :) ((++) . flatten) (fromDynamic x) $ flatten xs

Это для гетерогенности. А так если переписать в лоб, то будет проблема с бесконечными типами, точно также как если переписать Y в лоб, которая решается обособлением нужных рекурсивных типов - rose tree для вложенных списков (в Data.Tree уже есть flatten :: Tree a -> [a]) для flatten и Mu для Y.

flatten (x:xs) = maybe (x :) ((++) . flatten) (fromDynamic x) $ flatten xs

То есть

flatten (x:xs) = maybe [x] flatten (fromDynamic x) ++ flatten xs

или

flatten (x:xs) =
  case fromDynamic x {- :: [Dynamic], i.e. check if `x' is a het. list or not -} of
    Nothing -> x : flatten xs
    Just ys -> flatten ys ++ flatten xs

Можно обобщить на произвольные подтипы:

class sup :> sub where
  ($>) :: (sub -> sub) -> sup -> sub

flatten :: (a :> [a]) => [a] -> [a]
flatten [] = []
flatten (x:xs) = flatten $> x ++ flatten xs

В частности, для top запускается на правах того, что список значений top типа сам значение top типа, то есть [top] <: top:

instance Dynamic :> [Dynamic] where
  f $> dyn = maybe [dyn] f (fromDynamic dyn)

А так если переписать в лоб

Так и требуется переписать в лоб. Потому что если переписать не в лоб - это уже _другой_ терм. А тот что нужен - не чекается. Хотя он корректен и редуцируется корректно.

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

Ну вот о чем и речь. У нас есть корректный терм. И он либо тайпчекается либо нет в зависимости от того, на сколько выразительна система типов. Хотя терм _заведомо_ корректный.

Приведи пример.

lambda x . x - чекается в SystemF (: forall (A) A -> A), не чекается в STLC.

Я с этим не соглашался. В типизированном языке мы пишем типы.

Мы рассматриваем язык с full inference, так что типы можно не писать и синтаксис будет полностью совпадающим. На систему типов это никак не влияет. Для STLC и SystemF без high-rnak (<=2) фулл инференс работает, так что спокойно чекаем.

точно также как если переписать Y в лоб, которая решается обособлением нужных рекурсивных типов - rose tree для вложенных списков (в Data.Tree уже есть flatten :: Tree a -> [a]) для flatten и Mu для Y.

И в результате мы снова поулчаем _другой_ терм. Тот, другой, он тоже корректный. Но чекается. А первый корректный - не чекается.

Напишешь?

Ну стандартное выражение y-комбинатора. Лень писать, ты и сам его знаешь.

Смотря что понимать под стиранием.

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

Синтаксисы разные

Синтаксисы совпадают. Ты просто без вывода типов рассматирваешь.

Как я его напишу, если я говорю «не пишется ни в одной из этих [лямбда куба] систем (STLC, System F, ...)»?

Ну как не пишется если пишется? Берем терм y-комбинатора в ULC, он точно такой же в STLC и SystemF. То есть является синтаксически корректным термом этих систем. Другое дело, что он там не чекнется. Но пишется свободно.

Потому что если переписать не в лоб - это уже _другой_ терм.

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

                                                  -- flatten :: Dynamic -> [Dynamic]
(define (flatten x)                               flatten x = case fromDynamic x of
  (cond ((not (pair? x)) (list x))                  Nothing -> [x]
        ((null? x) '())                             Just [] -> []
        (else (append (flatten (car x))             Just (x:xs) -> flatten x ++
                      (flatten (cdr x))))))                        flatten (toDyn xs)

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

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

Ты просто без вывода типов рассматирваешь.

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

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

И во что превратились полиморфные id, map, compose и т.п.? В счётное количество функций? Или в лексикографическое от количества типов в программе количество функций (как в компиляторах SML и при раскрытии шаблонов C++)? Это компиляция, то есть абстракция по типам и аппликация к типам просто выбрасываются (хотя они сами по себе термы, а не части термов, как ": type" в (lambda (x : type) . ...)). Но вообще согласен, можно назвать такое «стиранием типов» (стирание же).