Type classes and named implementations

[Mesabloo]

There are multiple ways to handle ad-hoc polymorphism (re-defining a given function with different types):

1. Going for the “C++ way”, where ad-hoc polymorphism is unrestricted and difficult to type. This also makes type errors harder to show, and type inference much harder to implement.
2. Going for the “Haskell way”, where ad-hoc polymorphism is managed through the use of type classes and class implementations. This makes type-checking a bit easier than the first approach, but still complicates things quite a bit.
3. Simply no ad-hoc polymorphism, which is not very satisfactory.

The retained option is number 2, adding type classes and implementations.
For this to work, we have to think about:

1. type constraints:
   • we have to have a constraint kind representing any concrete (fully applied) constraint.
   • ∀-quantified variables can be restricted to only have implementations for specific implementations (taking in account the -XFlexibleConstraints extension of Haskell).
   • a constraint is considered ambiguous if any of its type variable arguments is left unused in the function type, e.g. forall<a | show(a)> u64 -> u64
2. type classes:
   • type class defiinitions can only contain type variables in their heads, and reference those inside the members' types.
3. type class implementations:
   • type class implementations are unrestricted (taking the -XFlexibleInstances, -XMultiParamTypeClasses and some other Haskell extensions as default) and also allow using a special _ (or ·) as a sort of a “function hole” (like at the expression level). This is sufficiently restricted not to need higher order unification of type terms (which would be undecidable).

Originally posted by @Mesabloo in #4 (comment)

[Mesabloo]

With all the “recent” changes in the language, all this will need happen that way.

Let's elaborate.
A typeclass is basically a record definition. An instance is a specific value of the given typeclass.
In programming languages such as Haskell, this behavior is not revealed in the surface language and is only present in the core language.

For Zilch, we want to go the Agda way, with a specific {{id : ty}} parameter construct which automatically opens id at the beginning of the scope. ty may be restricted to only be a record type (a true record type, not a module or anything else alike).
A {{id : ty}} is basically the same as {open id : ty} but with extra heuristics for “instance resolution”.
Therefore there will not be any specific construct in the surface language.