Typeclasses (and MLsub)

This post is a continuation to the previous post in that it's studying how Hindley-Milner type inference concepts translate to MLsub type inference.

I studied Hindley-Milner few weeks ago. I think that was important for understanding MLsub well. So you don't need to study HM, I will try to write this post such that you learn the necessary details for understanding this post, while you read.

Typeclasses arise from the polymorphic type inference almost as if they were there all along. The idea is that you create a type signature and associate it to a constraint, like this:

eq :: forall a. Eq(a) => (a, a) -> bool

Lets examine this line a bit:

1. eq :: tells that this is the type signature of eq variable.
2. The forall a. means that when the type is instantiated, the a variable is replaced with a fresh variable in the expression.
3. Eq(a) => is the constraint, this is used to select among implementations of the eq.
4. (a, a) -> bool is a type signature of a function that takes in two values that are then unified, and the result has to be of the type bool.

This allows you to provide many implementations for eq, rather than just one.

Type inference in HM

To see this in practice, lets do some HM type inference for the following simple expression eq(1,n).

To inference types for this clause, we have to provide a type environment for every variable that appears in the expression.

We do not define what n is, but it needs a type signature in the type environment. The type environment with our eq is the same as before. With these changes we get the following input for type inferencer:

eq :: forall a. Eq(a) => (a, a) -> bool
n :: b
eq(1, n)

HM type inference involves opening the expression being type inferenced, the result of that open is:

eq(1, n) : c
{eq} == ({1},{n}) -> c
eq : instantiate(eq)
1 : int
n : instantiate(n)

The instatiation of n ends up with type variable b, because that's in the type environment, but eq ends up instatiating the constraint for our typeclass. The class is lifted up from the expression to the top after the instatiation is finished.

eq(1, n) : Eq(d) => c
{eq} == ({1},{n}) -> c
eq : (d, d) -> bool
1 : int
n : b

Now we can eliminate the equality constraint:

eq(1, n) : Eq(d) => c
(d, d) -> bool == (int, b) -> c

It is broken into pieces...

d == int
d == b
bool == c

And now we can substitute.

eq(1, n) : Eq(int) => c
(int, int) -> bool == (int, b) -> c
int == b
bool == c

The type of n changes because the b is substituted away:

n :: int
eq(1, n) : Eq(int) => c
(int, int) -> bool == (int, int) -> c
bool == c

And finally we get:

n :: int
eq(1, n) : Eq(int) => bool
(int, int) -> bool == (int, int) -> bool

The constraint has been eliminated, we also have type inferenced the expression eq(1, n).

The type is Eq(int) => bool.

Aside that the typeclass constraint ends up being dragged along, we haven't done anything here so far that would be different from doing the ordinary Hindley-Milner type inference.

So the typeclass constraint is filled. After the type inference we can look at this constraint and select the implementation for Eq(int) if it exists.

Likely questions

If you did read through the example, and you are not familiar with HM yet attentive, you ended up with some questions or complaints.

Recursion issues

Many useful computer programs are recursive. Since the constraint for a type class is instantiated, won't we end up with infinitely many Eq(...) -clauses to our type if it's recursive?

Recursion was already a problem for parametric polymorphism, and therefore the problem has been already solved. In the example I pointed out that the type environment needs to be filled before the type inference can happen.

The constraints for the type environment are satisfied by replacing the closed form recursion with open form recursion. Below examples of closed-form and open-form recursive definition of factorial:

fact(x)       = if x == 0 then 1 else x * fact(x-1)
fact(fact)(x) = if x == 0 then 1 else x * fact(x-1)

The original closed form is retrieved by using the fixed-point combinator, below an example of what it does:

fix(fact)
let x = fact(x) in x
let x = fact(x) in fact(x)
let x = fact(x) in fact(fact(x))
let x = fact(x) in fact(fact(fact(x)))
...

We do not need to open the fixed-point combinator though, so it allows us to isolate the recursion into the combinator.

We know the type signature for fix and it's easy to derive by hand. It is the forall a. (a -> a) -> a.

Understanding the above may prove to be an useful reference when solving similar, recursively defined constraint satisfaction problems in general.

Type signature explosion

An another concern that may arise is when you notice that every callsite essentially introduces a new constraint to worry about. For example, say you use the eq twice, such as below:

test(a,b,c) = (eq(a, b) and eq(b, c))
test :: forall a. (Eq(a), Eq(a)) => (a, a, a) -> bool

Eq(a) appears twice because eq is used twice, but it's the same constraint that has to be solved here. We do not need to specify it twice.

This is a real issue and needs to be solved. It is discussed on the page 17. of "Typing Haskell in Haskell", by Mark P. Jones.

Free variables, defaulting

What if the type inference doesn't inference the types? For example, like in the following expression:

lit :: forall a. Lit(a) => int -> a
add :: forall a. Add(a) => (a,a) -> a
add(lit(4), lit(2)) : (Lit(a), Add(a)) => a

Clauses that are not perfectly defined can be generalized, but there's a problem if you have to evaluate this. You literally cannot know what should evaluate in place of lit(4).

One option is to type default, which is likely a good choice in an interactive prompt. Other times it's better to not assume anything.

Problem partially unsolved

Next if you go creative with typeclasses, you may end up with a situation where you end up with constraints that cannot be solved individually but can be solved together.

For example, this could happen if you separate everything in the typeclass constraint into free variables:

