使用翻转类型参数为用户定义的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

写完所有信息后教你如何做,我应该说在任何情况下你绝对不应该这样做.