Недавно занялся изучением языка ATS — Applied Type System, который еще давно привлек мое внимание очень хорошими скоростными показателями на language shootout. Тогда меня отпугнула многословность решений, а оказывается она там не просто так: ATS содержит систему зависимых типов и конструктивных доказательств, которые поднимают уровень обеспечения коррекности до невиданных высот, вплоть до полного статического доказательства того, что программа делает то, что надо, и не содержит багов. Компилируется язык путем трансляции в Си и использования gcc, что дает ему очень простой FFI и все gcc-шные наработки по оптимизациям. А возможность указания массы условий и инвариантов в типах и их статического доказательства позволяет избежать лишних проверок в рантайме и обеспечить высокую скорость. В языке есть поддержка сборки мусора, но доступно также и подмножество языка, работающее без GC: можно собирать программы без GC, причем корректность работы с памятью обеспечивается системой типов. Документация по языку сильно разрозненная и неполная, но я начал серию постов по-русски с рассказами о фичах ATS доступным языком.
сорт и kind — это одно и тоже?
> на типах вы можете сделать всё что угодно, при условии что этого никак нельзя будет наблюдать в окружающем мире
а почему нельзя использовать функцию, которая распакует сорт в реальное значение?
например, если kind определен для типа, который существует на уровне исполнения, то достаточно инстанциировать в runtime-е этот тип kind-ом.
Здравствуйте, DarkGray, Вы писали:
DG>сорт и kind — это одно и тоже?
Нет, довольно таки разные вещи.
>> на типах вы можете сделать всё что угодно, при условии что этого никак нельзя будет наблюдать в окружающем мире
DG>а почему нельзя использовать функцию, которая распакует сорт в реальное значение?
Не уверен, что правильно понял вопрос, если отвечу невпопад, то уточни вопрос.
В ряде случаев это тавтология, например значение типа int 3 может быть только тройкой, статика и динамика совпадают, распаковывать ничего не нужно. А в ряде других случаев мы упираемся в то, что статические значения используются только в компайл-тайме, в рантайме их просто нет. Банальный пример — тип list(int, 10) (т.е. список из 10 интов) в рантайме представлен классическим односвязным списком, длина нигде не хранится. Просто при компиляции компилятор проверит все равенства и неравенства, упоминающие длину этого списка, на непротиворечивость и, если все ок, выдаст корректный код, в котором не будет например обращений к 11-му элементу данного списка. Но чтобы получить в рантайме длину этого списка как рантайм-значение, его надо честно вычислить, обойдя список.
DG>>сорт и kind — это одно и тоже?
DM>Нет, довольно таки разные вещи.
в чем отличие?
DM> А в ряде других случаев мы упираемся в то, что статические значения используются только в компайл-тайме, в рантайме их просто нет.
согласен, по умолчанию они на runtime не переносятся, но их туда можно перенести тем или иным способом.
DM> Банальный пример — тип list(int, 10) (т.е. список из 10 интов) в рантайме представлен классическим односвязным списком, длина нигде не хранится. Просто при компиляции компилятор проверит все равенства и неравенства, упоминающие длину этого списка, на непротиворечивость и, если все ок, выдаст корректный код, в котором не будет например обращений к 11-му элементу данного списка. Но чтобы получить в рантайме длину этого списка как рантайм-значение, его надо честно вычислить, обойдя список.
если при компиляции было указано число 10, то ничего считать не надо, надо лишь подставить в нужное место это число (там где нужна распаковка).
при этом возникает лишь задача протащить через код это число от места введения до места использования.
зы
посчитать один раз придется, если использует сорт вида "список константной длины n", тогда и на уровне компиляции неизвестна длина списка, а известно лишь что список не меняет своей длины при преобразованиях.
Здравствуйте, DarkGray, Вы писали:
DG>>>сорт и kind — это одно и тоже? DG>в чем отличие?
kind — вид типа данных (или их конструкторов?)
sort — вид статического терма, не только типа данных. Например, утверждения (props) — статические термы, не являющиеся типами данных. Еще можно свой сорт ввести, который будет как-то использоваться при компиляции для формулирования некоторых инвариантов и фактов, но типом данных он сам по себе не будет. "Тип данных" — лишь один из сортов, грубо говоря.
DM>> А в ряде других случаев мы упираемся в то, что статические значения используются только в компайл-тайме, в рантайме их просто нет. DG>согласен, по умолчанию они на runtime не переносятся, но их туда можно перенести тем или иным способом.
Можно, просто девиз ATS — точность. "If I could associate only one single word with ATS, I would choose the word precision. Programming in ATS is about being precise and being able to effectively enforce precision."
Хочешь рантайм-значение — опиши его явно: где оно создается, куда передается и как связано с остальными.
которые живут только в compile-time?
DM>sort — вид статического терма, не только типа данных. Например, утверждения (props) — статические термы, не являющиеся типами данных. Еще можно свой сорт ввести, который будет как-то использоваться при компиляции для формулирования некоторых инвариантов и фактов, но типом данных он сам по себе не будет. "Тип данных" — лишь один из сортов, грубо говоря.
т.е., например, то, что инвариант цикл двигается ближе к цели от итерации к итерации — это сорт?
DM>>> А в ряде других случаев мы упираемся в то, что статические значения используются только в компайл-тайме, в рантайме их просто нет. DG>>согласен, по умолчанию они на runtime не переносятся, но их туда можно перенести тем или иным способом.
DM>Можно, просто девиз ATS — точность. "If I could associate only one single word with ATS, I would choose the word precision. Programming in ATS is about being precise and being able to effectively enforce precision." DM>Хочешь рантайм-значение — опиши его явно: где оно создается, куда передается и как связано с остальными.
во, извращенцы!
что называется — выберите любые две: сложность решаемой задачи, точность описания, реальное время разработки.
Здравствуйте, DarkGray, Вы писали:
DM>>kind — вид типа данных (или их конструкторов?) DG>которые живут только в compile-time?
Это ты мне скажи, раз о kind'ах заговорил. Насколько я их понимаю — да. В самом ATS такого явного понятия (как в Хаскеле) нет, вроде.
DM>>sort — вид статического терма, не только типа данных. Например, утверждения (props) — статические термы, не являющиеся типами данных. DG>т.е., например, то, что инвариант цикл двигается ближе к цели от итерации к итерации — это сорт?
Если этот инвариант выразить явно, получится утверждение (а.k.а. теорема) — статический терм, внешне похожий на тип. Доказывать его будут динамические значения — доказательства, внешне похожие на рантайм-значения, но на самом деле в рантайм не попадающие. Так вот, это утверждение будет иметь сорт prop. См. http://thedeemon.livejournal.com/41388.html
Подобно тому, как обычным выражениям (динамическим термам) в программе мы приписываем их типы (являющиеся статическими термами), статическим термам мы приписываем их "тип" — сорт.
Рантайм-значение (динамический терм) 3 может иметь тип int, который имеет сорт t@ype.
Рантайм-значение "abc" имеет тип string, имеющий сорт type.
В примере по ссылке динамическое значение LEONbase доказывает утверждение LEON(0,1), имеющее сорт prop.
Рантайм-значение 3 может также иметь тип int n, который имеет сорт t@ype, где n — статический терм сорта int (и в данном случае равный 3).
Упомянутый выше список из десяти интов имеет тип list(int, 10), этот тип имеет сорт t@ype (или type, не помню). В статическом терме list(int,10) участвуют статический терм int сорта t@ype и статический терм 10 сорта int. Будучи статическим термом, эта 10 не попадает в рантайм.
DM>>Хочешь рантайм-значение — опиши его явно: где оно создается, куда передается и как связано с остальными.
DG>во, извращенцы! DG>что называется — выберите любые две: сложность решаемой задачи, точность описания, реальное время разработки.
Да, правда. Писать на ATS cложно и медленно. Зато уверенность в корректности получаемого кода over 9000.
DM>>>kind — вид типа данных (или их конструкторов?) DG>>которые живут только в compile-time?
DM>Это ты мне скажи, раз о kind'ах заговорил. Насколько я их понимаю — да. В самом ATS такого явного понятия (как в Хаскеле) нет, вроде.
я это слово вроде как раз в твоем ЖЖ увидел, поэтому и спрашиваю.
DM>>>Хочешь рантайм-значение — опиши его явно: где оно создается, куда передается и как связано с остальными.
DG>>во, извращенцы! DG>>что называется — выберите любые две: сложность решаемой задачи, точность описания, реальное время разработки.
DM>Да, правда. Писать на ATS cложно и медленно. Зато уверенность в корректности получаемого кода over 9000.
из неточного определения часто можно восстановив точное, автоматически выведя детали, если при этом заданы ключевые точки (что, например, и делается при выведении типов — выводится детализированный тип каждой переменной, или при оптимизациях — выводятся детали исполнения каждого мелкого участка кода)
т.е. насколько я понимаю, работа по исследованию — что надо задать, чтобы остальное можно было вывести автоматически — в ATS не проводится?
Здравствуйте, DarkGray, Вы писали:
DG>т.е. насколько я понимаю, работа по исследованию — что надо задать, чтобы остальное можно было вывести автоматически — в ATS не проводится?
Затрудняюсь ответить. В определенных рамках автоматический вывод там есть: решатель арифметических соотношений довольно умен, а доказательства теорем часто выглядят как серия намеков — большую часть текста не приходится выписывать, ее компилятор сам выводит. Но менять за спиной у программиста определения типов и функций, добавлять параметры и вычисления компилятор не считает себя вправе, это момент идеологический. Вплоть до того, что есть явное различие между голой функцией (как в Си), замыканием с данными в управляемой куче и замыканием с данными, освобождаемыми вручную.
Здравствуйте, VladD2, Вы писали:
DM>>Введение в ATS и зависимые типы
VD>Не хочешь объединить это все в полноценную статью и опубликовать на РСДН?
Можно. А в каком объеме и жанре? Сейчас там у меня несколько постов, в них описание не систематическое и неполное, на базе конкретных примеров. Последнее в серии — один очень большой пример с доказательством сортировки smoothsort. Рассказ про smoothsort получился шибко длинным и сложным, его почти никто не осилит, не думаю, что его следует включать. Если же пытаться сделать более полное и систематичное описание языка, это может вылиться в нехилый трактат. К тому же, ряд нетривиальных но интересных фич я еще сам не освоил. Самое простое сейчас — объединить, слегка причесав, три первых поста: введение с примером про фильтрацию IP-адресов, про доказательства и про ограничения арифметики в типах.
Здравствуйте, D. Mon, Вы писали:
DM>Недавно занялся изучением языка ATS — Applied Type System, который еще давно привлек мое внимание очень хорошими скоростными показателями на language shootout. Тогда меня отпугнула многословность решений, а оказывается она там не просто так: ATS содержит систему зависимых типов и конструктивных доказательств, которые поднимают уровень обеспечения коррекности до невиданных высот, вплоть до полного статического доказательства того, что программа делает то, что надо, и не содержит багов. Компилируется язык путем трансляции в Си и использования gcc, что дает ему очень простой FFI и все gcc-шные наработки по оптимизациям. А возможность указания массы условий и инвариантов в типах и их статического доказательства позволяет избежать лишних проверок в рантайме и обеспечить высокую скорость. В языке есть поддержка сборки мусора, но доступно также и подмножество языка, работающее без GC: можно собирать программы без GC, причем корректность работы с памятью обеспечивается системой типов. Документация по языку сильно разрозненная и неполная, но я начал серию постов по-русски с рассказами о фичах ATS доступным языком.
Тоже был когда-то интересен, даже совсем простенькая версия ордербука с поддержкой только рыночных и лимитных ордеров была перепилена с F#, чтобы понять, насколько вкусно поедается кактус.
Еле допилил, ибо пресловутое многословие ATS убило напрочь желание его использовать.
В итоге перекрестился и забыл
А он продолжает жить, и начинаю думать-может попробовать еще раз?
Сам то используешь или тоже забросил?
