On Mon, Mar 22, 2010 at 10:57 AM, Pal-Kristian Engstad <[email protected]> wrote: > In this context, I'd highly recommend reading: Objects to Unify Type Classes > and GADTs, by B. Oliviera and M. Sulzmann. It might provide the answer to > your question.
Thanks. This paper came up here very recently, but I confess that I am having a hard time getting my head around it. My initial response to the paper here was less than constructive. Perhaps some of you here can help. For those who want to have a look, the paper is here: http://ropas.snu.ac.kr/~bruno/papers/Objects.pdf My first confusion starts with a terminology issue. In all likelihood, I am "stuck" in the notions of "class" and "object" that I have from C#/Java/C++, so I am having a hard time translating the terminology of the paper into my head. On page 2 of the paper, I would have characterized "Set 'a" as a "family", the ListSet object as a class, and instances of the ListSet objects as "objects". [Note: I'm guilty of this problem myself with DEFOBJECT] It appears to me that in the definition of ListSet, what has happened here is that we end up with a bunch of functions that are closed over the state of the particular ListSet instance. In BitC, we would call these methods. The signatures declared in the definition of "Set 'a" notably exclude this state. Now that I look at it, Bruno's "class" mechanism smells a lot like what I originally called DEFCAPSULE and is now DEFOBJECT in BitC. Bruno's "object" declaration in turn looks a lot like my mechanism for instantiating capsules from "matching" structures, except that it collapses the declaration of the structure into the same syntactic construct. If I am understanding what is going on, the ListSet constructor returns something that is of type "Set 'a" rather than "ListSet", and the implementation state of ListSet thereby becomes existentially typed. In effect, the ListSet declaration is actually instantiating a new constructor for "Set 'a". Is this much correct? If so, I think I want to juggle some keywords, and I want to think about data fields, and we seem to need to deal with inheritance (hmm. maybe that's already covered), but I think I like the concept thus far. I do find it confusing that the declaration for ListSet does not include the 'a on the LHS, as in: object ListSet 'a :: Eq 'a => ['a] -> Set 'a Is this merely syntactic shorthand, or is there some significance in the omission? In the object specification just below it, the "l" in "object ListSet l" is certainly not of type 'a, so I do see potential for syntactic confusion if it is included. Now I get to the upper right of page two and the definition of "Eq 'a". So far as I can tell, it is a key distinction between the EqInt object and the ListSet object that the definition of EqInt does not specify a constructor, and therefore cannot be instantiated explicitly. I presume that the sense in which EqInt is "implicit" is that there is an implicit singleton instance. There is much to like here, but most notably the fact that type class instances are named. This is something I had already identified as necessary in BitC, because we need a way to control the import/export of instances across module boundaries. There is one thing that I find puzzling, though: the determination of whether a class is a type class or an object class seems to be done by the "object" declaration. In particular, given the definition of Eq 'a on page 2, it seems to me that we might define: object StrangeEqInstance z :: Eq Int where (==) = primIntEQ (x `mod` y) 0 and given this definition, it seems that StrangeEqInstance is an object constructor (admittedly a broken one, since the type of z is not inferrable)! That is: it does not seem evident from the declaration of a class whether that class is a constraint or a type. Perhaps it partakes of both, and what I am really struggling with is this quality of partaking of both. And finally a small nit, easily corrected: I see no reason why there should be only one constructor for ListSet. In the example given, it would clearly be benficial to allow ListSets to be constructed from singletons. This raises a bit of a reductio problem that has me scratching my head a bit, though it does seem like a resolvable reductio. How close am I to starting to get my head around this? shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
