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