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