It all began with class (Vector (Point x)) => HasSpace x where type Point x :: * So far, so good. I was rather surprised that you _can_ write class (Complete (Completed x)) => Incomplete x where type Completed x :: * complete :: x -> Completed x I was almost as surprised to discover that you _cannot_ write class (HasSpace x, Complete (Completed x), HasSpace (Completed x), Point x ~ Point (Completed x)) => Incomplete where... It just means that every time you write an Incomplete instance, you might have to add the Point constraint manually. Which is mildly irritating. More worrying, adding Point foo ~ Point bar to an instance declaration causes GHC to demand that you turn on Undecidable Instances, for reasons beyond my comprehension. It's also interesting that when you write a class instance that has some constraint on it, and then you try to write a subclass instance, you still have to repeat the exact same constraint, even though the superclass instance declaration implies it. The only reason I can think of is that theoretically somebody could add a new superclass instance without the constraint. (Wouldn't that be an overlapping instance though?) 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... Next, you can't derive Eq or Show for this type, but you *can* declare them manually: instance (Show x, Show (Point x)) => Show (Foo x) where show (Foo x px) = "Foo (" ++ show x ++ ") (" ++ show px ++ ")" Again, no hint of the fact that this will only work if we have HasSpace x. And yet GHC happily accepts this. I'm starting to think maybe I'm pushing the type system further than it can cope, and I should just completely redesign the whole thing...
Andrew Coppin
It all began with
class (Vector (Point x)) => HasSpace x where type Point x :: *
So far, so good.
I was rather surprised that you _can_ write
class (Complete (Completed x)) => Incomplete x where type Completed x :: * complete :: x -> Completed x
I was almost as surprised to discover that you _cannot_ write
class (HasSpace x, Complete (Completed x), HasSpace (Completed x), Point x ~ Point (Completed x)) => Incomplete where...
It just means that every time you write an Incomplete instance, you might have to add the Point constraint manually. Which is mildly irritating.
Yeah... have to wait until at least 6.16 by all accounts :(
More worrying, adding Point foo ~ Point bar to an instance declaration causes GHC to demand that you turn on Undecidable Instances, for reasons beyond my comprehension.
Because the type-checker isn't smart enough to figure this out itself. And if you think yours is bad... (code taken from the new FGL): ,---- | class (InductiveGraph (g n e)) => MappableGraph g n e where | | gmap :: (InductiveGraph (g n' e')) => (Context (g n e) -> Context (g n' e')) | -> g n e -> g n' e' | gmap f = fromContexts . map f . toContexts | | nmap :: ( InductiveGraph (g n' e) | , Node (g n e) ~ Node (g n' e) | , EdgeLabel (g n e) ~ EdgeLabel (g n' e)) | => (NodeLabel (g n e) -> NodeLabel (g n' e)) | -> g n e -> g n' e | nmap f = gmap f' | where | f' (Context ei n l eo) = Context ei n (f l) eo | | emap :: ( InductiveGraph (g n e') | , Node (g n e) ~ Node (g n e') | , NodeLabel (g n e) ~ NodeLabel (g n e')) | => (EdgeLabel (g n e) -> EdgeLabel (g n e')) | -> g n e -> g n e' | emap f = gmap f' | where | f' (Context ei n l eo) = Context (applyF ei) n l (applyF eo) | applyF = map (second f) `---- Since we can't apply constraints in the type-class, we have to apply them in the methods :s
It's also interesting that when you write a class instance that has some constraint on it, and then you try to write a subclass instance, you still have to repeat the exact same constraint, even though the superclass instance declaration implies it. The only reason I can think of is that theoretically somebody could add a new superclass instance without the constraint. (Wouldn't that be an overlapping instance though?)
What do you mean? If it's what I think you mean, it's nothing specific to type families: ,---- | instance Eq a => Eq (Set a) where | t1 == t2 = (size t1 == size t2) && (toAscList t1 == toAscList t2) | | instance Ord a => Ord (Set a) where | compare s1 s2 = compare (toAscList s1) (toAscList s2) `---- We have to specifically state that a is ordered even though Ord is a sub-class of Eq...
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...
Yeah, I'm not sure if I like or don't like this behaviour. It's good from the "we shouldn't put class constraints in data types" perspective, but bad from the "wtf does that even mean for non-instances?" perspective.
Next, you can't derive Eq or Show for this type, but you *can* declare them manually:
instance (Show x, Show (Point x)) => Show (Foo x) where show (Foo x px) = "Foo (" ++ show x ++ ") (" ++ show px ++ ")"
Yes, this slightly annoys me as well; Show is easy, Read is more annoying. I've resorted to specifying a non-TF version and then using derive to work out what the instance should looks like and then tweaking it myself.
Again, no hint of the fact that this will only work if we have HasSpace x. And yet GHC happily accepts this.
I'm guessing it's implied somehow... but yeah :s
I'm starting to think maybe I'm pushing the type system further than it can cope, and I should just completely redesign the whole thing...
Nah, push it as far as you can: * We need people to push it and find weird things like this to see what is weird and what can be fixed. * It will save you from converting it back down the track when type families take over the world... ;-) -- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com IvanMiljenovic.wordpress.com
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 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. - -- brandon s. allbery [linux,solaris,freebsd,perl] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkxoFikACgkQIn7hlCsL25VIJgCbB/3zqsATPssYNFsCD/H5fMOO DnUAn2+gBqlHyD0FyGFANSyVxWdI0PQR =/SmY -----END PGP SIGNATURE-----
Brandon S Allbery KF8NH wrote:
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
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.
Well, since Point is part of the definition of HasSpace, and therefore Point x is defined only if an instance HasSpace x exists. I'm not sure how that's "Point x doesn't require HasSpace x".
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
participants (4)
-
Andrew Coppin -
Brandon S Allbery KF8NH -
Ivan Lazar Miljenovic -
wren ng thornton