使用翻转类型参数为用户定义的 Vect 版本实现可折叠

Question

我已经定义了自己的Vect数据类型如下

data MyVect : (n : Nat) -> (t : Type) -> Type where
  Nil  : MyVect Z t
  (::) : (x : t) -> (xs : MyVect n t) -> MyVect (S n) t

然后开始为数据类型实现Foldable接口

Foldable MyVect where
  foldr = ?res2

但是在重新加载文件时，Idris 抱怨

When checking argument t to type constructor Prelude.Foldable.Foldable:
        Type mismatch between
                Nat -> Type -> Type (Type of MyVect)
        and
                Type -> Type (Expected type)

        Specifically:
                Type mismatch between
                        Nat
                and
                        TypeUnification failure

摸了摸头，我猜我可以通过编写来满足 Idris 对类型构造函数的要求

Foldable (MyVect n) where
  foldr = ?res2

然后我开始思考“如果我定义 MyVect 并翻转类型参数会怎样？...”

data MyVect : (t : Type) -> (n : Nat) -> Type where
  Nil  : MyVect t Z
  (::) : (x : t) -> (xs : MyVect t n) -> MyVect t (S n)

是否可以为MyVect 的“参数翻转”版本实现可折叠接口？ （以及如何？）

Answer 1

您看到的类型错误的来源是Foldable：

Idris> :t Foldable 
Foldable : (Type -> Type) -> Type

而您的MyVect 的第一个版本具有类型：

Idris> :t MyVect 
MyVect : Nat -> Type -> Type

第二个有：

Idris> :t MyVect 
MyVect : Type -> Nat -> Type

你是对的，你可以像使用普通的旧函数一样部分应用类型。

因此Foldable (MyVect n) 有效，因为MyVect n 具有Type -> Type 类型，这正是Foldable 接口想要的。

在我们确信类型的行为类似于函数之后，您可以为 MyVect 提供翻转的类型别名，一切都会正常工作：

FlippedVect : Nat -> Type -> Type
FlippedVect n t = MyVect t n

Foldable (FlippedVect n) where

你也可以使用已经定义的函数来实现类似的东西：

Idris> :t flip
flip : (a -> b -> c) -> b -> a -> c
Idris> :t flip MyVect
flip MyVect : Nat -> Type -> Type

现在你可以写了：

Foldable (flip MyVect n) where

您甚至可以为匿名函数定义实例。这是完整版：

Foldable (\a => MyVect a n) where
  foldr f z Nil = z
  foldr {n=S k} f z (x :: xs) = x `f` foldr {t=\a => MyVect a k} f z xs

  foldl = believe_me  -- i'm on Idris-0.12.3, I got type errors for `foldl`
                      -- but you can implement it in the same way

在写了所有信息来教你如何做之后，我应该说在任何情况下你绝对不应该这样做。