По направлению к COQ'у
Jun. 19th, 2009 09:00 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
deniokSimon Peyton Jones, Chung-Chieh Shan и Oleg Kiselyov обещают статью "Fun with type functions", а пока выложили слайды. После впечатляющих примеров на Хаскелле с использованием индексированных семейств типов и функций над типами, радует замечание на последнем слайде:
At some point it may be best to say “enough fooling around: just use Coq”. But we aren’t there yet.
Хорошее, годное замечание.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2009-06-19 09:42 pm (UTC)no subject
Date: 2009-06-20 07:04 am (UTC)no subject
Date: 2009-06-20 07:06 am (UTC)http://haskell.org/haskellwiki/Simonpj/Talk:FunWithTypeFuns
no subject
Date: 2009-06-20 07:28 am (UTC)no subject
Date: 2009-06-20 01:10 pm (UTC)Глядишь, люди и прислушиваться начнут ;-)
no subject
Date: 2009-06-20 01:45 pm (UTC)no subject
Date: 2009-06-20 01:47 pm (UTC)А кое-где даже и принесёт неудобство в связи
с отсутствием общей рекурсии (думать больше придётся).
no subject
Date: 2009-06-20 01:53 pm (UTC)На Хацкеле-то вон люди и бухгалтерию делают..
no subject
Date: 2009-06-20 02:04 pm (UTC)так что, значительную часть
можно делать и на коке.
Но я не слышал, чтобы на нём
хоть кто-то делал прикладные программы...
no subject
Date: 2009-06-20 02:06 pm (UTC)no subject
Date: 2009-06-20 02:10 pm (UTC)Микроскоп должен быть удобным ;-)
no subject
Date: 2009-06-20 02:15 pm (UTC)no subject
Date: 2009-06-20 02:28 pm (UTC)Так-то, сделать удобства типа
того же хаскелевого IO, библиотеки,
и уже вполне можно было бы
"промышленно" программировать на Coq.
Но мне больше нравится Agda.
Но в Coq с доказательствами лучше.
Хоть мне и не нравится способ,
которым они сделали улучшения.
no subject
Date: 2009-06-20 02:20 pm (UTC)"Category theory is quite the most general and abstract branch of pure mathematics. [ . . . ] The corollary of a high degree of generality and abstraction is that the theory gives almost no assistance in solving the more specific problems within any of the subdisciplines to which it applies. It is a tool for the generalist, of little benefit to the practitioner [ . . . ]."
no subject
Date: 2009-06-20 02:29 pm (UTC)Но чем сложнее задача,
тем выше уровень "generality".
Главное, чтобы для простых вещей
оно не становилось сложнее.