Здравствуйте, 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.
