How to write correct type signature for Vect in Idris?

Question

Recently I have been exploring dependent types in Idris. However, I overcome to a problem which is quite annoying, which is in Idris, I should start my program with type signature. So the problem is, How Can I write concise type signature in Idris?

For example,

get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String))
get_member store idx = Vect.mapMaybe maybe_member (Vect.fromList idx)
  where
    maybe_member : (x : Fin n) -> Maybe (Nat, String)
-- The below line should be type corrected
-- maybe_member x = Just (Data.Fin.finToNat x, Vect.index x store)

If I comment the last line, the compile will type-check the above function, but if I make the last line as expression, the compile will complain.

When checking right hand side of VecSort.get_member, maybe_member with expected type
        Maybe (Nat, String)
When checking an application of function Data.Vect.index:
        Type mismatch between
                Vect n1 String (Type of store)
        and
                Vect n String (Expected type)

        Specifically:
                Type mismatch between
                        n1
                and
                        n

But I do it as lambda function,

get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String))
get_member store idx = Vect.mapMaybe (\x => Just (Data.Fin.finToNat x, Vect.index x store)) (Vect.fromList idx)

it will be type-check as well.

So the question is, how should I define Vect type with the correct length in the type signature?

Markus Markus · Accepted Answer · 2017-08-14T08:35:58

I am not sure if my explanation is correct, but the following typechecks:

get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String))
get_member store idx {n} = Vect.mapMaybe (maybe_member) (Vect.fromList idx)
    where
      maybe_member : (x : Fin n) -> Maybe (Nat, String)
      maybe_member x = Just (Data.Fin.finToNat x, Vect.index x store)

The difference is that you get the implicit parameter n into your scope. This {n} and x: Fin x refer both to the same n. Without pulling the implicit n in your scope, idris cannot assume that both ns are indeed the same, and it will complain with the error message that it does not know wheter n1 and n are the same.

How to write correct type signature for Vect in Idris?

1 Answers