CODEWITHSUNDEEP
type-inferenceagdaidris
Cactus
Cactus

Reputation: 27626

Can Idris infer indices in types of top-level constants?

For example, Agda allows me to write this:

open import Data.Vec
open import Data.Nat

myVec : Vec ℕ _
myVec = 0 ∷ 1 ∷ 2 ∷ 3 ∷ []

and myVec will have type Vec ℕ 4 as expected.

But if I try the same in Idris:

import Data.Vect

myVec : Vect _ Nat
myVec = [0, 1, 2, 3]

I get an error message from the typechecker:

 When checking right hand side of myVec with expected type
         Vect len Nat

 Type mismatch between
         Vect 4 Nat (Type of [0, 1, 2, 3])
 and
         Vect len Nat (Expected type)

 Specifically:
         Type mismatch between
                 4
         and
                 len

Is there a way to define myVec in Idris without manually specifying the index of the Vect?

Upvotes: 8

Views: 221

Answers (1)

Boyd Stephen Smith Jr.
Boyd Stephen Smith Jr.

Reputation: 3202

Per the comments, top-level holes in Idris was universally quantified, instead of being filled via term inference.

I believe (but, ultimately someone from the development team would have to confirm / deny) that this was done partially to encourage explicit types, and thus type-directed development, and partially to have a nice syntax for don't-care values in interface implementations like:

Uninhabited v => Uninhabited (_, v) where
    uninhabited (_, void) = uninhabited void

This don't-care use of the underscore is adopted from it's use in patterns, rather than it's use in expressions.

For something like this (it's not exactly what you want, but it is robust against changes to the constant), you can use an explicit existential:

fst : DPair t _ -> t
fst (x ** _) = x

snd : (s : DPair _ p) -> p (fst s)
snd (_ ** prf) = prf

myVecEx : (n ** Vect n Nat)
myVecEx = (_ ** [0, 1, 2, 3])

myVec : Vect (fst myVecEx) Nat
myVec = snd myVecEx

fst and snd might be in the standard library under different names, but I didn't find then in a quick search.

EDIT: An upvote recently drew this answer to my attention again. If you are using Idris 2, I believe you can use a ? instead of a _ at the top level to have it filled in my idris. _ at the top level, is an erased, implicit, unnamed parameter, still. https://idris2.readthedocs.io/en/latest/implementation/overview.html#additional-type-inference

Upvotes: 2

Related Questions