Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update tutorial's "using" example to avoid errors #4688

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

acarrico
Copy link

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?

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?
@melted
Copy link
Contributor

melted commented May 30, 2019

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

@acarrico
Copy link
Author

acarrico commented Jun 2, 2019

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.

@jfdm
Copy link
Contributor

jfdm commented Jun 3, 2019

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

@acarrico
Copy link
Author

acarrico commented Jun 4, 2019

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants