Idris: Writing an initial segments function for vectors with length as a Fin rather than a Nat

Question

I'm trying to write an initial segments function for vectors, which stores the length of the vector as a Fin rather than a Nat, as follows:

vectorsInits : Vect n t -> Vect n (p ** Vect (finToNat p) t)
vectorsInits Nil = Nil
vectorsInits (x::xs) = ((FS FZ) ** (x::Nil)) :: map (\(p ** ys) => ((FS p) ** x::ys)) (vectorsInits xs)

This definitions doesn't work however as i get the following type error:

When checking right hand side of vectorsInits with expected type

    Vect (S len) (p : Fin n ** Vect (finToNat p) t)

When checking argument pf to constructor Builtins.MkDPair:

    Type mismatch between

            Vect 1 t (Type of [x])

    and

            Vect (finToNat (FS FZ)) t (Expected type)

    Specifically:

            Type mismatch between

                    1

            and

                    finToNat (FS FZ)

But the definition of finToNat is clear that finToNat (FS FZ) would equal 1,. even if I write the following function to try and get idris to realise they're equal, I get an error:

intproof : Vect 1 t -> Vect (finToNat (FS FZ)) t 
intproof x = x
...
vectorsInits (x::xs) = ((FS FZ) ** intproof (x::Nil)) :: map (\(p ** ys) => ((FS p) ** x::ys)) (vectorsInits xs)

gives me the error:

When checking right hand side of vectorsInits with expected type
        Vect (S len) (p : Fin n ** Vect (finToNat p) t)
When checking argument pf to constructor Builtins.MkDPair:
    Type mismatch between
            Vect (finToNat (FS FZ)) t (Type of intproof [x])
    and
            (\p => Vect (finToNat p) t) (FS FZ) (Expected type)
    Specifically:
            Type mismatch between
                    1
            and
                    finToNat (FS FZ)

even writing:

intproof : Vect 1 t -> (\p => Vect (finToNat p) t) (FS FZ)
intproof x = x

gets an identical error as above

I've got %default total and I'm importing Data.Vect at the beginning of my file.

Is there any way to force Idris to recognise that finToNat (FS FZ) is equal to 1 (that is, S Z))?

Thanks

It's not possible to write a function with the type you've provided, because it would lead to a contradiction -- see this proof. — Anton Trunov

HTNW HTNW · Accepted Answer · 2018-04-30T11:55:21

You've got an issue:

vectorsInits : Vect n t -> Vect n (p ** Vect (finToNat p) t)

What is the type of p? You haven't given it, and it actually ends up being

vectorsInits : Vect n t -> Vect n (p : Fin m ** Vect (finToNat p) t)

That is, the type of the Fins running beside your data, is totally unrelated to the input. That's not right. It should (at least) be

vectorsInits : Vect n t -> Vect n (p : Fin n ** Vect (finToNat p) t)

However, that's not quite right either. What should happen is that the Fins count up from FZ to last as you go down the output, but your current implementation does not do that. If you change it to do so, you'll notice that each output vector ends up having a length one greater than the index:

vectorsInits : Vect n t -> Vect n (p : Fin n ** Vect (S (finToNat p)) t)
vectorsInits [] = []
vectorsInits (x :: xs) = (FZ ** [x]) :: map (\(idx ** ixs) => (FS idx ** x :: ixs)) (vectorsInits xs)

Or, you can affix a [] to the start of the output (after all, [] is a prefix of every list), and thus get a version which obeys the identity index n (vectorInits xs) = take n xs (some mangling omitted):

vectorsInits : Vect n t -> Vect (S n) (p : Fin (S n) ** Vect (finToNat p) t) 
vectorsInits [] = [(FZ ** [])] 
vectorsInits (x :: xs) = (FZ ** []) :: map (\(idx ** ixs) => (FS idx ** x :: ixs)) (vectorsInits xs)

Idris: Writing an initial segments function for vectors with length as a Fin rather than a Nat

1 Answers