Evidence Monomorphization

[b-studios]

This is still a WIP.

Right now there is a problem: for every different flow type we generate a fresh nominal type.
So, when we generate different types for the parameter of a function and for the argument at the call site, it is not surprising that we cannot call the function :)

As an example, here is the generated scheme code:

(define hof_535 (lambda (r_533)
  ($then ((apply0_943 r_533))
          (lambda (__927)
           (handle ([make-Exc_534 (raise$_946 (msg_539) resume_540 
           (pure #f))]) 
             (lambda (Exc$capability_878)
               ($then ((raise$0_947 Exc$capability_878) "")
                       (lambda (__930)
                        ((apply1_942 r_533))))))))))


(define main_536 (lambda ()
  (define exc_543 (make-Exc_534 (lambda (msg_541)
                                  (define tmp575_931 (println_12 msg_541))
                                  (pure tmp575_931))))
  (hof_535 (make-Function_940 (lambda ()
             (define tmp576_932 (println_12 "hello"))
             (pure tmp576_932))
            (lambda ()
             (define tmp576_932 (println_12 "hello"))
             (pure tmp576_932))))))

Note that at the callsite we create a make-Function_940, but at the definition site we use the accessor apply0_943 which belongs to a different function type.

This is not so clearly visible in the lifted/monomorphized core, since there the functions and selectors do not print unique ids:

interface Exc{raise$0}
interface Function{apply1; apply0}
interface Function{apply1; apply0}

def hof(r: () => Unit): Unit =
  r.apply0();
  try { (Exc$capability: Exc) => 
    Exc$capability.raise$0("");
    r.apply1()
  } with Exc {
    def raise$(msg: String, resume: (Unit) => Unit) = 
      ()
  };
def main(): Unit =
  def exc = new Exc {
    def raise$0(msg: String) = 
      let tmp575 = println(msg)
      
      tmp575
  }
  
  hof(new Function {
    def apply1() = 
      let tmp576 = println("hello")
      
      tmp576
    def apply0() = 
      let tmp576 = println("hello")
      
      tmp576
  })

We either need to rely on structural subtyping of the target, or insert coercions manually...

[b-studios]

There is still some way to go, but good news first: triples can be successfully monomorphized in the Chez-lift backend:

(define choice_1005 (lambda (n_1004 Fail$capability_1216 Flip$capability_1218)
  (if (infixLt_77 n_1004  1)
    ((Fail$0_2680 Fail$capability_1216))
    ($then ((Flip$0_2681 Flip$capability_1218))
            (lambda (tmp1105_1237)
             (if tmp1105_1237
               (pure n_1004)
               (choice_1005 (infixSub_28 n_1004  1)
                             Fail$capability_1216
                             Flip$capability_1218)))))))


(define triple_1008 (lambda (n_1006 s_1007 Fail$capability_1221 Flip$capability_1223)
  ($then (choice_1005 n_1006  Fail$capability_1221  Flip$capability_1223)
          (lambda (i_1031)
           ($then (choice_1005 (infixSub_28 i_1031  1)
                   Fail$capability_1221
                   Flip$capability_1223)
                   (lambda (j_1032)
                    ($then (choice_1005 (infixSub_28 j_1032  1)
                            Fail$capability_1221
                            Flip$capability_1223)
                            (lambda (k_1033)
                             (if (infixEq_70 (infixAdd_19 (infixAdd_19 i_1031
                                              j_1032)
                                              k_1033)
                                              s_1007)
                               (pure (MkTriple_1016 i_1031  j_1032  k_1033))
                               ((Fail$0_2680 Fail$capability_1221)))))))))))


(define handledTriple_1011 (lambda (n_1009 s_1010)
  (handle ((make-Flip_996 (lambda ()
                            (shift there
                           (lambda (resume_1034)
                            (define tmp1125_1238 (run (resume_1034 #t)))
                            
                            (define tmp1126_1239 (run (resume_1034 #f)))
                            (concat_1003 tmp1125_1238  tmp1126_1239)))))) 
    (lambda (Flip$capability_1227)
      (handle ((make-Fail_995 (lambda ()
                                (shift here
                               (lambda (resume_1036)
                                (pure (Nil_1023))))))) 
        (lambda (Fail$capability_1230)
          ($then (triple_1008 n_1009
                  s_1010
                  Fail$capability_1230
                  Flip$capability_1227)
                  (lambda (tmp1122_1240)
                   (pure (Cons_1024 tmp1122_1240  (Nil_1023)))))))))))


(define main_1012 (lambda ()
  (define tmp1131_1241 (run (handledTriple_1011 10  15)))
  
  (define tmp1132_1242 (println_12 tmp1131_1241))
  (pure tmp1132_1242)))

The important part to look at is shift there and shift here!

[b-studios]

We just looked at it together. There are a few limitations and open issues:

• local state and recursive functions do not always work (region polymorphic recursion)
• regions are not monomorphized, but are necessary for schedulers (can only be implemented as type monomorphic regions)
• error messages in case of region polymorphic recursion have non-existing error position.

Otherwise, we agreed to merge this. I'll go over it once more and then merge regardless of the missing things (TM).

[phischu]

The fact that Get and Put have an id : Id confused me a lot. These should be Expr.

[b-studios]

That's right -- for regions it could be general expressions. For local variables it is always just names.

In the source language this will always be names. How would you read from / write to a more complicated variable expression?

For example

f(x) = 3

is not wellformed, it needs to be:

var z ...;
z = 3

Of course, we could in principle generalize here, but I don't see the value of that, yet.

If we would generalize, then it would be a block, not an expr, no? References ought to be second-class.

[b-studios]

Long story short: References are not (yet) first (second) class citizens.

[b-studios]

@CodiumAI-Agent /review

(good luck ;) )

[CodiumAI-Agent]

PR Analysis

• 🎯 Main theme: Monomorphization of functions in the Effekt language
• 📌 Type of PR: Enhancement
• ✨ Focused PR: True
• 🔒 Security concerns: No security concerns found

PR Feedback

• General suggestions: The PR seems to be a work in progress and is focused on implementing monomorphization for the Effekt language. The changes are quite extensive and touch multiple files. It would be beneficial to add tests to ensure that the new functionality works as expected and does not introduce regressions.

• 🤖 Code feedback:

  • relevant file: effekt/shared/src/main/scala/effekt/lifted/mono/Elaborator.scala
    suggestion: Consider refactoring the elaborate method. It's quite large and handles many cases, which makes it hard to understand and maintain. You could split it into smaller, more manageable methods, each handling a specific case. [important]
    relevant line: def elaborate(s: Stmt)(using T: TransformationContext): Stmt = s match {

  • relevant file: effekt/shared/src/main/scala/effekt/lifted/mono/Elaborator.scala
    suggestion: The elaborate method seems to be recursive. Make sure to handle potential stack overflow errors that might occur with large inputs. [medium]
    relevant line: def elaborate(s: Stmt)(using T: TransformationContext): Stmt = s match {

  • relevant file: effekt/shared/src/main/scala/effekt/lifted/mono/Elaborator.scala
    suggestion: The elaborate method seems to be doing a lot of pattern matching. Consider using a visitor pattern or similar to make the code more maintainable and easier to extend in the future. [medium]
    relevant line: def elaborate(s: Stmt)(using T: TransformationContext): Stmt = s match {

How to use

Tag me in a comment '@CodiumAI-Agent' and add one of the following commands:
/review [-i]: Request a review of your Pull Request. For an incremental review, which only considers changes since the last review, include the '-i' option.
/describe: Modify the PR title and description based on the contents of the PR.
/improve: Suggest improvements to the code in the PR.
/ask <QUESTION>: Pose a question about the PR.

To edit any configuration parameter from 'configuration.toml', add --config_path=new_value
For example: /review --pr_reviewer.extra_instructions="focus on the file: ..."
To list the possible configuration parameters, use the /config command.