Lambda application in `typeof()` not allowed

[gbluma]

I found a bug when testing nested typeof expressions. I think the issue is part of the recursive type analysis stuff in flx_lookup.ml, but I can't make heads or tails of it yet.

example.flx

syntax PIPES {

  satom := sexpr "`map`" satom =>#
    ((map    (fun (_:typeof(head(?1))) => ?3) ?1));

  satom := sexpr "`filter`" satom =>#
    ((filter (fun (_:typeof(head(?1))) => ?3) ?1));

  satom := sexpr "`iter`" satom =>#
    ((iter   ?3 ?1));

};
open syntax PIPES;

list(1,2,3)
  `map` (_ + 5)    // take this line out and it works
  `filter` (_ > 2)    // take this line out and it works
  `iter` (proc (x:int) { println x;})
;

// if you keep `map` and `filter` it fails.

Error:

FELIX COMPILER ERROR
In /home/ubuntu/grammartest2.flx: line 5, cols 15 to 44
4:   satom := sexpr "`map`" satom =># 
5:     ((map    (fun (_:typeof(head(?1))) => ?3) ?1));
                 ******************************
6: 

[bind_expression] Unexpected lambda or object when binding expression (should have been lifted out)(inline function(lambda) (val _: typeof((head (list (1, 2, 3))))) = {
  return _+5;
})

I find it odd that it complains about this. If it were able to decide the types "bottom-up" it wouldn't have any trouble figuring it out. Also,

[refi64]

Also,

Come on, you're leaving me hanging here! :)

[gbluma]

Haha.. Also! That's how I like to end ALL MY SENTENCES.

... Also, it's not complaining about the recursion problem, just that it fails to "lift" the expression, whatever that means. There are a few gaps the the compiler phases that I'd like to work on, and this could be another case of one.

