A glimpse of future
May. 1st, 2011 03:13 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonAgda (from version 2.2.6) has a command, ‘Auto’, which searches for type inhabitants. It can be used as an aid when interactively constructing terms in Agda. In a system with dependent types it can be meaningful to use such a tool for finding fragments of, not only proofs, but also programs. For instance, giving the type signature of the map function over vectors, you will get the desired function as the first solution.
The tool is based on a term search implementation independent of Agda called ‘Agsy’. Agsy is a general purpose search algorithm for a dependently typed language similar to Agda. One shouldn’t expect it to handle large problems of any particular kind, but small enough problems of almost any kind.
Any solution coming from Auto is checked by Agda.
оттудова
В глаза еще не видел, но по описанию очень похоже на то, о чем я недавно говорил в посте про будущее программирования.
The tool is based on a term search implementation independent of Agda called ‘Agsy’. Agsy is a general purpose search algorithm for a dependently typed language similar to Agda. One shouldn’t expect it to handle large problems of any particular kind, but small enough problems of almost any kind.
Any solution coming from Auto is checked by Agda.
оттудова
В глаза еще не видел, но по описанию очень похоже на то, о чем я недавно говорил в посте про будущее программирования.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2011-05-01 11:25 am (UTC)no subject
Date: 2011-05-01 01:09 pm (UTC)Фактически, нам предлагают часть алгоритма выписывать в виде типов, которые соединяются друг с другом каким-либо очевидным образом.
no subject
Date: 2011-05-01 03:57 pm (UTC)no subject
Date: 2011-05-01 04:36 pm (UTC)В случае option α -- так вообще можно легко предложить счётное множество функций, для каждого натурального числа n возвращающее n'ый элемент списка либо None в случае его отсутствия.
no subject
Date: 2011-05-02 03:01 am (UTC)no subject
Date: 2011-05-02 03:04 am (UTC)no subject
Date: 2011-05-02 09:18 am (UTC)Всё. Для зависимых типов этого достаточно.
Пример с [a]→a хорошо показывает, что тип может определять много выражений и его надо уточнять.
Можно ещё выдавать несколько выражений с возрастающими сложностями.
Где-то это может и пригодиться...
Но на мой взгляд, уж лучше, задавать тип точнее.
no subject
Date: 2011-05-02 12:13 pm (UTC)Понятно, что зависимые типы делают так, что в некоторых случаях оно катит, но всё же.
no subject
Date: 2011-05-02 12:25 pm (UTC)Код по спецификации так генерить, это не ерунда, всё-таки.
Те же RFC довольно чотко описывают.
Ну и есть одно применение, когда качество сгенерированного почти похер — это доказательства.
no subject
Date: 2011-05-02 09:32 am (UTC)no subject
Date: 2011-05-02 10:00 am (UTC)no subject
Date: 2011-05-02 10:37 am (UTC)no subject
Date: 2011-05-02 10:51 am (UTC)http://www.anekdot.ru/scripts/anekdotid.php?ids=-2030519007
no subject
Date: 2011-05-02 03:56 pm (UTC)"Штангист" родилось из общения с Сергеем Зефировым и сильно укрепилось после его высказываний про то, что при занятиях спортом голова думает лучше. После это обобщили до всех "небыдло"-знаний типа теории категорий, которой кое-то таки в том же Haskell'е объясняется.
no subject
Date: 2011-05-02 03:51 pm (UTC)http://wiki.portal.chalmers.se/agda/pmwiki.php
Я не думаю, что кто-то делал бы туториал специально для знающих OCaml или Haskell.