У меня есть компилятор, и я ищу библиотеку, которая могла бы выполнять проверку типов для меня. Пока ничего полезного не нашел=/ Кто-нибудь знает хорошие библиотеки для проверки типов? Я использую Haskell, но я рассмотрю любой другой язык, если библиотека хорошая =)
Библиотеки проверки типов
comment
Около 100% проверки типов зависит от (реализованной) системы типов языка и IR/AST компилятора. Я не думаю, что вы можете написать библиотеку на эту тему...
- person schedule 06.12.2010
comment
Вы можете написать средство доказательства теорем, так что вы также можете написать библиотеку проверки типов. Я не понимаю, почему это было бы невозможно.
- person Marek Sapota schedule 06.12.2010
comment
На каком языке вы собираетесь компилировать?
- person wlangstroth schedule 06.12.2010
comment
@maarons: не столько невозможно, сколько непрактично: он будет применять определенный формат IR (и / или потребует от вас написания большого количества связующего кода), и он может справиться только с любой системой (системами) типа, которую библиотека пытается реализовать. .
- person schedule 06.12.2010
comment
@Will: Типизированный диалект Лиспа, но система типов может быть простой.
- person Marek Sapota schedule 06.12.2010
comment
@delan: я не думаю, что потребуется большая часть связующего кода. Насчет системы типов - да, это правильно, и я бы с этим согласился.
- person Marek Sapota schedule 06.12.2010
comment
@maarons: просто, поскольку вы просто хотите иметь доступ к примитивам, или просто, поскольку вам нужны базовые типы для реализации более высокого уровня, или ...?
- person wlangstroth schedule 06.12.2010
comment
@Will: Меня не очень волнует выразительность системы типов - я не ограничен каким-либо языковым стандартом, поэтому я рассмотрю любую библиотеку проверки типов.
- person Marek Sapota schedule 06.12.2010
comment
Вам серьезно нужно подумать о проверке типов и выводе типов. Откровенно говоря, проверка типов тривиальна для любого языка без зависимых типов. У вас есть AST, у вас есть среда типизации, которую вы создаете по ходу работы с типами данных идентификаторов, и вы просто проверяете, что они совпадают, продолжая перемещаться по AST.
- person sclv schedule 09.12.2010
Ответы (3)
Могут быть библиотеки, которые помогут с битами проверки типов, особенно если вам действительно нужна проверка типов, а не вывод типов. Например, были библиотеки, встраивающие логическое программирование в Haskell — на высоте 10 000 футов кажется немного проще написать средство проверки типов, используя логическое программирование, чем функциональное программирование (например, Chameleon, упомянутый shapr выше, основан на на языке CHR, встроенном в Haskell).
Тем не менее, программирование встроенной логики в Haskell — это большой шаг с, возможно, небольшой документацией, если вы никогда раньше не писали средства проверки типов. Точно так же грамматики атрибутов (т. е. UUAG) — это приятный формализм, предоставляющий довольно много механизмов, которые вам понадобятся для написания самостоятельно, но они могут поставить вас в место с несколькими указателями, если вы никогда раньше их не использовали.
Если вы раньше не писали средство проверки типов, возможно, лучше не беспокоиться о библиотеках и работать над процессом с нуля. Статья Марка П. Джонса «Типирование Haskell в Haskell», вероятно, является такой же хорошей отправной точкой, как и любая другая.
person
stephen tetley
schedule
07.12.2010
Похоже хороших готовых решений нет и придется делать самому. Бумага кажется весьма полезной, спасибо.
- person Marek Sapota; 07.12.2010
Однажды я спросил кого-то, какой кусок кода им больше всего понравился. Он на мгновение задумался, а затем сказал: проверка типов для (какого-то компилятора). :-)
- person Edward Z. Yang; 08.12.2010
Я нашел несколько средств проверки типов на hackage, в том числе dedukti, гибрид и lambdacube, возможно, один из них сработает?
person
John L
schedule
07.12.2010
дедукти не строится, а два других кажутся мёртвыми=/
- person Marek Sapota; 07.12.2010
