[Haskell-cafe] Assorted AT fun and games
wren ng thornton
wren at freegeek.org
Sun Aug 15 20:26:26 EDT 2010
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?
More information about the Haskell-Cafe