[TYPES] A show-stopping problem for modular type classes?

[Brian Hulley]

Karl Crary wrote:
> 
> Brian Hulley wrote:
>> Thanks for pointing out that the compiler could just reject this 
>> clause: perhaps this would be an acceptable penalty to pay for the 
>> advantages of having scoped instances. However there are situations 
>> where it would not be so clear what the compiler should do eg:
>>
>>    bar :: forall a. G a -> (a, Int)
>>    bar (Problem x) = (x + x, 1 + 2)
>>    bar (Ok _)      = ((), 0)
> 
> 1.
> As Derek correctly pointed out, this works fine.  In the "Problem" case, 
> "a" is an abstract type that has in instance of Num.  The addition for x 
> is resolved using the instance for "a", and other addition is resolved 
> using the instance for Int.
> 
> I wonder if you're forgetting that overloading is resolved statically?  
> The type "a" is abstract, and it has a unique instance for Num.  The 
> possibility that "a" might ultimately be instantiated with Int is 
> irrelevant.  So one solution to your problem is to treat the unpacking 
> of a GADT arm associated with an instance as a using declaration, with 
> the usual test for overlapping instances

Following on from my reply to Derek I think the problem is that I didn't explain enough what I meant by giving that example. I can see that there exists a way to formalize a type system such that the above example is acceptable, and as you and Derek have pointed out, MTC is one such system, but from the point of view of the design space of *a* modular type system following the general discussion at the beginning of the paper, not just the particular detailed design and formalization that was chosen, it isn't clear to me that the above is the only internally consistent way of looking at things, and therefore there is a corner of the design space that could perhaps be illuminated further.

For example you say that (a) is an abstract type. But I could argue that (a) is actually a placeholder that represents any particular concrete type, and that the function definition above should be understood as representing a template for an infinite number of monomorphic functions, one of which will accept the argument type (G Int).

This might seem like a really obtuse interpretation, but it would seem to match the natural expectation of behaviour if the programmer expects functions to be inlined at the call site wherever possible.

Anyway I understand it is not a problem for MTC as presented in the paper - I'm just being a devil's advocate to try and make sure no stone is left unturned ;-)

> 
> 
> 2.
> I didn't know that Haskell allows GADTs to be built over kinds other 
> than Type (aka *).  That's nice.  What I was suggesting went beyond 
> that.  My suggestion is that the index to a GADT, even when it happens 
> to be a type, should not be associated with an instance.  Under such a 
> design, this problem would simply go away.

This is also what I thought you meant, though if people are used to refining types (of whatever kind) by giving type class constraints, it is possible that someone doing some very advanced programming would find the restriction irksome and in that sense the idea that the problem would go away might be brought into a homology with the idea that the Gordian Knot was solved when Alexander cut through it.

> 
> 
> 3.
> I'm surprised to hear that the GHC internals now support type 
> abstraction, in the sense of indefinite references.  Am I understanding 
> you correctly? Not so long ago I was told that implementing functors in 
> GHC would be a non-starter.
> 

I'm not an expert on GHC internals. The only reference I can think of about implementing functors in GHC is [1], and of course Oleg's related post on the Haskell mailing list where he shows how to implement an applicative translucent functor using typeclasses [2].

Cheers, Brian.

[1] "Higher-order modules in system Fw and Haskell" by Chung-chieh Shan, Harvard University. (2004 ?)

[2] Post to Haskell mailing list with title "Applicative translucent functors in Haskell" by oleg at pobox.com, Fri Aug 27 19:51:43 EDT 2004