Potential Bug?

[michaelto20]

When testing the REPL I noticed that the order of assigning variables is quite strict. This may be a design decision or it could be a bug, let me know where you want to go with this.

Try this in the REPL:

let p = fun m (triv triv)
let m = (succ unit)
:u p

Your output is fun m (triv triv) whereas I had expected it to use the value of m and display fun (succ unit) (triv triv) . It will display that if you switch the order of commands to this:

let m = (succ unit)
let p = fun m (triv triv)
:u p

Again this may be expected behavior but it just surprised me so I wanted to bring it up and get your thoughts on it.

[heades]

This is a feature, right? You shouldn't use state-based variables that have not been declared yet.

Garbage in, garbage out.

Now, we could get around this, but you will have to implement it.

[heades]

Something is not right with you example.

[heades]

Functions take in a bound variable, and the body. So fun m t is not a function. Here fun turns into a variable. Just so that you know.

[heades]

See even GHCI doesn't allow this:

➜ constructive git:(master) ✗ ghci GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help Prelude> let p = f m 1 1

:1:9: error: Variable not in scope: f :: t0 -> Integer -> Integer -> t :1:11: error: Variable not in scope: m Prelude>

[michaelto20]

Yes the example was just something to show how the variable was only being evaluated in certain circumstances.

On Sat, Oct 22, 2016 at 1:08 PM, Harley D. Eades III < notifications@github.com> wrote:

Functions take in a bound variable, and the body. So fun m t is not a function. Here fun turns into a variable. Just so that you know.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/heades/gradual-typing/issues/14#issuecomment-255540728, or mute the thread https://github.com/notifications/unsubscribe-auth/AEqTwM08rw9LvgqJbI-rmbWxv-KuTvDnks5q2kL6gaJpZM4Kd6Wd .

[michaelto20]

So should we expand TypeChecker to determine if variables are being declared before they are used?

On Sat, Oct 22, 2016 at 1:09 PM, Harley D. Eades III < notifications@github.com> wrote:

See even GHCI doesn't allow this:

➜ constructive git:(master) ✗ ghci GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help Prelude> let p = f m 1 1

:1:9: error: Variable not in scope: f :: t0 -> Integer -> Integer -> t

:1:11: error: Variable not in scope: m Prelude>

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/heades/gradual-typing/issues/14#issuecomment-255540794, or mute the thread https://github.com/notifications/unsubscribe-auth/AEqTwOkG6rE7HRM9_CmA8jssUlURHWaWks5q2kM9gaJpZM4Kd6Wd .

[heades]

No, this has nothing to do with the type checker. This has everything to do with the repl.

We could try and catch this and throw a proper error.

[heades]

This should be pretty easy to catch. After parsing in the term, check to see if all free variables have been declared in the definition queue. If not, then throw an error, and if so, then continue doing what ever command we got.

[michaelto20]

I got stuck working on dynamically loading a file in the repl so I started to work on this feature. I've looked through the code and have an idea how I would implement the above feature, i.e. checking to make sure all free variables have been declared in the definition queue.

Take the example: let p = m (split<Nat> n) and assume m is some function and n is of type Nat where both m and n are defined earlier in the definition queue. I'm struggling to come up with a good method to find the variables inside the definition of p whose values need to be looked up in the definition queue. Once I have them, looking them up should be simple. Here are the steps for one idea I had:

1. Pass the definition of p to a function that tokenizes it based on white space, parentheses, and <.
2. Then make sure each token is either a Type, a Term, or in the definition queue.
3. If it is not, then it is an open term that isn't previously defined

Now that I've written this out it seems more doable then I first realized. I'll see if I can put it together by our Monday meeting.

[heades]

I think you are making this harder than it is.

Why not just unfold the definition of p, and then grab whatever you need?

[heades]

In addition, I would much rather you work on the examples we decided on before Monday instead of catching this error. I just don't think this is very pressing.

[heades]

When using the REPL just make sure to declare your variables first.

[heades]

Thinking about this more, it is pretty easy.

Unfold the definitions in p, and then if a free variable remains, then throw an undefined variable error. So no additional parsing is needed.