[Haskell-cafe] decoupling type classes

[Yin Wang]

> Also, you don't seem to have thought about the question of parametric
> instances: do you allow them or not, if you do, what computational
> power do they get etc.?

I may or may not have thought about it. Maybe you can give an example
of parametric instances where there could be problems, so that I can
figure out whether my system works on the example or not.


> I'm surprised that you propose passing all "type class" methods
> separately. It seems to me that for many type classes, you want to
> impose a certain correspondence between the types of the different
> methods in a type class (for example, for the Monad class, you would
> expect return to be of type (a -> m a) if (>>=) is of type (m a -> (a
> -> m b) -> m b)). I would expect that inferencing these releations in
> each function that uses either of the methods will lead to overly
> general inferenced types and the need for more guidance to the type
> inferencer?

I thought they should be of type (a -> m a) and (m a -> (a -> m b) ->
m b)), but I just found that as if they should also work if they were
of type (c -> m c) and (m a -> (a -> m b) -> m b)).

It doesn't seem to really hurt. We either will have actually types
when they are called (thus catches type errors). Or if they stay
polymorphic, c will be unified with a when they bind. Also, return and
(>>=) will be dispatched to correct instances just as before.


> By separating the methods, you would also lose the laws that associate
> methods in a type class, right?
>
> An alternative to what you suggest, is the approach I recommend for
> using instance arguments: wrapping all the methods in a standard data
> type (i.e. define the dictionary explicitly), and pass this around as
> an implicit argument.

I went quickly through your paper and manual and I like the explicit
way. The examples show that the records seem to be a good way to group
the overloaded functions, so I have the impression that "grouping" and
"overloading" are orthogonal features. But in your paper I haven't
seen any overloaded functions outside of records, so I guess they are
somehow tied together in your implementation, which is not necessary.

Maybe we can let the user to choose to group or not. If they want to
group and force further constraints among the overloaded functions,
they can use overloaded records and access the functions through the
records; otherwise, they can define overloaded functions separately
and just use them directly. This way also makes the implementation
more modular.


> For this example, one might also argue that the problem is in fact
> that the Num type class is too narrow, and + should instead be defined
> in a parent type class (Monoid comes to mind) together with 0 (which
> also makes sense for strings, by the way)?

I guess more hierarchies solves only some of the problem like this,
but in general this way complicates things, because the overloaded
functions are not in essence related.


>> There is another benefit of this decoupling: it can subsume the
>> functionality of MPTC. Because the methods are no longer grouped,
>> there is no “common” type parameter to the methods. Thus we can easily
>> have more than one parameter in the individual methods and
>> conveniently use them as MPTC methods.
>
> Could you explain this a bit further?

In my system, there are no explicit declarations containing type
variables. The declaration "overload g" is all that is needed.

For example,

overload g
 ... ...
f x (Int y) = g x y


then, f has the inferred type:

'a -> Int -> {{ g:: 'a -> Int -> 'b }} -> 'b

(I borrowed your notation here.)

Here it automatically infers the type for g ('a -> Int -> 'b) just
from its _usage_ inside f, as if there were a type class definition
like:

class G a where
  g :: a -> Int -> b

So not only we don't need to defined type classes, we don't even need
to declare the principle types of the overloaded functions. We can
infer them from their usage and they don't even need to have the same
principle type! All it takes is:

overload g

And even this is not really necessary. It is for sanity purposes - to
avoid inadvertent overloading.

So if g is used as:

f x y (Int z) = g x z y

then f has type 'a -> 'b -> Int -> {{ g :: 'a -> Int -> 'b -> 'c}} -> 'c

Then g will be equivalent to the one you would have defined in a MPTC method.


> I would definitely argue against treating undefined variables as
> overloaded automatically. It seems this will lead to strange errors if
> you write typo's for example.

I agree, thus I will keep the "overload" keyword and check that the
unbound variables have been declared as overloaded before generating
the implicit argument.


>> But the automatic overloading of the undefined may be useful in
>> certain situations. For example, if we are going to use Haskell as a
>> shell language. Every “command” must be evaluated when we type them.
>> If we have mutually recursive definitions, the shell will report
>> “undefined variables” either way we order the functions. The automatic
>> overloading may solve this problem. The undefined variables will
>> temporarily exist as automatic overloaded functions. Once we actually
>> define a function with the same name AND satisfies the type
>> constraints, they become implicit parameters to the function we
>> defined before. If we call a function whose implicit parameters are
>> not associated, the shell reports error very similar to Haskell’s
>> “type a is not of class Num …”
>
> The design you suggest seems to differ from Haskell's current
> treatment, where functions can refer to other functions defined
> further in the file, but still have them resolved statically?

Yep. What I was talking about was a fantasy that if one day we have an
operating system written in Haskell and its shell language and command
line language are also Haskell, then this kind of implicit overloading
can help making the shell work more interactively. It could accept
definitions containing undefined variables by treating them as
implicit arguments.



>> RELATIONSHIP TO DYNAMIC SCOPING
>>
>> It seems to be helpful to think of the “method calls” as referencing
>> dynamically scoped variables. They are dispatched depending on the
>> bindings we have in the call site's scope (and not the scope where the
>> method is defined!). So it is very much similar to the much-hated
>> dynamic scoping. But the dispatching is more disciplined — it doesn't
>> just match the name. It must match both the name and the inferred
>> principle type.
>>
>> This intuition also explains why local instances shouldn't be allowed,
>> because if we capture the variables at the definition site, the method
>> call becomes "statically scoped".
>
> I don't understand this argument: do you mean that if I write a
> function that does "(4 :: Int)+4", you don't want to statically
> resolve this to a certain (local or not) instance of + for Int that is
> in scope at this call site?

Certainly + should be resolved to a certain instance of +, but the
instance should be visible to the call site and not definition site.
If the instance is only visible at the definition site, it shouldn't
be captured.

Let me post an example from Oleg:

"""
foo x =
 let overload bar (x:Int) = x + 1
 in \() -> bar x

Now,

baz =
 let overload bar (x:int) = x + 2
 in foo (1::Int)

To which bar the reference within foo resolves? One may say: to
baz's bar. On the other hand, since we instantiate the polymorphic
function foo to x being an Int, then foo's bar is also eligible.

For that reason, local instances in Haskell were not allowed (although
they have been considered in the first Wadler's paper on type classes,
and rejected for this reason).

"""

Here at the call site foo (1::Int), bar should be resolved to the one
inside baz, and not the one inside foo. My analogy to "dynamic
scoping" is useful to understand the reason here. If we capture the
bar inside foo's definition site, it would correspond to "lexical
scoping".


> Footnotes:
> [1]  https://lirias.kuleuven.be/handle/123456789/304985
> [2]  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments