Ad Hoc Polymorphism · beginners · Zulip Chat Archive

My understanding is that global type inference is not possible if there's ad hoc polymorphism?

Martin Stewart (Feb 26 2023 at 17:12):

In case I'm mixing up the terminology, my understanding of ad hoc polymorphism is that it lets you do

foo : A, A -> Bool

foo : B -> I64

foo : a, a -> a

or in other words, have multiple functions with arbitrary type signatures have the same name and the correct one will be used during runtime

Assuming I have that right, and assuming it does prevent decidable type inference, it seems to me like it wouldn't be very difficult to just write

foo : A, A -> Bool

foo2 : B -> I64

foo3 : a, a -> a

Richard Feldman (Feb 26 2023 at 18:30):

so Abilities let you do ad hoc polymorphism, but we don't have documentation for them yet :sweat_smile:

Ayaz Hafiz (Feb 26 2023 at 18:34):

we are able to keep decidable type inference except for the specific case where ad-hoc polymorphism cannot be resolved for a type that doesn't come into or out of a function type. For example,

ability Evil has
  make : Str -> a | a has Evil
  destroy : a -> Str | a has Evil

f = \s -> destroy (make s)

clearly we don't know what a has Evil to instantiate inside of f here, so this will become a type error.

But, if the type of a was taken into the function (or was exported out), the inference would be complete

Ayaz Hafiz (Feb 26 2023 at 18:35):

Martin Stewart (Feb 26 2023 at 18:42):

I stand corrected then! I had thought that ad hoc polymorphism was one of the reasons that languages like C# and Java didn't support global type inference. I guess it has more to do with subtyping then?

Ayaz Hafiz (Feb 26 2023 at 18:43):

Kesanov (Feb 27 2023 at 13:46):

How do you plan to deal with it? The sane solution that came to my mind was to disallow make-like constructors.

Ayaz Hafiz (Feb 27 2023 at 14:09):

You could disallow them, but that would make illegal real usage patterns we want to allow (like encoding/decoding) so it’s not an option. The way we plan to do this is to detect such problems during typechecking. The cases where this can happen are well defined and I have an algorithm for how to check them.

Notification Bot (Feb 28 2023 at 00:41):

Kesanov (Feb 28 2023 at 09:51):

Isn't that the same as saying: we are willing to sacrifice automatic type inference?

Richard Feldman (Feb 28 2023 at 12:51):

the types are inferred correctly, it's just that the code has an error :big_smile:

Richard Feldman (Feb 28 2023 at 12:52):

like if I write x = {} + 1 the type checker correctly infers the type of x to be an error, because {} + 1 is an invalid expression

Richard Feldman (Feb 28 2023 at 12:53):

with f = \s -> destroy (make s) it's the same - we can infer what all the types involved are, and we also know this is an invalid expression, so we want to report an error

Richard Feldman (Feb 28 2023 at 12:54):

in contrast, sacrificing type inference means "what you've written is valid, but I don't know what type I should infer for it" - which doesn't come up here

Ayaz Hafiz (Feb 28 2023 at 13:48):

To clarify - f = \s -> destroy (make s) is ambiguous because the type cannot ever be inferred, and in that sense it's an error. The compiler can't materialize a type you want, and in fact no compiler could. You could imagine a world where there are some rules for the "default" ad-hoc specialization inferred, but that is unlikely the behavior you want

Kesanov (Feb 28 2023 at 21:18):

Hm, but it seems awfully close to broken type inference, since you basically say to the user:
1) I don't know what type this has exactly.
2) Please, specify the type explicitly.
Which is exactly the same thing you would say, if you couldn't infer type for something.

Ayaz Hafiz (Feb 28 2023 at 21:20):

It's a bit different - the type inference cannot be decidable. The type inference is still complete. But, if the type is undecidable, it must be the programmer that specifies what type they want. I don't think that's broken, since you couldn't have any machine where the type could be materialized without deambiguation

Ayaz Hafiz (Feb 28 2023 at 21:38):

it's kind of similar to saying, please choose a type for the value "1 + 1". The question is a bit ambiguous - do you want a signed integer, a one-byte integer, and 8-byte integer, etc? In a sense the question is undecidable. Most languages including Roc choose a default in these cases, because they can guess that you may have reasonably meant, for example, a signed 64-bit integer.

With ad-hoc polymorphism you can wind up in the same kind of question, but there is often not a reasonable default. So the question is just deemed undecidable. But when the question can be decidable, the type inference is complete.

Ron Panduwana (Mar 01 2023 at 00:44):

Brian Carroll (Mar 01 2023 at 07:38):

It's only type inference. All it can do is pick a type. That can't change your function into the identity function.

Brian Carroll (Mar 01 2023 at 07:40):

And we don't want the type checker to implicitly replace your code with something different if you make a mistake. I'd much prefer an error.

Anatoliy Baskakov (Mar 20 2023 at 11:43):

Inline type annotation could help, I believe. Not sure if it is planned for roc, though.

Stream: beginners

Topic: Ad Hoc Polymorphism

Kesanov (Feb 26 2023 at 09:57):

Martin Stewart (Feb 26 2023 at 17:06):