Разделение вектора в Идрисе: почему нельзя объединить 0 и m+n?

Question

Я хотел бы разделить вектор на два новых вектора.

Мы не можем знать, какова будет длина отдельных векторов, но сумма полученных векторов должна быть равна аргументу. Я попытался захватить это свойство следующим образом:

partition : (a -> Bool) -> Vect (m+n) a -> (Vect m a, Vect n a)
partition p [] = ([], [])
partition p (x::xs)
  = let (ys,zs) = partition p xs
  in case p xs of
    True  => (x::ys, zs)
    False => (ys, zs)

Но Идрис сообщает (указывая на "раздел p []"), что при разработке левой части Main.partition:

Can't unify
        Vect 0 a
with
        Vect (m + n) a

Specifically:
        Can't unify
                0
        with
                plus m n

Почему это так?

Мне кажется совершенно очевидным, что если "0 = m + n", то m = n = 0. Как можно убедить Идриса в этом?

Answer 1

Помните, что объединение - это синтаксическая операция, которая в таких языках, как Idris, дополняется прямым сокращением в соответствии с сопоставлением с образцом. Он не знает всех фактов, которые мы можем доказать!

Конечно, мы можем доказать в Идрисе, что если n+m=0, то m = 0 и n = 0:

sumZero : (n, m : Nat) -> plus n m = Z -> (n=Z, m=Z)
sumZero Z m prf = (refl, prf)
sumZero (S k) m refl impossible

но это не дает объединителю знать об этом факте, поскольку это делает проверку типов неразрешимой.

Возвращаясь к исходному вопросу: если я перевожу тип вашего раздела на английский, будет написано "для всех натуральных чисел". m а также nдля всех логических предикатов p над aс учетом вектора длины plus m nЯ могу получить пару, состоящую из вектора длины m и вектор длины n"Другими словами, чтобы вызвать вашу функцию, мне нужно знать заранее, сколько элементов вектора удовлетворяет предикату, потому что мне нужно указать m а также n на сайте звонка!

Я думаю, что вы действительно хотите это partition функция, которая, учитывая вектор длины n, возвращает пару векторов, длина которых составляет n, Мы можем выразить это, используя зависимую пару, которая является версией экзистенциальной квантификации в теории типов. Перевод "пары векторов, длины которых складываются в n"есть" существует m а также m' и векторы с такими длинами, что сумма m а также m' мой вклад n".

Этот тип выглядит так:

partition : (a -> Bool) -> Vect n a -> (m ** (m' ** (Vect m a, Vect m' a, m+m'=n)))

и полная реализация выглядит так:

partition : (a -> Bool) -> Vect n a -> (m ** (m' ** (Vect m a, Vect m' a, m+m'=n)))
partition p [] = (Z ** (Z ** ([], [], refl)))
partition p (x :: xs) with (p x, partition p xs)
  | (True, (m ** (m' ** (ys, ns, refl)))) = (S m ** (m' ** (x::ys, ns, refl)))
  | (False, (m ** (m' ** (ys, ns, refl)))) =
      (m ** (S m' ** (ys, x::ns, sym (plusSuccRightSucc m m'))))

Это немного глоток, так что давайте разберемся. Чтобы реализовать функцию, мы начнем с сопоставления с образцом на входе Vect:

partition p [] = (Z ** (Z ** ([], [], refl)))

Обратите внимание, что единственный возможный вывод - это то, что находится справа, иначе мы не могли бы построить refl, Мы знаем это n является Z из-за объединения n с индексом конструктора Nil из Vect,

В рекурсивном случае мы рассмотрим первый элемент вектора. Здесь я использую with правило, потому что это читабельно, но мы могли бы использовать if на правой стороне вместо сопоставления на p x налево.

partition p (x :: xs) with (p x, partition p xs)

в True В этом случае мы добавляем элемент в первый подвектор. Так как plus сводится к первому аргументу, мы можем построить доказательство равенства, используя refl потому что сложение становится абсолютно правильным:

  | (True, (m ** (m' ** (ys, ns, refl)))) = (S m ** (m' ** (x::ys, ns, refl)))

в False случае, нам нужно сделать немного больше работы, потому что plus m (S m') не может объединиться с S (plus m m'), Помните, как я сказал, что объединение не имеет доступа к равенствам, которые мы можем доказать? Функция библиотеки plusSuccRightSucc делает то, что нам нужно, хотя:

  | (False, (m ** (m' ** (ys, ns, refl)))) =
      (m ** (S m' ** (ys, x::ns, sym (plusSuccRightSucc m m'))))

Для справки, тип plusSuccRightSucc является:

plusSuccRightSucc : (left : Nat) ->
                    (right : Nat) ->
                    S (plus left right) = plus left (S right)

и тип sym является:

sym : (l = r) -> r = l

Единственное, чего не хватает в приведенной выше функции, так это того факта, что функция на самом деле разделяет Vect, Мы можем добавить это, сделав векторы результата состоящими из зависимых пар элементов и доказательством того, что каждый элемент удовлетворяет p или же not p:

partition' : (p : a -> Bool) ->
             (xs : Vect n a) ->
             (m ** (m' ** (Vect m (y : a ** so (p y)),
                           Vect m' (y : a ** so (not (p y))),
                           m+m'=n)))
partition' p [] = (0 ** (0 ** ([], [], refl)))
partition' p (x :: xs) with (choose (p x), partition' p xs)
  partition' p (x :: xs) | (Left oh, (m ** (m' ** (ys, ns, refl)))) =
    (S m ** (m' ** ((x ** oh)::ys, ns, refl)))
  partition' p (x :: xs) | (Right oh, (m ** (m' ** (ys, ns, refl)))) =
    (m ** (S m' ** (ys, (x ** oh)::ns, sym (plusSuccRightSucc m m'))))

Если вы хотите стать еще более безумным, вы также можете заставить каждый элемент доказать, что это был элемент входного вектора и что все элементы входного вектора находятся на выходе ровно один раз, и так далее. Зависимые типы предоставляют вам инструменты для выполнения этих задач, но в каждом случае стоит учитывать компромисс со сложностью.