Idris-dev
Idris-dev copied to clipboard
Update tutorial's "using" example to avoid errors
As a beginner, I just interpolated between the working example, and the broken example with "using". This fix renders the example less perfect for introducing "using" notation, but at least it goes through without errors in my installation (Idris 1.3.0). Is there a better fix which keeps {x:a} up in the "using" clause?
Hmmm, doesn't that change the meaning of it, even if the end result is the same?
Right. I took another look at this (with a tiny bit more experience learning Idris), and I think the problem is with my understanding of the lexical scoping rules in Idris. Renaming the identifiers resolves the specific issue:
data IsElem1 : a -> Vect n a -> Type where
Here1 : {x:a} -> {xs:Vect n a } -> IsElem1 x (x :: xs)
There1 : {x,y:a} -> {xs:Vect n a} -> IsElem1 x xs -> IsElem1 x (y :: xs)
testVec : Vect 4 Int
testVec = 3 :: 4 :: 5 :: 6 :: Nil
using (x2:a, y2:a, xs2:Vect n a)
data IsElem2 : a -> Vect n a -> Type where
Here2 : IsElem2 x2 (x2 :: xs2)
There2 : IsElem2 x2 xs2 -> IsElem2 x2 (y2 :: xs2)
inVect2 : IsElem2 5 Prims.testVec
inVect2 = There2 (There2 Here2)
As would just removing a binding of x elsewhere in the module. It seems like Here1 : {x:a} binds a new x but using (x: doesn't. As a beginner, I assumed that using introduced a new scope, but apparently it does not. In the tutorial, the offending binding is at the top of the section:
module Prims
x : Int
x = 42
I also ran into an issue with the TDD book, which also appeared to come down to scoping. It had been noted on the mailing list in the past, so I revived the thread. I don't think the OP got a proper answer, and unfortunately I didn't get a reply. See:
Re: [Idris] Re: Can't match on Main.addToStore, addToData
Thanks for the note. I can withdraw this request, but if people are running into scoping problems on these two examples (here, in the tutorial and Main.addToStore, addToData in TDD book), then it would be nice to clarify things someplace in the beginner docs.
A good action point from this issue would be to have some documentation contributed to the language reference, and beginner tutorial, to clarify matters.
I'm trying to check the docs, but I can't find any reference documentation for the "using" keyword. Did I miss it? Best I could find is syntax reference:
Using ::= 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock ;
I had assumed that identifiers in the UsingDeclList are local to the Decl*. If so, is this a compiler bug? If not, why is there a block at all?