Length polymorphism in Comp language?

[edsko]

The following program does not type check:

fun comp f(a : arr int) {
  emit length(a);
}

fun comp test() {
  a <- take;
  emit a;
  f({1});
  f({1, 2});
} 

let comp main = read[int] >>> test() >>> write[int];

Do we not support length polymorphism in the comp language? (There is a TODO in the type checker code for this, too.)

[edsko]

This affects typechecking of map, too.

[dimitriv]

Yes, at the moment we don't support length-polymorphism at the computation level. We never needed it really so far, so I never bothered implementing (contrary to the expression-level polymorphism which turned out to be useful for @bradunov). But maybe it's actually not hard to implement now given all our refactorings? I would also not mind leaving this for later if there are more important things (e.g. optimization cleanup in PassFold, or the partial evaluator) in flux.

[edsko]

Let's talk about this later. There's a long email for you in my draft folder :)

[edsko]

Note that even if we say that comp functions cannot be length polymorphic, we should probably still deal with length polymorphic expression functions when they are called from the comp language (for instance, when they appear as a call to map).