[Haskell-cafe] Assorted AT fun and games

[wren ng thornton]

Brandon S Allbery KF8NH wrote:
> On 8/15/10 09:00 , Andrew Coppin wrote:
>>  class (Vector (Point x)) => HasSpace x where
>>    type Point x :: *
> (...)
>> And now things get *really* interesting. Consider this:
>>
>>  data Foo x = Foo !x !(Point x)
>>
>> Surprisingly, GHC accepts this. This despite the rather obvious fact that
>> "Point x" can exist if and only if "x" has a HasSpace instance. And yet, the
>> type definition appears to say that "x" is simply an unconstrained type
>> variable. Intriguing...
> 
> Maybe I'm missing something in all the type machinery I elided, but it looks
> to me like you have that backwards:  HasSpace x requires Point x but not
> vice versa.  Your actual usage may require the reverse association, but the
> definition of Foo won't be modified by that usage --- only applications of
> that definition.


Not quite. What we're doing is defining a type function: Point. We may 
ask, then, what is the kind of Point? I don't know what the notation is 
for writing it in GHC these days, but the kind is:

     Point :: (x::*) -> HasSpace x -> *

That is, we accept a type as an argument. Let's call that argument "x". 
Then we accept a proof of HasSpace for x. This argument will be computed 
by searching for typeclass instances, where the instance itself is the 
proof. Given these two arguments, Point can return a type (namely by 
projecting it from the instance record). This is the same for any other 
method of a typeclass; we don't write the class constraint in the 
function types either, because it's implied by being in a typeclass 
definition. Ditto for the types of record selectors.

Translating this kind down to its type-level ramifications is where 
things get weird, because of how instances are implicitly discovered and 
passed around. Effectively, instances have their own function space 
distinct from (->).

In any case, it seems that the only sensible way to get a result back 
from Point is if we provide it with both a source type and a class 
instance for that type. Thus, when asking what the kind of Foo is (or 
the type of the other Foo for that matter) there should be a constraint. 
How else can we pass the correct instance to Point?

-- 
Live well,
~wren