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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
