CODEWITHSUNDEEP
idrisdependent-type
brainrape
brainrape

Reputation: 346

How to write an Idris function that accepts a Vect of length less than 3

Idris 1.2.0. I tried to automatically find a proof that the length of the vector is less than 3.

f : {n : Nat} -> {auto prf: n < 3 = True} -> Vect n a -> ()
f v = ()

f' : {n : Nat} -> {auto prf: isJust (natToFin n 3) = True} -> Vect n a -> ()
f' v = ()

Both of these typecheck, and work with f {n=2} [1, 2} and even f (the (Vect 2 Nat) [1, 2]) but when I call it like f [1, 2], I get

When checking argument x to constructor Data.Vect.:::
    No such variable len

I also tried another way:

g : {x : Fin 3} -> Vect (finToNat x) a -> ()
g v = ()

This works with g {x=2} [1, 2] too, but again fails with g [1, 2]

When checking an application of function Main.g:
    Type mismatch between
            Vect 2 Integer (Type of [1, 2])
    and
            Vect (finToNat x) Integer (Expected type)

    Specifically:
            Type mismatch between
                    2
            and
                    finToNat x

Ok, I guess these two expressions don't reduce to the same canonical form when x is unknown.

I don't understand the first error. I suspect it has something to do with [] syntax overloading. What am I doing wrong?

Upvotes: 2

Views: 625

Answers (2)

brainrape
brainrape

Reputation: 346

Thanks to gallais for the insight. Here's a complete example:

-- idris -p contrib

import Data.BoundedList
import Data.Vect

-- a function that takes a list of at most 3 elements
f : BoundedList 3 a -> ()
f xs = ()

-- a shorter vector
v : Vect 2 Int
v = [1, 2]

-- convert the vector to a bounded list and weaken the bound
bounded : BoundedList 3 Int
bounded = weaken $ fromList $ toList v

-- call the function
answer : ()
answer = f bounded

Upvotes: 1

gallais
gallais

Reputation: 12103

Idris does not try to inverse the (injective) function finToNat to guess the value for x when trying to solve the unification problem finToNat x = 2. So it simply gets stuck.

On a more general level rather than pushing computations in the type or proof search in the implicit arguments, I would represent bounded vectors by either:

record BoundedVec (n : Nat) (a : Type) where
  size : Nat
  less : LTE size n
  vect : Vect size a

Or, following Agda's standard library

data BoundedVec : (n : Nat) -> (a : Type) -> Type where
  Nil  : BoundedVec n a
  Cons : a -> BoundedVec n a -> BoundedVec (S n) a

Upvotes: 3

Related Questions