feat: open lambda effect

[JonathanStarup]

Two typing changes:

• in def name(args...): type \ ef1 = e: type \ ef2 it is required that ef2 + alpha = ef1
  • This eliminates the need for a lot of checked_ecast(???) and touch(rc)
• in x: type1 -> e: type2 \ ef the final lambda type is type1 -> type2 \ ef + alpha

This is used to remove functions

• constant(x: t): Unit -> t \ ef
• identity(x: t): t
• eidentity(x: t): t \ ef
• touch(_rc: Region[r]): Unit \ r

which were primarily used to upcast effects. this makes community builds fail.

[magnus-madsen]

We should be able to remove the checked_ecasts in the std lib now, right?

[JonathanStarup]

All checked_cast removed. very slow. downside is also that we taint the definition instead of checking at application so information is less precise

[magnus-madsen]

downside is also that we taint the definition instead of checking at application so information is less precise

What do you mean?

[magnus-madsen]

Will you investigate the failing tests?

[JonathanStarup]

downside is also that we taint the definition instead of checking at application so information is less precise

What do you mean?

fx that x -> x will have type a -> a \ Crash if needed, this means that we might instrument pure code with effect handler things because of the larger effect. It would be more exact to enlarge the effect use-site (a la proper subtyping) because the definition would still say pure

[magnus-madsen]

downside is also that we taint the definition instead of checking at application so information is less precise

What do you mean?

fx that x -> x will have type a -> a \ Crash if needed, this means that we might instrument pure code with effect handler things because of the larger effect. It would be more exact to enlarge the effect use-site (a la proper subtyping) because the definition would still say pure

I see. But we were struggling to make that work? What do you propose?

[JonathanStarup]

It was just an observation, its nice to have this as a solution

[JonathanStarup]

@magnus-madsen it solves all of our checked_ecast uses

[magnus-madsen]

We have an identity function :) and even an eidentity :)

[magnus-madsen]

Oh. You removed OK 👍

But lets please not call an argument id. We can call it z or w.

[magnus-madsen]

It seems the base system works then? (Other than a horrible slowdown)

What about integration with the rest of the compiler? Monomorphization? Purity reflection? Traits?