A glimpse of future

[thedeemon]

Agda (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.
оттудова

В глаза еще не видел, но по описанию очень похоже на то, о чем я недавно говорил в посте про будущее программирования.

Comments

[dimitrykakadu.livejournal.com]

Забавно) Хаскеллист-штангист, агдаист-сварщик. А камлист кто?

[thedeemon.livejournal.com]

Это не обязательно про агдаистов.
http://www.anekdot.ru/scripts/anekdotid.php?ids=-2030519007

[nivanych.livejournal.com]

"Сварщик", как показано выше, это из анекдота.
"Штангист" родилось из общения с Сергеем Зефировым и сильно укрепилось после его высказываний про то, что при занятиях спортом голова думает лучше. После это обобщили до всех "небыдло"-знаний типа теории категорий, которой кое-то таки в том же Haskell'е объясняется.