functional-programmingmatrix-transformidris2

Transpose Vector Matrix in Idris2 With Dependant Types

I have trouble figuring out what my Idris2 Type- or Compile-Error is about, so I thought I could ask some Idris2 Veterans or Enthusiasts to give me some explanation on how I can make my approach work or why it cannot work like that. Any additional information and in-depth advice is always highly appreciated as I want to use the knowledge to convert stuff from Haskell to Idris2 for proveable structures etc.

The General solution that I already know is this one (with all helper Functions):

data Vect : (len : Nat) -> (a : Type) -> Type where
  Nil  : Vect 0 a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith f []        []         = []
zipWith f (x :: xs) (y :: ys)  = f x y :: zipWith f xs ys


replicate : (n : Nat) -> a -> Vect n a
replicate 0     _  = []
replicate (S k) va = va :: replicate k va

replicate' : {n : _} -> a -> Vect n a
replicate' = replicate n


transpose : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose [] = replicate' []
transpose (xs::xss) = zipWith (::) xs (transpose xss)

That was the Solution from the GitHub Guide I was learning with.

Now my approach:

transLines : Vect n (Vect (S m) a) -> Vect n a
transLines [] = []
transLines ((x :: _) :: xss) = x :: transLines xss

dropLines : Vect n (Vect (S m) a) -> Vect n (Vect m a)
dropLines [] = []
dropLines ((_ :: xs) :: xss) = xs :: dropLines xss


transpose' : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose' {m = 0} [] = []
transpose' ([]:: _) = []
transpose' ma = (transLines ma) :: transpose' (dropLines ma)

I know what specifically does not work, the types from "Vect n (Vect m a)" and "Vect ?n (Vect (S ?m) a)" cannot match when I call "droplines ma" in the transpose function, but that right there is where im stuck, I dont know if it is possible to change some definitions so that it works, or if the approach as a whole is just not doable with Dependant types.

Thank you in advance and Cheers

Solution

  • Your approach works fine if you just pattern match properly:

    transpose' : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose' {m = 0} ma = []
transpose' {m = S m'} ma = transLines ma :: transpose' (dropLines ma)