Bug #13

Variables aren't consumed properly in peeks

Added by Mike Burrell about 2 years ago. Updated about 2 years ago.

Status:New Start:01/30/2010
Priority:Look at it when you have time Due date:
Assigned to:Mike Burrell % Done:

70%
Category:Implementation
Target version:-

Description

We should be doing a context intersection at the end of each peek but we aren't. Consider the following example:

f = | x, y.peek peek x of { Zero.y; Succ(_).Zero } of {
    Zero.y;
    Succ(_).y };

Clearly y should have been consumed in the inner peek and thus this should lead to a typing error. Because y isn't used in the last branch that's typed, however, it's not considered to be consumed.

History

Updated by Mike Burrell about 2 years ago

Actually the example should be:

f = x | y.case case x of { Zero.y; Succ(_).Zero } of {
    Zero.y;
    Succ(_).y };

Updated by Mike Burrell about 2 years ago

  • Status changed from New to Resolved

Okay the case example can't work either since y can't be used in an o context. I'll close this until I can find an example that shows it off.

Updated by Mike Burrell about 2 years ago

  • Status changed from Resolved to New

Better example:

f = | x, y.(x, y);
g = | x, y.f(peek x of { Zero.y; Succ(_).Zero }, y);

Currently this types, though it shouldn't.

Updated by Mike Burrell about 2 years ago

  • Priority changed from Work on it right now to Look at it when you have time
  • % Done changed from 0 to 70

Fix for inductive types is done and will be in the next revision. Coinductive will wait a wee bit....

Also available in: Atom PDF