Implementing Foldable for a user defined version of Vect with flipped type parameters

Question

I have 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 started to implement the Foldable interface for the data type

Foldable MyVect where
  foldr = ?res2

However when reloading the file, Idris complaints

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

After scratching my head a bit, I guessed that I could obey Idris demands for the type constructor by writing

Foldable (MyVect n) where
  foldr = ?res2

Then I started to think "what if I had defined MyVect with the type parameters 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 'parameter-flipped' version of MyVect? (and how?)

Shersh Shersh · Accepted Answer · 2017-03-12T20:01:09

The source of type errors you see is in type of Foldable:

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

Whereas your first version of MyVect has type:

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

and second one has:

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

You're right that you can partially apply types as you can do with plain old functions.

Thus Foldable (MyVect n) works because MyVect n has type Type -> Type which is exactly what Foldable interface wants.

After we convinced ourselves that types behaves like functions you can come up with flipped type aliases for MyVect and everything will work:

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

Foldable (FlippedVect n) where

You can also use already defined functions to implement similar stuff:

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

And now you can write:

Foldable (flip MyVect n) where

You can even define instance for anonymous functions. Here is complete version:

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

After writing all that information to teach you how to do it I should say that under any circumstances you definitely shouldn't do it.

Implementing Foldable for a user defined version of Vect with flipped type parameters

1 Answers