为什么Idris不接受我的定制折叠？

Question

这是一个向量,其元素由向量的长度索引.

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类型不会在Idris检查？

Answer 1

伊德里斯正在将你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)