Search code examples
idris

Type checking for Vectors in Idris

From REPL how does not ensures that the a list is indeed interpret as a vector instead?

For example if I type:

:t Vect

I get Vect : Nat -> Type -> Type which makes absolute sense, if I type

:t Vect 2

I get Vect : Type -> Type which makes again absolute sense. But I try now:

:t Vect 2 [1,2]

and get an error 

Can't disambiguate since no name has a suitable type: 
         Prelude.List.::, Prelude.Stream.::, Data.Vect.::

I was hoping to see instead [1,2] : Vect 2 Int instead. What I am doing wrong? I also have issues when using the function the when trying to interpret a list as vector.

Any suggestion?

Solution

  • the : (a : Type) -> a -> a takes a type and a value of that type and returns that value. So if the target type cannot be inferred from context, like in the REPL, you can use the (Vect 2 Int) [1,2] to specify what you mean with [1,2].

    (Vect 2 [1,2] tries to use the List, Stream or Vect [1,2] as the argument in Vect 2 : Type -> Type. But unlike e.g. Int, the list [1,2] is not a Type, so that throws you that error.)