實現可摺疊的的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 MyVect where 
    foldr = ?res2 

的摺疊式接口

然而重新加載該文件時，伊德里斯投訴

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 

劃傷後荷蘭國際集團我的頭一下，我猜我會服從伊德里斯的類型構造要求寫

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 

你是對的，你可以n可以像使用普通舊功能一樣部分應用類型。

因此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 

寫入所有的信息，教你如何做，我應該說，在任何情況下，你絕對不應該這樣做了。