tag:blogger.com,1999:blog-5685240425738948136.post5778154321141882850..comments2023-05-24T13:56:11.840+03:00Comments on Проще пареной репы: Uniqueness types in AgdaDmytrohttp://www.blogger.com/profile/02037025138151611540noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-5685240425738948136.post-61202948099319079832013-01-18T17:30:04.471+02:002013-01-18T17:30:04.471+02:00Агда еще развивается, и я думаю если моя идея окаж...Агда еще развивается, и я думаю если моя идея окажется достаточно удачной, можно будет предложить некоторые изменения в сам язык (я думаю можно обойтись очень минимальными с использованием quote и quoteTerm).<br />Если честно меня больше беспокоит необходимость вставлять доказательство равенства типов (там в примерах refl), тогда как типы хоть и undecidable но все же известны и с использованием рефлексии можно было бы это доказательство вывести автоматически.Dmytrohttps://www.blogger.com/profile/02037025138151611540noreply@blogger.comtag:blogger.com,1999:blog-5685240425738948136.post-85600219593078283952013-01-18T16:27:43.365+02:002013-01-18T16:27:43.365+02:00Интересно, конечно. По моим поверхностным впечатле...Интересно, конечно. По моим поверхностным впечатлениям, тут для счастья не хватает щепотки синтаксического метапрограммирования :) Ну, чтобы биндинги не строками, а идентификаторами хост-языка. Хотя с этим всё чуточку усложнилось бы: ведь пришлось бы ещё при аппликации функций к uniqueness-типизированным аргументам переименовывать соответствующий биндинг текущего контекста в имя аргумента функции, чтобы он правильно заиспользовался в её теле и т.д.Anonymousnoreply@blogger.com