add :: forall a b c. Add(a,b,c) => (a,b) -> c

Now if we have an expression with many calls to add, we end up with following result after the type inference:

(Add(int, int, a), Add(a, int, b) => b

We might have the following implementations:

Looking at the implementations it would seem that we could solve this puzzle through eliminating implementations that do not fit, but notice that a free type variable is a proposition that the type could be anything. Therefore doing backsubstitution a with int would correspond to defaulting.

Note that wildcards on the implementation side of the typeclasses can be acceptable. For example:

Eq(a) => Eq([a])

Is a valid implementation type signature for the Eq typeclass.

Implementation aspects

Further intuition about typeclasses can be gathered by reading about the ways they are implemented. "Implementing and Understand Type classes" is good reading for this purpose.

I haven't read "Typing Haskell in Haskell" yet, but I'm planning to do so next week. It looks like a good paper describing details here.

Now with subtyping

There are cases where MLsub doesn't need typeclasses for things that need typeclasses in ML. Types themselves can fuse together and depart without needing the typeclass mechanism, for example:

print :: printable() -> unit

Every object with "printable" -property can satisfy this expression. We may also treat attribute access like this:

.x :: forall a. get_x(a) -> a

But these are merely parametric traits. These typing schemes are analogous to doing unification with parametric typing.

Typeclasses would appear to become even stranger under subtyping. For this reason I'm not sure about what they might represent or how they could be used.

Here are two interesting typeclass signatures, I haven't named them because I'm not sure what they might be:

aa :: forall a. A(a) => (a) -> unit
bb :: forall a. B(a) => () -> a
cc :: forall a. C(a) => a

What if we just used them like they would be used in ML?

lit :: forall a. Lit(a) => int -> a
add :: forall a. Add(a) => (a,a) -> a

One central concept in subtyping is variance. What is the variance of the variables in a typeclass constraint?

The right side of the expression must be covariant so that we can apply using it. Below a rough graph about what happens on a function call:

+ +     -      (-, -) input
| |     |       |  |
(-,-) -> +  <:  (+, +) -> - ----> + output

Well we can see what would actually happen if we did this in a subtyping system. The rules can be applied very much in the same way as they were applied with ordinary Hindley-Milner type inference.

So lets take an earlier example and the types.

lit :: forall a. Lit(a) => int -> a
add :: forall a. Add(a) => (a,a) -> a

Lets solve the lit(5) first:

lit(5) : a
{lit} <: {5} -> a
lit : Lit(b) => int -> b
5 : int

(int -> b) <: int -> a
int <: int
b <: a

The first bisubstitution means we replace contravariant b with a&b. Lit(b) is lifted up again. We treat Lit as if it was a bivariant clause.

lit(5) : Lit(<a&b, b>) => a

We can duplicate the result for lit(2), now we have to solve the rest of the problem:

add(lit(5), lit(2)) : f
{add} <: ({lit(5)}, {lit(2)}) -> f
add : Add(e) => (e,e) -> e
lit(5) : Lit(<a&b, b>) => a
lit(2) : Lit(<c&d, d>) => c

There are so many typeclass constraints that we lift them a level up, and then we do the constraint elimination as before:

Add(<e,e>), Lit(<a&b, b>), Lit(<c&d, d>) =>
add(lit(5), lit(2)) : f
((e,e) -> e) <: (a,c) -> f
a <: e
c <: e
e <: f

None of these bisubstitutions are on concrete type, so we keep doing the bisubstitution with contravariant sides.

Add(<e&f,e>), Lit(<a&b&e&f, b>), Lit(<c&d&e&f, d>) =>
add(lit(5), lit(2)) : f

Now the types should be simplified a bit. The a and c no longer create any flow so they can be discarded, also the e and f flows always appear together, so they can be fused.

add(lit(5), lit(2)) : (Add(<e,e>), Lit(<b&e, b>), Lit(<d&e, d>)) => e

It also looks like we can fold the bivariants because the opposite flows do not appear anywhere, and finally the two Lit constraints are similar so we can fold them too.

The final type is:

add(lit(5), lit(2)) : (Add(a), Lit(a)) => a

The expression no longer appear to have any concrete type, although we use constructors there.

Also...

add(lit(5), frac(2.5)) : (Add(a), Lit(a), Frac(a)) => a

The meaning of these expressions would appear to depend entirely on what properties the resulting type has to have.

So we end up to select, or generate, a method based on what is required. Alternatively we select it by what is going to be given.

Note that the concrete types will still flow through the (a,a) -> a here. For example:

add(lit(5), 2) : (Add(<a, a|int>), Lit(a)) => int|a

The information in the Add constraint appears to provide enough information so that we can reliably typecheck that the function we select will fill the location correctly.

How should we select the implementation? How to ensure that we don't make a puzzle out of this? I'm not sure whether I have answer to these yet.

Usecases

Without typeclasses, ML or Haskell would be too strict. MLsub in other hand appears to make it difficult to be strict enough.

The purpose of typeclasses in MLsub is unclear though. They can be used to decide constructors by what the value is used for though.

Taggless-final style presents typeclasses as a mechanism for constructing domain specific languages on top of a strictly typed language. Motivated from the need to find out a good basis for computer algebra, I found some curiosity for tagless-final style and realised that the "traits" in a subtyping model might not entirely correspond to typeclasses.

I probably have to implement the typeclasses to find out what uses they have in MLsub -style type inferencers.