Comments 8
А зачем идрис позаимствовал от хаскелла синтаксис, но поменял местами
Чтобы людям было сложнее и вдумчивее портировать хаскельное наследие?
: и ::?Чтобы людям было сложнее и вдумчивее портировать хаскельное наследие?
Синтаксис не так уж строго взят из Haskell: в том же Haskell они поменяны местами, если сравнивать с ML. В Agda тоже используется одно двоеточие для типов и два для списков, что многим представляется более удобным.
Но проблема замечена верно: уже не раз у меня возникали проблемы с двоеточиями при чередовании Agda/Idris с Haskell.
Но проблема замечена верно: уже не раз у меня возникали проблемы с двоеточиями при чередовании Agda/Idris с Haskell.
Есть минимум две причины:
Первая связанная с научной составной типизированного лямбда исчисления, то есть «как принято у ученых». Типизированное лямбда исчисление определяется как формальная грамматика, в которой, как вы поняли, тип как раз указывается через две (а не четыре) точки.
Другая причина связанная с тем, как часто приходится писать тот или иной токен. В этом смысле хаскелисты решили, что cons-конструктор списка они пишут чаще чем тип, и по-этому для списка выбрали более короткой токен. Тогда как Агда/Идрис программисты чаще описывают типы.
Первая связанная с научной составной типизированного лямбда исчисления, то есть «как принято у ученых». Типизированное лямбда исчисление определяется как формальная грамматика, в которой, как вы поняли, тип как раз указывается через две (а не четыре) точки.
Другая причина связанная с тем, как часто приходится писать тот или иной токен. В этом смысле хаскелисты решили, что cons-конструктор списка они пишут чаще чем тип, и по-этому для списка выбрали более короткой токен. Тогда как Агда/Идрис программисты чаще описывают типы.
Было бы интересно послушать про принципы более продвинутого применения этого инструмента. Как его можно использовать для верификации программ, какие шаги предпринимаются для этого? Программы переписывают с помощью Idris, или же его можно как-то натравить на исходники, написанные на других языках (или же на формальные нотации, описывающие сетевые протоколы или структуры данных)? Можно ли его внедрить для реализации каких-то критичных к правильности участков программы? Можно ли на нём сделать какие-нибудь нетривиальные штуки (например, реализовать кусочки приснопамятного SSL) и внедрить их в продакшен?
Тема статической верификации очень интересна и, на мой взгляд, актуальна, но простого доступного материала, к сожалению, очень и очень мало.
Тема статической верификации очень интересна и, на мой взгляд, актуальна, но простого доступного материала, к сожалению, очень и очень мало.
По поводу верификации — есть два основных подхода: первый — постановка и доказательство теорем после написания самой программы, второй — упор на точность спецификации. Программы в обоих случаях должны быть написаны либо на этом языке, либо на языке, интерпретатор которого на нём написан (что сильно усложняет задачу, но иногда бывает полезно). Но, в то же время, верифицировать можно не только программы, но и любые системы, которые мы можем смоделировать — тогда верификация заключается в доказательстве наличия интересующих нас свойств.
Внедрить для реализации критичных участков, по крайней мере в теории, вполне реально: поскольку идёт компиляция в те же C и JS, ничто не мешает вызывать получившиеся функции из этих языков. Но в Idris на данный момент это не приоритет, так что на практике это будет неудобно.
Штуки наподобие SSL, опять-таки в теории, ничто не мешает реализовать; на практике же, как упомянул в статье, язык «необкатан», и прямо сейчас можно стать первооткрывателем багов компилятора. Но цель разработчиков — сделать его пригодным для таких задач.
Внедрить для реализации критичных участков, по крайней мере в теории, вполне реально: поскольку идёт компиляция в те же C и JS, ничто не мешает вызывать получившиеся функции из этих языков. Но в Idris на данный момент это не приоритет, так что на практике это будет неудобно.
Штуки наподобие SSL, опять-таки в теории, ничто не мешает реализовать; на практике же, как упомянул в статье, язык «необкатан», и прямо сейчас можно стать первооткрывателем багов компилятора. Но цель разработчиков — сделать его пригодным для таких задач.
Пропустил вопрос про натравливание на существующий код: нет, это отдельный язык, так что если хочется «натравить» — нужно сформулировать язык-цель на этом языке, т.е. построить целую модель, причём сложную, и потом уже анализировать. Это не слишком практично, а также долго и сложно.
С описаниями протоколов или структур может быть практичнее, но, думаю, тут проще будет говорить о конкретных примерах (протоколов/структур и желаемых доказательств) — они могут быть довольно разными.
С описаниями протоколов или структур может быть практичнее, но, думаю, тут проще будет говорить о конкретных примерах (протоколов/структур и желаемых доказательств) — они могут быть довольно разными.
Отличная статья! Большое спасибо.
Даже имея, пусть и весьма поверхностное, знакомство с хаскелом, не все примеры осилил. Но начало статьи отличное и язык интересный.
Sign up to leave a comment.
Обзор языка Idris