decoupling type classes
Hi all, I have an idea about type classes that I have been experimenting. It appears to be a generalization to Haskell’s type classes and seems to be doable. It seems to related the three ideas: type classes, implicit parameters, and (typed) dynamic scoping. But I don't know whether it is good or not. I hope to get some opinions before going further. Basically, Haskell’s type classes passes dictionaries around. Each dictionary contains one or more “methods”. When “names” which belong to a dictionary are called, we invoke functions that match its principle type in the call site's scope. I have an experimental system which “decouples” the dictionary. Instead of passing on a dictionary, it passes individual “implicit parameters" around. Those implicit parameters are type inferenced and they can contain type parameters just as methods in a type class. Similarly, they are resolved by their types in the call site's scope. The convenience of this approach compared to Haskell’s type classes is that we no longer require a user of a type class to define ALL the methods in a type class. For example, a user could just define a method + without defining other methods in the Num class: -, *, … He can use the method + independently. For example, if + is defined on the String type to be concatenation, we can use + in another function: weirdConcat x y = x + y + y This has a utility, because the methods in the Num class don’t “make sense” for Strings except +, but the current type class design requires us to define them. Note here that weirdConcat will not have the type (Num a) => a -> a -> a, since we no longer have the Num class, it is decoupled into separate methods. 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. SOME IMPLEMENTATION DETAILS Here is how it can be implemented. When we see an “undefined” variable in a function definition which has been declared as “overloaded function”, we store the function name, and the type variables that are associated with it. For example, overload g — (explicitly declare g as an overloaded function) f x y (String s) = … … let z = g x s y in … … We don’t know what x and y are, but we know from the body of f that their types satisfy this pattern: g ’a String ’b. Thus we store this pattern constraint as an extra (implicit) argument in the type of f: f :: a → b → String (exist g: g a String b) We may have multiple such arguments. At the call sites of f, we look for a function g in the scope that satisfies the pattern g ‘a String ’b, but we don’t pass on the substitution, so they remain polymorphic. Once found, the function is passed as an extra parameter to f. This is essentially dictionary passing, but without grouping. It can be also more efficient because the parameters may be stored in registers. Here g is explicitly declared as “overloaded”, although my experimental system doesn’t need this. Any undefined variable inside function body automatically becomes overloaded. This may cause unintended overloading and it catches bugs late. That’s why we need the “overload” declarations. 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 …” 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". -- yin
Yin,
2012/1/12 Yin Wang
I have an idea about type classes that I have been experimenting. It appears to be a generalization to Haskell’s type classes and seems to be doable. It seems to related the three ideas: type classes, implicit parameters, and (typed) dynamic scoping. But I don't know whether it is good or not. I hope to get some opinions before going further.
I find your ideas interesting. You may be interested in a related design which I recently implemented for Agda [2], and an ICFP 2011 paper that presents it [1]. 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 have an experimental system which “decouples” the dictionary. Instead of passing on a dictionary, it passes individual “implicit parameters" around. Those implicit parameters are type inferenced and they can contain type parameters just as methods in a type class. Similarly, they are resolved by their types in the call site's scope.
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? 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.
The convenience of this approach compared to Haskell’s type classes is that we no longer require a user of a type class to define ALL the methods in a type class. For example, a user could just define a method + without defining other methods in the Num class: -, *, … He can use the method + independently. For example, if + is defined on the String type to be concatenation, we can use + in another function:
weirdConcat x y = x + y + y
This has a utility, because the methods in the Num class don’t “make sense” for Strings except +, but the current type class design requires us to define them. Note here that weirdConcat will not have the type (Num a) => a -> a -> a, since we no longer have the Num class, it is decoupled into separate methods.
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)?
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?
Here g is explicitly declared as “overloaded”, although my experimental system doesn’t need this. Any undefined variable inside function body automatically becomes overloaded. This may cause unintended overloading and it catches bugs late. That’s why we need the “overload” declarations.
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.
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?
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? Dominique Footnotes: [1] https://lirias.kuleuven.be/handle/123456789/304985 [2] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArg...
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.InstanceArg...
participants (2)
-
Dominique Devriese -
Yin Wang