Foldable implementation for custom version of Vect with flip type options

Question

I defined my own Vect data type as follows

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

And then he began to implement the Foldable interface for the data type

Foldable MyVect where
  foldr = ?res2

However, when Idris complaint file is reloaded

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

Scratching my head a little, I guessed that I could obey Idris' requirements for a type constructor by writing

Foldable (MyVect n) where
  foldr = ?res2

Then I started thinking "what if I defined MyVect with parameters of type flipped? ..."

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

Is it possible to implement the Foldable interface for this version with a modified parameter MyVect? (And How?)

Answer 1

The source of errors of the type you see is in the type 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.

, , , flapped 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

, , , , .