Idris newbie question...

[Emanuele Colombo]

Hi all,

I'm a newcomer in the Idris world, I'm just trying to understand how all these new things work, reading the "Type Driven Development with Idris" book and experimenting with some code.

I'm now facing a problem that I can't understand. Here is an example that currently doesn't type-check:

import Data.Vect

data Rankings: Nat -> Type where

   MkRankings: (count : Nat) -> Vect count String -> Rankings count

data Position: (rankings: Rankings (S maxIndex)) -> Type where

   MkPosition: (pos: Fin (S maxIndex)) -> Position rankings

rankingsNames: Rankings count -> Vect count String

rankingsNames (MkRankings count names) = names

nameAtPosition: {rankings: Rankings (S maxIndex)} -> Position rankings -> String

nameAtPosition {rankings} (MkPosition pos) = let allNames = rankingsNames rankings in

                                                index pos allNames

Please, don't stop on the usefulness of this code, it is just an example I've extracted from a more complex code I'm working.

If you try to make it compile, you can see that the last line doesn't work because of some mismatch on the maxIndex value. I can't understand why it doesn't work since a Position instance is related to the "maxIndex" value provided by the Rankings instance that defines the type itself (Position rankings).

What should I do/change in order to make this code compile?

Sorry if I didn't explained my problem quite well, I'm new to this world and I don't own very much the correct terminology.

Thank you very much!

Emanuele

[David Thrane Christiansen]

Hello Emanuele,

The summary of the issue is that Position doesn't do quite what you think it should.

In the interest of helping you see how you could have solved this, I'll be a bit verbose and walk you through how I figured it out.

First, looking at the error message:

     When checking an application of function Data.Vect.index:
             Type mismatch between
                     Vect (S maxIndex1) String (Type of allNames)
             and
                     Vect (S maxIndex) String (Expected type)
            
             Specifically:
                     Type mismatch between
                             maxIndex1
                     and
                             maxIndex

I saw that there were two different variables named maxIndex, and that Idris had helpfully renamed one of them so they could be told apart. The next step was to replace the right hand side with a hole:

nameAtPosition: {rankings: Rankings (S maxIndex)} -> Position rankings -> String

nameAtPosition (MkPosition pos) = ?nameAtPosition_rhs_1

The context was then:

Holes

- + Main.nameAtPosition_rhs_1 [E]
 `--                   maxIndex : Nat
                       rankings : Rankings (S maxIndex)
                      maxIndex1 : Nat
                            pos : Fin (S maxIndex1)
     ---------------------------------------------------
      Main.nameAtPosition_rhs_1 : String

Note that there are indeed two separate implicit arguments named maxIndex. The one related to pos came after everything having to do with rankings, so that means that something about the types of those two arguments failed to related things the way it should have.

The next step was to look at the Position datatype to see where the multiple maxIndex arguments came from. I right-clicked it in Emacs and picked "show definition". This pops up the following window:

data Position : Rankings (S maxIndex) -> Type where
  MkPosition : Fin (S maxIndex) -> Position rankings

Looks good so far. The next step was to right-click both the type constructor's type and the constructor's type, and pick "show core", so the window shows:

data Position : (maxIndex : Prelude.Nat.Nat) →
                (rankings : Main.Rankings (Prelude.Nat.S maxIndex)) → Type where
  MkPosition : ({maxIndex_507} : Prelude.Nat.Nat) →
               (rankings : Main.Rankings (Prelude.Nat.S {maxIndex_507})) →
               (maxIndex : Prelude.Nat.Nat) →
               (pos : Data.Fin.Fin (Prelude.Nat.S maxIndex)) →
               Main.Position {maxIndex_507} rankings

Now we see the issue: the constructor has two separate maxIndex arguments. One of them is the one referred to by pos, and the other is the one referred to by rankings. The type constructor refers only to the first one, while the one on pos is independent.

This can be fixed by pointing the type constructor at the same maxIndex:

data Position: (rankings: Rankings (S maxIndex)) -> Type where

    MkPosition: (pos: Fin (S maxIndex)) -> Position {maxIndex} rankings

With this change, the original code goes through:

nameAtPosition: {rankings: Rankings (S maxIndex)} -> Position rankings -> String
nameAtPosition {rankings} (MkPosition pos) =
  let allNames = rankingsNames rankings in
  index pos allNames

A good rule of thumb is that when an equality is important, it should be mentioned in the type constructor.

BTW: your explanation was great. No need to worry about that.

David

[Andrej Tokarčík]

Hi Emanuele,

As an alternative to David's suggestion you could consider
"flattening" the Position datatype by turning it into a type function:

Position : Rankings (S maxIndex) -> Type

Position {maxIndex} _ = Fin (S maxIndex)

The nameAtPosition function would then become:

nameAtPosition : {rankings : Rankings (S maxIndex)} -> Position
rankings -> String

nameAtPosition {rankings} pos = let allNames = rankingsNames rankings in
index pos allNames

Kind regards,
Andrej

[Emanuele Colombo]

Thank you both David and Andrej for your replies!

David, after your explanation the situation has more sense. I wasn't aware of the "show core" option since I used the atom and the visual studio code plugins that appear to don't have this feature; I've never used EMACS...

Andrej, thank you for your addition, I started using both data type declarations and type functions, but in order to understand better what I'm doing and create less confusion in my mind ;-) I'm trying to be a little more "verbose" and use data type declarations as much as possible. Anyway, it is an useful alternative I'll try to work with, thanks.

Generally speaking about Idris, I'm a bit worried about the proofs thing, I think I'll be back here soon with some questions when I'll crash into it :-)

Many thanks!

Emanuele