Автоматическое определение домена для функции зависимого типа в Idris

Question

В учебнике по языку Идрис есть простой и понятный пример идеи зависимых типов: http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html

Вот код:

isSingleton : Bool -> Type
isSingleton True = Int
isSingleton False = List Int

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

sum : (single : Bool) -> isSingleton single -> Int
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs

Я решил потратить больше времени на этот пример. Что меня беспокоит в sum функция в том, что мне нужно явно передать single : Bool значение для функции. Я не хочу этого делать и хочу, чтобы компилятор угадал, каким должно быть это логическое значение. Следовательно я прохожу только Int или же List Int в sum функция должна быть взаимно-однозначным соответствием между логическим значением и типом аргумента (если я передаю какой-то другой тип, это просто не должно проверять тип).

Конечно, я понимаю, что это невозможно в общем случае. Такие трюки компилятора требуют моей функции isSingleton (или любая другая подобная функция) быть инъективным. Но для этого случая это должно быть возможно, как мне кажется...

Итак, я начал со следующей реализации: я только что сделал single аргумент неявный.

sum : {single : Bool} -> isSingleton single -> Int
sum {single = True} x = x
sum {single = False} [] = 0
sum {single = False} (x :: xs) = x + sum' {single = False} xs

Ну, это действительно не решает мою проблему, потому что мне все еще нужно вызывать эту функцию следующим образом:

sum {single=True} 1

Но я прочитал в учебнике о auto ключевое слово. Хотя я не совсем понимаю, что auto делает (потому что я не нашел описание этого), я решил немного исправить свою функцию:

sum' : {auto single : Bool} -> isSingleton single -> Int
sum' {single = True} x = x
sum' {single = False} [] = 0
sum' {single = False} (x :: xs) = x + sum' {single = False} xs

И это работает для списков!

*DepFun> :t sum'
sum' : {auto single : Bool} -> isSingleton single -> Int
*DepFun> sum' [1,2,3]
6 : Int

Но не работает для одного значения:(

*DepFun> sum' 3
When checking an application of function Main.sum':
        List Int is not a numeric type

Может кто-нибудь объяснить, возможно ли в действительности достичь моей цели при использовании таких инъекционных функций в настоящее время? Я смотрел это короткое видео о доказательстве чего-либо, это инъекция: https://www.youtube.com/watch?v=7Ml8u7DFgAk

Но я не понимаю, как я могу использовать такие доказательства в моем примере. Если это невозможно, как лучше написать такие функции?

Answer 1

auto Ключевое слово в основном говорит Идрису: "Найди мне любое значение этого типа". Таким образом, вы можете получить неправильный ответ, если этот тип не содержит только одно значение. Идрис видит {auto x : Bool} и заполняет его любым старым Boolа именно False, Он не использует свои знания более поздних аргументов, чтобы помочь ему выбрать - информация не течет справа налево.

Одним из исправлений было бы сделать поток информации в другом направлении. Вместо того чтобы использовать конструкцию в стиле юниверса, как описано выше, напишите функцию, принимающую произвольный тип, и используйте предикат, чтобы уточнить его до двух требуемых параметров. Таким образом, Идрис может посмотреть на тип предыдущего аргумента и выбрать единственное значение IsListOrInt чей тип соответствует.

data IsListOrInt a where
    IsInt : IsListOrInt Int
    IsList : IsListOrInt (List Int)

sum : a -> {auto isListOrInt : IsListOrInt a} -> Int
sum x {IsInt} = x
sum [] {IsList} = 0
sum (x :: xs) {IsList} = x + sum xs

Теперь, в этом случае пространство поиска достаточно мало (два значения - True а также False) что Идрис мог реально исследовать каждую опцию методом грубой силы и выбрать первый вариант, который приводит к программе, которая проходит проверку типов, но этот алгоритм плохо масштабируется, когда типы намного больше двух или при попытке вывести несколько значений.

Сравните слева направо характер информационного потока в приведенном выше примере с поведением обычного неauto фигурные скобки, которые инструктируют Идриса находить результат в двух направлениях, используя объединение. Как вы заметили, это может быть успешным только в том случае, если рассматриваемые функции типов инъективны. Вы можете структурировать свой ввод как отдельный индексированный тип данных и позволить Idris взглянуть на конструктор, чтобы найти b используя унификацию.

data OneOrMany isOne where
    One : Int -> OneOrMany True
    Many : List Int -> OneOrMany False

sum : {b : Bool} -> OneOrMany b -> Int
sum (One x) = x
sum (Many []) = 0
sum (Many (x :: xs)) = x + sum (Many xs)

test = sum (One 3) + sum (Many [29, 43])

Предсказание, когда машина будет или не сможет угадать, что вы имеете в виду, является важным навыком в программировании с зависимой типизацией; вы поймете, что становитесь лучше в этом с большим опытом.

Конечно, в данном случае это все спорно, потому что списки уже есть один или много-семантики. Напишите свою функцию поверх простых старых списков; затем, если вам нужно применить его к одному значению, вы можете просто обернуть его в единый список.