undefined inhabits Void #2557

Closed
minad opened this Issue Jan 11, 2017 · 26 comments

Projects

None yet

3 participants

@minad
minad commented Jan 11, 2017 edited
undefined :: forall a. a
undefined = (\_ -> undefined) "foo"

void :: Void
void = undefined

Is this a problem with the scoping?

@paf31 paf31 added the wontfix label Jan 11, 2017
@garyb
Member
garyb commented Jan 11, 2017

You can use that undefined anywhere, since forall a. a will unify with everything.

@paf31
Member
paf31 commented Jan 11, 2017

Thanks for the report, but this is a known limitation of the way we handle scoping. We do disallow things like

undefined = undefined

since that would lead to an actual undefined (in the JS sense) at runtime.

We require self-recursion to be guarded by a function for this reason. Unfortunately, that means your undefined passes the checker, even though it's obviously not a good definition.

@minad
minad commented Jan 11, 2017 edited

well, but undefined returns javascript "undefined". This is different from direct recursion "undefined = undefined"

@paf31 paf31 closed this Jan 11, 2017
@minad
minad commented Jan 11, 2017

@paf31 I would still argue that the scoping should be fixed. Is there some known limitation preventing that?

@paf31
Member
paf31 commented Jan 11, 2017

How would you fix it?

@garyb
Member
garyb commented Jan 11, 2017 edited

Could we check when we have a lambda that makes a recursive reference to see if the lambda is evaluated as part of its definition?

@paf31
Member
paf31 commented Jan 11, 2017

I'd rather not make the check more complicated. I don't think it's possible to solve this in general, and what we have now seems like a decent approximation.

@minad
minad commented Jan 11, 2017

@paf31 You could allow only lambdas in recursive bindings. But then you lose many cases which work right now, e.g., recursive monads.

I haven't found a better solution yet. I was toying around with my own small strict lambda interpreter and had the same problem.

@garyb
Member
garyb commented Jan 11, 2017

I dunno, it seems like a rather big flaw if the typechecker will let runtime-undefined definitions through!

It is tricky though, as yeah, I've already thought of a way that the check I described is not good enough...

@minad
minad commented Jan 11, 2017

@garyb It is a big flaw.

@paf31
Member
paf31 commented Jan 11, 2017

It is a big flaw in any language with general recursion.

@minad
minad commented Jan 11, 2017 edited

@paf31 Yes, but I would expect an endless loop, but not undefined.

This is what I meant concerning recursive bindings:

data Expr
  = LetAtom Name Atom Expr
  | LetLambda [(Name, Lambda)] Expr --- Recursive lambdas
  | ...
@paf31
Member
paf31 commented Jan 11, 2017

How is an endless loop more useful?

@garyb
Member
garyb commented Jan 11, 2017

It doesn't really help, requiring recursion to be explicit, as the problem still exists though right?

@minad
minad commented Jan 11, 2017 edited

I would argue that the only possible bad behaviour in a non-total language should be an endless loop. But this is just my opinion.

@garyb If recursion is explicity allowed in the core language only for functions then this problem would not occur.

@garyb
Member
garyb commented Jan 11, 2017

@paf31 it's a little easier to figure out what's going on if the program stalls while evaluating definitions vs an undefined popping up somewhere later on.

@minad
minad commented Jan 11, 2017

@paf31 I think my opinion is the commonly accepted one. For example in the dependent haskell proposal by Eisenberg, equality proofs must be evaluated to keep the type system sound. This means that fake proofs would loop. But in this case here, we get "undefined", which means the type system is not sound in the sense of Haskell.

@garyb
Member
garyb commented Jan 11, 2017

@minad I'm not sure I follow... but nevermind, as I don't think we're likely to change the language that fundamentally at this point given general recursion usage is already very common.

@paf31
Member
paf31 commented Jan 11, 2017

I'm saying this is impossible because it requires us to solve the halting problem. What's the solution?

@minad
minad commented Jan 11, 2017 edited

@paf31 How is this equivalent to the halting problem? I am just asking to detect the invalid scoping as in this case, not checking totality in general.

@paf31
Member
paf31 commented Jan 11, 2017

I'd also like to point out that Elm does the exact same thing. I say Elm because it's the one strict language with an online editor that I know of. I can check others.

@minad
minad commented Jan 11, 2017

Again, what would solve the issue is if one allows only lambdas in the recursive bindings (as in the LetLambda above), since then the bound functions are well defined in javascript.

var f1, f2;
f1 = function() { calls f2 }
f2 = function() { calls f1 }

What you allow right now is something like this:

var x;
x = (function() { use x here while it is not yet defined })(...);
@paf31
Member
paf31 commented Jan 11, 2017

That disallows too many useful things though.

@minad
minad commented Jan 11, 2017

@paf31 Yes, indeed 😞 So the only acceptable solution is modifying the checker. But nevermind, I was just playing around - I don't think fixing this issue is very important, since this problem probably wouldn't occur in normal use. Thx for the quick responses!

@paf31
Member
paf31 commented Jan 11, 2017

Sure, and sorry the answer is so disappointing. I agree it's not ideal, but I've thought quite a bit about this in the past, and this is the best approximation I could come up with, with decent trade-offs.

@minad
minad commented Jan 11, 2017

Hmm, I think it could be solved by wrapping in functions (like introducing laziness).

Currently ps generates:

var $$undefined = (function (v) {
    return $$undefined;
})("foo");

Replace this with:

var $$undefined2 = function() { (function (v) {
    return $$undefined2();
})("foo") };
var $$undefined = $$undefined2();

This would also work for mutually recursive bindings. But I don't really like this transformation since it would recompute things when it isn't really necessary.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment