Whiley / WhileyCompiler

The Whiley Compiler (WyC)
http://whiley.org
Apache License 2.0
217 stars 36 forks source link

Lambda Expressions #1049

Closed DavePearce closed 2 years ago

DavePearce commented 3 years ago

There is a flaw in the way lambda "declarations" are typed. Specifically, the following example illustrates:

type State is { int status }
type handler is method(State)|method(int)

type DomObject is &{
  method addEventListener(int[], handler),
  ...
}

method empty():
    skip

method register(DomObject obj):
    // Register identity
    obj->addEventListener("click",&(State s -> empty()))

The problem is that the expression &(State s -> empty()) must have type handler, but the Decl.Lambda instance generated has type method(State).

DavePearce commented 3 years ago

Can we somehow just use LambdaAccess for both, whereby in this case it refers to a Decl.Lambda rather than e.g. a Decl.Function. I think this can work, though the whole issue with the Binding is problematic.

DavePearce commented 2 years ago

Fixed by #1132