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

[gds.livejournal.com]

ага, согласен. Но даже тупой пример придумывается сходу: ∀α . list α → option α -- тут очень много функций может быть найдено.
Фактически, нам предлагают часть алгоритма выписывать в виде типов, которые соединяются друг с другом каким-либо очевидным образом.

[thedeemon.livejournal.com]

Помнится, когда Мейер рассказывал про статью Вадлера "Theorems for free", он практически этот пример приводил как демонстрацию обратного. Если мы не имеем другой информации о функции, синтезируем чистые функции (в том числе не замыкания со ссылками на значения из окружения), и стараемся брать самую простую из подходящих, то для ∀α . list α → α кроме как hd и предложить особо нечего.

[gds.livejournal.com]

но почему hd, а не какой-нибудь "последний элемент"?
В случае option α -- так вообще можно легко предложить счётное множество функций, для каждого натурального числа n возвращающее n'ый элемент списка либо None в случае его отсутствия.

[thedeemon.livejournal.com]

Потому что "стараемся брать самую простую из подходящих".

[thedeemon.livejournal.com]

Точнее, самую простую из использующих максимум информации о типах, иначе можно было бы просто возвращать None.

[nivanych.livejournal.com]

Самое простое (например, самое короткое) выражение этого типа.
Всё. Для зависимых типов этого достаточно.
Пример с [a]→a хорошо показывает, что тип может определять много выражений и его надо уточнять.
Можно ещё выдавать несколько выражений с возрастающими сложностями.
Где-то это может и пригодиться...
Но на мой взгляд, уж лучше, задавать тип точнее.

[gds.livejournal.com]

да ну, унылое говно ведь это. Я за неявные фишки (правда, касаемо планировщика) уже говорил, про это тем более скажу.
Понятно, что зависимые типы делают так, что в некоторых случаях оно катит, но всё же.

[nivanych.livejournal.com]

Почему это унылое? Весёлое, бодрое!
Код по спецификации так генерить, это не ерунда, всё-таки.
Те же RFC довольно чотко описывают.
Ну и есть одно применение, когда качество сгенерированного почти похер — это доказательства.