Question about overloading

[ricardopieper]

Hello! Thanks for your work, I'm using this as a guide for some work I'm doing, with some changes to accomodate some quirks of my language that don't fit lambda calculus precisely, for instance, functions have 0 or more parameters (instead of functions that return functions in lambda calculus) and if/else statements.

I wonder, though: How could this be adapted to support overloading? Suppose I want to support operators, such as +, -, *, /, and so on, but the + operator acts on many inputs:

Int -> String -> String (concatenation) String -> int -> String (also concatenation) String -> String -> String (also concatenation) Int -> Int -> Int (sum)

for instance:

let plus = fn(a, b) => {
    a + b
} in plus(10, "20")

This fails because a + b only sees the t0 and t1 parameters I create on the fly, and this will unify with any of the 4 signatures, and I don't know exactly which one fits.

I'm currently trying a strategy of deferring for later (i.e. just return a new type variable and record the types involved and the possible signatures), then make the information at the call site somehow flow backwards, but so far no success.

I wonder if you can give me any directions on this issue.

[ricardopieper]

Another thought that crossed my mind is:

When I access the function during a function call, VAR will first instantiate the plus from the generalized Va Vb Vc -> a -> b -> c into d -> e -> f. Maybe I could then map it back to the original ungeneralized a -> b -> c, figure out a substitution a -> d, b -> e, c -> f, and because I know the types int and string when evaluating the function arguments, perhaps it's possible to do a unification usingint -> string -> g if and only if I know that plus needs to be inferred in this contrived way...

The problem is that this code type checks when it shouldn't:

let some_math = fn(a, b) => {
    (a + b) - b
};
some_math(10, \"20\")",

A + B is allowed, but the - B is not allowed because there is no string -> int -> ?? overload...

[domdomegg]

My understanding (which is likely to be wrong! something something Cunningham's Law) is that the way languages like Haskell get around this is to really be defining different functions, and then you test whether any of them could work. For example in this case you say + is really +₁ (forall a where a is stringifyable. string -> a -> string), +₂ (forall a where a is stringifyable. a -> string -> string), +₃ (int -> int -> int) and it must resolve to one of these at compile time.

In your second example, the fact that it compiles means the constraints aren't being resolved correctly or the polymorphic type you've given it is wrong - e.g. the minus there should have type int -> int -> int, which when unifying with the result of the addition forces it to be an int, which only matches the int -> int -> int option for +, which means both a and b must be int

See also:

• https://www.cs.tufts.edu/comp/150PLD/Notes/TypeClasses.pdf
• https://wiki.haskell.org/Performance/Overloading

[ricardopieper]

Thanks for the material!

I'm currently starting to learn OCaml and it already gives me some insights into how non-trivial this problem is under Hindley-Milner, not even OCaml really handles this. There are different operators depending on what you want.

With a type-annotated bottom-up type inference this looks much easier to pull off as I discovered myself. No wonder why Swift has some exponential behaviors around operators...

The way I thought about solving this problem is to branch off the solver when it finds an operation, i.e. tries int -> int -> int until the program is fully typed, if an error occurs then backtrack aalll the way back and try again with int -> string -> string, and so on. This is highly inefficient and perhaps it would be best to just generate the combinatoral explosion of possible functions.... or properly learn how Haskell does it.

[ricardopieper]

And I'd like to thank you again for the videos, awesome job!