Почему Idris не принимает мой пользовательский фолд?

Вот вектор, элементы которого индексируются по длине вектора.

data IxVect : (n : Nat) -> (a : Nat -> Type) -> Type where
    Nil : IxVect 0 a
    (::) : a n -> IxVect n a -> IxVect (S n) a

Я хочу сложить IxVect.

total
foldr : {b : Nat -> Type} -> ({m : Nat} -> a m -> b m -> b (S m)) -> b Z -> IxVect n a -> b n
foldr f z Nil = z
foldr f z (x :: xs) = f x (foldr f z xs)

Я получаю следующую ошибку в случае шага:

test.idr:9:25:
When elaborating right hand side of Main.foldr:
Can't convert
        (Nat -> Type) -> Type
with
        Type -> Type

Я смущен тем, что ошибка пытается сказать мне. Мое определение foldr не кажется мне неправильным, и оно отлично работает в Haskell:

data Nat = Z | S Nat

data IxVect n a where
    Nil :: IxVect Z a
    Cons :: a n -> IxVect n a -> IxVect (S n) a

foldr :: (forall m. a m -> b m -> b (S m)) -> b Z -> IxVect n a -> b n
foldr f z Nil = z
foldr f z (Cons x xs) = f x (foldr f z xs)

Почему мой тип foldr не проверяется в Идрисе?


fold haskell dependent-type idris
person Benjamin Hodgson♦    schedule 25.07.2015    source источник
comment
Текущий мастер Idris на github намного лучше справляется с устранением неоднозначности имен по типу (и действительно намного лучше сообщает об ошибках, когда он терпит неудачу). Ваш пример работает нормально, без изменений. Совсем скоро будет новый выпуск.   -  person Edwin Brady    schedule 25.07.2015

Ответы (1)


arrow_upward
8
arrow_downward

Идрис смешивает ваш foldr с уже существующим. Вы можете решить эту проблему, уточнив рекурсивное вхождение foldr или переименовав файл foldr.

foldr : 
     {n : Nat} -> {a, b : Nat -> Type} 
  -> ({m : Nat} -> a m -> b m -> b (S m)) -> b Z -> IxVect n a -> b n
foldr f z Nil = z
foldr f z (x :: xs) = f x (Main.foldr f z xs)
person András Kovács    schedule 25.07.2015
comment
Бинго! Большое спасибо. Это сообщение об ошибке вообще ничего не объясняет :( - person Benjamin Hodgson♦; 25.07.2015