[Haskell-cafe] Assorted AT fun and games

[Ivan Lazar Miljenovic]

Andrew Coppin <andrewcoppin at btinternet.com> writes:

> 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 at gmail.com
IvanMiljenovic.wordpress.com