CODEWITHSUNDEEP
typesfunctional-programmingidrisdependent-type
Ace shinigami
Ace shinigami

Reputation: 1484

type of Idris chop

I'm trying to write a chop function in Idris. The Haskell equivlant would look like:

chop :: Int -> [t] -> [[t]]
chop n [] = []
chop n v = take n v : chop n (drop n v)

my initial attempt in Idris looks like:

chop : (n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop n Nil = Nil
chop n v = (take n v) :: (chop n (drop n v))

type checking error:

Type mismatch between
               Vect 0 a (Type of [])
       and
               Vect (mult k n) a (Expected type)

       Specifically:
               Type mismatch between
                       0
               and
                       mult k n

Upvotes: 2

Views: 71

Answers (1)

xash
xash

Reputation: 3722

k can still be set as an argument, i.e. chop {k=3} Z [] would result in [[], [], []] : Vect 3 (Vect Z a). Your implementation would return chop n Nil = [], so Idris' type system correctly complains. :-)

You need to consider k:

chop : (n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop {k} n v = ?hole

If you want the actual implementation, here is a spoiler:

It is quite similar to yours. Because mult recurses on the first argument (k in this case), chop's recursion should also follow k:
chop {k = Z} n v = []
chop {k = (S k)} n v = take n v :: chop n (drop n v)

Another approach is to specify how many blocks you want instead of how big each block is.

chop' : (k : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop' Z v = []
chop' {n} (S k) v = take n v :: chop k (drop n v)

n needs to be in scope to call take and drop.

Upvotes: 2

Related Questions