How to rewrite a function body in Idris so that the type corresponds to the function signature and the whole thing compiles

8
votes

I would like for this to compile:

foo: Vect n String -> Vect n String
foo {n} xs = take n xs

This fails to compile because the compiler cannot unify n with n + m. I understand that this is because of the signature of take for Vect's but I cannot figure out how to go about showing the compiler that they can be unified if m = 0.

2
dependent-typeidris
where does m is defined ? – Guillaume Massé
m is a type variable from Vector.take – max taldykin
What is the function intended to do? The type indicates that the length of the output list (n) is the same as the length of the input (n), and the only way to achieve that is for the output to be the input... The implementation, on the other hand, suggests that you want the length of the output to be exactly n, where that is not necessarily the length of the input. – Edwin Brady
@EdwinBrady But n is the length of the input. Does the type declaration not say so or are all of the n's in the above code not all one and the same? – jedesah
@UndercoverAgent Yes, they are - the thing that confused me here was what the take was intended for, since it's always going to result in xs. Or is this part of something larger? I have a more concise solution anyway, which I'll give as a proper answer rather than a comment. – Edwin Brady

2 Answers

6
votes

Just to add to the previous answer, one other possibility is to do the rewrite inline using the existing plusZeroRightNeutral lemma from the library:

foo: Vect n String -> Vect n String
foo {n} xs = let xs' : Vect (n + 0) String
                     = rewrite (plusZeroRightNeutral n) in xs in
                 take n xs'

The difficulty Idris is having in unification is because it is unwilling to infer the m in the application of take:

take : (n : Nat) -> Vect (n + m) a -> Vect n a

You've given it a Vect n String where it wanted a Vect (n + m) a - it has happily unified the a with the String, because Vect is a type constructor, but is unwilling to unify n with n + m because, in general, it can't invert functions. You and I can tell that m has to be zero, but Idris is not so clever.

3
votes

Idris can't unify n with n + m because it does not know that n = n + 0. You need to help him by manually proving that.

First of all, why it needs this proof. The reason is that take expects Vect (n+m) a:

Idris> :t Vect.take
Prelude.Vect.take : (n : Nat) -> Vect (n + m) a -> Vect n a

So, this will typecheck

foo: Vect (n + 0) String -> Vect n String
foo {n} xs = take n xs

You need a way to convert Vect n a to Vect (n + 0) a:

addNothing : {n : Nat} -> {a : Type} -> Vect n a -> Vect (n+Z) a

It is possible with replace function:

Idris> :t replace
replace : (x = y) -> P x -> P y

But now you need a proof that n = n + 0. Here it is (with the rest of the code):

plusAddZero : (n : Nat) -> n = n + 0
plusAddZero = proof
  intros
  rewrite (plusCommutative n 0)
  trivial

addNothing : {n : Nat} -> {a : Type} -> Vect n a -> Vect (n + 0) a
addNothing {n} {a} = replace {P = \m => Vect m a} (plusAddZero n)

foo : Vect n String -> Vect n String
foo {n} xs = Vect.take n (addNothing xs)

Seems like too much for such a simple function. Hope someone will show more concise solution.