(The other I ran into lately is a missing EXPR_ifdo clause somewhere. I was manually injecting expressions and found out it couldn't codegen.)

[skaller]

On 3 Jul 2016, at 12:28, Ryan Gonzalez notifications@github.com wrote:

Also,

Come on, you're leaving me hanging here! :)

Huh? Is this new or did I forget it?

— john skaller skaller@users.sourceforge.net http://felix-lang.org

[gbluma]

It's new. Just created it.

Took a spin trying to fix it, but couldn't figure it out.

Garrett

[skaller]

Ok, so the problem is non trivial.

Lambda lifting means, if you have a lambda in an expression, it is replaced by a name, and then the name is defined as a function in the same scope.

So if you write:

var f = (fun (x:int)=>x) 42;

it is replaced by

fun synth (x:int)=>x;
var f = synth 42;

where “synth” is some unique synthesised name.

The code that does lambda litfing is in

src/compiler/flx_desugar/flx_desugar_expr.ml

named “rex”. It is driven by the function in

src/compiler/flx_desugar/flx_desugar.ml

named “rst”. For example you get stuff like:

| STMT_fun_return (sr,e) -> let d,x = rex e in d @ [Exe (sr,EXE_fun_return x)]

where rex e splits e up into x (without lambdas) and into a list of definitions d which define the lambdas.

The PROBLEM is that given an arbitrary typeof() expression .. there is nowhere obvious to “lift” the lambdas to.

Actually they CAN be lifted, to the same place: the parent of the type expression.

This case is easy:

| STMT_type_alias (sr,name,vs,typ) -> [Dcl (sr,name,None,access,vs,DCL_type_alias (typ))]

This is a typedef statement. So any nested lambdas in “typ” can be lifted. But in general this isn’t enough.

More generally we need a “desugar_type” function, which doesn’t exist. Its trivial to write, because the only thing it does is desugar typeofs. The problem is integrating it into the rest of the desugaring process: EVERY statement or expression that contains a type code will have to be modified to extract the extra definitions.

— john skaller skaller@users.sourceforge.net http://felix-lang.org

[skaller]

So here are fix instructions:

(a) create a minimal test case, make sure it fails, use a typedef ONLY.

(b) add the lambda lifting function to desugar code, but DON'T CALL IT Just get it to compile

(c) Repair the STMT_type_alias case ONLY using the function.

(d) Test your test case.

(e) run all the tests (make test)

(f) rebuild Felix from the bootstrap

(g) if it is OK then commit change

(h) Now apply the change to another STMT_* This will have to include applying it to expressions. Again, make a test case and just do the mods for that test case. Make the test case more comprehensive and add more mods.

The secret is to do the "Extreme Programming" crap. Test case first. Run. MAKE SURE IT FAILS. Change the code. Now it should pass. Other tests should CONTINUE TO FAIL.

When you have a clear idea how the modification transformation pattern looks, do the lot.

I call this transformational programming. Its a scientific method. You must be able to predict that a change will make something work (that's the thesis) AND that other things will continue to fail: thats the CONTROL. If your prediction does not match experiment, STOP. Ask why.

USEFUL UTILITY: src/compiler/flx_core/flx_maps.ml You will probably HAVE to use this:

let full_map_expr fi ft fe (e:expr_t):expr_t = match e with ...

and you will need to understand how to do open recursion. Since this is a map, you will need a trick function that emits the extra definitions via a list ref which is instantiated at the statement handling level, where the extra definitions can be tacked onto the processed statement (but maybe in some cases the list can be inside the expression handling rex instead, not sure).

[skaller]

Just a BTW: lambda lifting may not be necessary, its not clear. C++11 has lambdas. Also, the lifting could be done later. In fact the need to lift is an EXTREME PAIN because later in processing the compiler needs to add functions to the code, and it has to manually synthesise a new function in the symbol table and call it every time. That is non-trivial because one has to add all the variables including parameter and all locals as well, and any other children, and also the really hard bit, making sure eveything has the right parent and type variables.

However it solves the problem theoreticians refer to as "reducing under the lambda" which means, doing reductions to terms inside a lambda binder. Difficult and tricky in lambda calculus at least because you need to hit a lambda to do alpha conversion. With lambda lifting the problem goes away because the function now has a name in the environment, so it's just a constant.

[gbluma]

I'll stew on this for a while and revisit it tomorrow. I don't think lifting is necessary for this situation. We don't need to carry around a lifted closure (something dynamic), we just need a static type.

Like you say John, we should be able to write a desugar_type function that can shortcut the process.

desugar_type( head(list(1,2,3)) ) 

could just deduce the type from

head : [A] list(A) -> A

which is concretely

list(int) -> int

and could just yield int by following the types. Application is just stepping forward in the type signature, after all.

What I'm cautious about of is the undiagnosed cases--i.e. conditionals and patterns, etc. Conceivably, they could be converted to sum types, but it could explode in complexity too.

Anyway, back on topic: here's a minimal example that can trigger this error.

typedef foo_t = typeof((fun (x:int) => x) 3);
var z :foo_t = 3;

[gbluma]

Ahh.. Actually I'm seeing why the lifting is there (polymorphism). My hypothesis (scientific method) could be wrong. :) Dang.

[skaller]

Lifting is there for a simple reason, its not polymorphism. The reason is that it allows compiler code that processes expression terms .. to process expression terms without a need to process embedded statements. Instead, by lifting the lambda out we have created a level of indirection, so that various passes of the compiler can treat the lambda as an entry in the symbol table.

This means, for example, the code that calculates the return type of a function without fully binding the function, can be applied to the lambda because it is a symbol table entry. Then there is a "hook" where we can cache the function type. Routines that analyse all functions, find the lambdas too.

Note that Felix has an expression term EXPR_index which allows you to avoid lookup issues, just make the function index so-and-so and call it with EXPR_index: its "pre-bound"; that is, bound by construction not by name.

Felix creates such private functions left right and centre. block/end is an example, its a 1->0 function (procedure) which is called like { .. }(). Pattern matching creates multiple function layers to manage context. Typically generated functions like this are marked "inline" and are inlined away.

At the back end, in C++89 we have no choice than use functions because there are no lambdas. In C++11 I would not trust C++11 lambdas to do the job except in limited cases.

So roughly the idea is to turn the input AST into unbound abstract machine code, and then bind it, preserving the structure but just replacing string names with integer indexes into the symbol table. Desugaring has the job of splitting code into two kinds: declarations/definitions, and executable code (Dcl and Exe terms). Dcls can contain Exes and other Dcls, so now we have a tree which clearly marks what needs to go into the symbol table. So

var x = 1;

is split into

[Dcl (x,var,typeof(1)); Exe (assign (x,1))]

and then we split the list into pure Dcls and pure Exes.

Anyhow the issue with typeof() is that it has to process ANY expression, and the only way to calculate the bound type of an expression is to actually bind it. It's not just lambdas. The expression can have overloading and anything else so it has to be bound by the same routine that would bind it were it in executable code. We just throw out the bound expression part and keep the type.

[gbluma]

For purposes of tracking the progress on this ticket, the following works as of yesterday.

typedef foo_t = typeof((fun (x:int) => x) 3);
var z :foo_t = 3;

More cases to follow.

[gbluma]

New changes make the following case work:

fun foo (x:typeof((fun (x:int) => x) 3)) => x;
println$ foo(3);

[gbluma]

I just wanted to put an update on this issue. I'm currently looking for more failing test cases (ones where typeof is used in the type). I have a hunch that records and tuples are still unsupported, but I'd rather have a failing test case to work against.

Anyway, let me know if you find anything. Thanks.