Idris-dev icon indicating copy to clipboard operation
Idris-dev copied to clipboard

Update tutorial's "using" example to avoid errors

Open acarrico opened this issue 6 years ago • 4 comments

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?

acarrico avatar Apr 17 '19 15:04 acarrico

Hmmm, doesn't that change the meaning of it, even if the end result is the same?

melted avatar May 30 '19 13:05 melted

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.

acarrico avatar Jun 02 '19 17:06 acarrico

A good action point from this issue would be to have some documentation contributed to the language reference, and beginner tutorial, to clarify matters.

jfdm avatar Jun 03 '19 08:06 jfdm

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?

acarrico avatar Jun 04 '19 18:06 acarrico