Applied Type System
Поигрался с чуть ли не вчера реализованном языком программирования - ATS. Драфт Language User's Guide выпущен буквально 1го декабря.
Очень интересно выглядит возможность автоматической верифицируемости различных линейных комбинаций между входными и выходными значениями. При необходимости, можно пытаться через линейные комбинации явно выписывать доказательства нелинейных свойств. Например, можно добится автоматической проверки того что функция concat принимающая на вход список длиной n состоящий из списков длиной r, возвратит список длиной n*r. А составив из параметров рекурсивной функции линейную, убывающую комбинацию - терминирующую метрику, можно быть уверенным что компилятор проверит завершимость данной функции.
Насчет production-ready я сомневаюсь, но по крайней мере, судя по Language Shootout, ATS вполне может оказаться Project Euler Ready языком :).
Для языка в котором programming is combined with theorem-proving результаты сравнений более чем потрясающие. По скорости программ ATS вполне сравним не только с Ocaml, но даже и с чистым C.
Хотя не все так просто, вероятно таких результатов удалось добится фактически тем что в языке доступны два способа хранения данных: boxed - обернутые и доступные сборщику мусора данные и flat - компилируемые в си структуры, и размещаемые на стеке.
Синтаксис, IMHO, зубодробительный, типы параметров функции, ограничения на них, ограничение на возвращаемое значение, терминирующая метрика, все идет скопом между "fun имя_функции" и знаком "=" перед телом.
Мне кажется префиксное описание ограничений, ну или хотя бы использование слов, вместо всего богатства скобочек (, [, { облегчило бы чтение программ.
Очень интересно выглядит возможность автоматической верифицируемости различных линейных комбинаций между входными и выходными значениями. При необходимости, можно пытаться через линейные комбинации явно выписывать доказательства нелинейных свойств. Например, можно добится автоматической проверки того что функция concat принимающая на вход список длиной n состоящий из списков длиной r, возвратит список длиной n*r. А составив из параметров рекурсивной функции линейную, убывающую комбинацию - терминирующую метрику, можно быть уверенным что компилятор проверит завершимость данной функции.
Насчет production-ready я сомневаюсь, но по крайней мере, судя по Language Shootout, ATS вполне может оказаться Project Euler Ready языком :).
Для языка в котором programming is combined with theorem-proving результаты сравнений более чем потрясающие. По скорости программ ATS вполне сравним не только с Ocaml, но даже и с чистым C.
Хотя не все так просто, вероятно таких результатов удалось добится фактически тем что в языке доступны два способа хранения данных: boxed - обернутые и доступные сборщику мусора данные и flat - компилируемые в си структуры, и размещаемые на стеке.
Синтаксис, IMHO, зубодробительный, типы параметров функции, ограничения на них, ограничение на возвращаемое значение, терминирующая метрика, все идет скопом между "fun имя_функции" и знаком "=" перед телом.
Мне кажется префиксное описание ограничений, ну или хотя бы использование слов, вместо всего богатства скобочек (, [, { облегчило бы чтение программ.