“ Failed to compile expression due to unresolved type constraints” for unused lambda in let clause

[hpcx82]

 let
     bar = (\x.match x with
         | "usd/jpy" -> "G7"
         | _         -> "others")
 in
     ()

Above code will produce compile error:

syntax.hob:6,1-11,6: Failed to compile expression due to unresolved type constraints
  Array a char
  ArrayView a b
 3     | _         -> "others")
 4
 5
 6 let
 7     bar = (\x.match x with
 8         | "usd/jpy" -> "G7"
 9         | _         -> "others")
10 in
11     ()

But below cases are all ok:

// outside of "let"
foo = (\x.match x with
     | "usd/jpy" -> "G7"
     | _         -> "others")


// Specify type explicilty:
 let
     bar = (\x.match x with
         | "usd/jpy" -> "G7"
         | _         -> "others")::[char]->[char]
 in
     ()

// Call the lambda
 let
     baz = (\x.match x with
         | "usd/jpy" -> "G7"
         | _         -> "others")
 in
     baz("")

What might be the explanation for such behavior?

[chenkai036]

Hi @baiyanhuang, IIRC, the variable x in the pattern matching can be any type as long as it satisfies the contract of Array(View) c char, meaning type c behaving like an array/view of char. A few concrete types, e.g. char array itself, std::string or possibly std::vector<char>, have the property. Therefore, the input type of lambda isn't actually determined when it's defined (like a function template). However a let-expression requires all the types to be resolved when hobbes evaluates its outcome. Due to this, the previous lambda causes the error in your first example, even though the expression doesn't care of the type of lambda and simply returns nothing. The second example will work because you enforce a concrete input type of the lambda and there is no unknown type left since then. The last example will infer the type during evaluating the call to baz(""), where you implicitly tell hobbes that the input type is a string.

Perhaps it's a good idea to provide user some friendly error messages in case of such errors.

[kthielen]

Exactly, we can't produce output code until we're certain that the expression that we're compiling has a fixed type (a monotype). Because that function in your let expression is polymorphic, even though you don't use it, the whole expression is polymorphic.

In the general case, you could have an expression like "let x=E in ()" or "let x=E in P" where x is not used in P. If we didn't have to worry about side-effects, then we could just rewrite those expressions to "()" or "P" and then they'd have monotypes and it would be fine. But we do have to worry about side-effects, since "E" could have some other effect. And because E is polymorphic, it might have a different effect depending on the indexed type (e.g. for ints, launch missiles, for doubles, buy a boat, etc).

In your specific case, because the expression is a function definition (but not because it has a function type, since expressions with side-effects can have function types, like e.g. "let _=print(42) in (+)"), it would be possible to drop the unused function definition without changing the meaning of the program.

So TLDR, it might be worthwhile to allow this and quietly drop the function definitions in let expressions where they aren't used.

[hpcx82]

Thanks Kalani, Kai,

so in let expression, it is required that all types are resolved, but not in global context? like

// outside of "let"
foo = (\x.match x with
     | "usd/jpy" -> "G7"
     | _         -> "others")

what is the rationale behind that?

[kthielen]

No it's possible to have polymorphic definitions in let expressions too. But global polymorphic functions are also very useful, since you might use 'foo' one way (with an std::string argument) and then also another way (with an array argument). It is very common for us to do this kind of thing. We like polymorphic definitions.

But where we started was that you had an expression, which happened to be a let expression, and you used it in a context where it needed to have a definite monotype (e.g. it had to be a function taking in an array and returning bool).

So the problem was that you had a point where you said that your expression had to have this definite monotype, but then type analysis determined that it didn't have that type (and in your case, the reason was that it had this polymorphic inner definition that wasn't decided). That's where the problem came from -- in your program you have something like 'c.compileFn<bool(const array*)>(exp)' and so there's no choice but to require that 'exp' has that definite monotype.

Does that make sense?

It's not the case that types always have to be definite monotypes in let expressions. For example, you can have a polymorphic function like:

foo x = let z=x+x in z*z

That function is (bounded) polymorphic, since you can use it with int, double, etc (any type supporting addition and multiplication). Further, its inner let expression is polymorphic. That's all fine, because it's not defined in a context where it is required to have a definite monotype.

Hope this helps.

[hpcx82]

Thanks Kalani, I got one more question:

you used it in a context where it needed to have a definite monotype (e.g. it had to be a function taking in an array and returning bool).

Why is this? and what is difference between inside let, or in global? when I have the same function defintion?

[kthielen]

Well what I meant there is that you might force the monotype requirement by how you use the hobbes::cc class. For example, you might compile a function with cc.compileFn<bool(Foo*)>(expr) in which case you force "expr" to be an expression with exactly the type 'bool(Foo*)' (or 'Foo -> bool' if you like writing it that way). Knowing how your application code uses this class, I think that's very likely where it'd be traced back to.

If you have a let expression, the whole expression type depends on the definitions you include and those definitions are only scoped for that expression. So you could write something like:

> sum([let x = 5 in x+x, let x=200 in x*x])
40010

There you have two let expressions with two independent scopes, even though they use the same variable name the bindings are independent.

You can make definitions that have polymorphic let bindings, though in general it's important to have definitions with constraints (or unbound type variables) that are coherent (have some eventual path to monotype resolution). This is what an incoherent definition looks like:

> foo = let a = zero; b = [a] in ()
> :t foo
HasZero a => ()

There you have a polymorphic let, but you'll never be able to use it for anything because there's nothing that relates its values to its type variables. It might be worth rejecting definitions like this too.