Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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?

like image 440
Cactus Avatar asked Oct 02 '17 15:10

Cactus


1 Answers

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

like image 92
Boyd Stephen Smith Jr. Avatar answered Dec 11 '22 07:12

Boyd Stephen Smith Jr.