TypeFamilies vs MultiParamTypeClasses

[snowleopard]

TypeFamilies vs MultiParamTypeClasses

[snowleopard]

There are good discussions on TF vs MPTC+FD in the "Associated Type Synonyms" paper:

https://www.microsoft.com/en-us/research/wp-content/uploads/2005/01/at-syns.pdf

and here: https://ghc.haskell.org/trac/ghc/wiki/TFvsFD

However, most arguments (e.g. expressivity) appear to be non-applicable to our simple case.

[snowleopard]

@ndmitchell has written a draft implementation with MPTC here: https://gist.github.com/ndmitchell/800fb7bf65f5875a22e72b1b868e1442

There is no functional dependency | g -> a which I have in the above snippet, which makes me wonder if it's really necessary (I think it seemed to be in my experiments).

[ndmitchell]

Note that g is higher kinded. If g had been * kind then you would need the FD. As it is, often g gives you the restriction automatically. Having | g -> a with the higher-kind would be a bad idea, since it rules out lots of useful instances.

[snowleopard]

Ah, I see!

So it is possible to have a higher-kinded g and define not fully-parametric Graph instances... we probably still lose some instances though, for example, IntAdjacencyMap or ()... not that the latter is very useful :-) But the former probably is.

Thanks! This is an interesting design point I haven't considered.

[ndmitchell]

You don't really lose any instances since you can have a new type with a phantom parameter. You certainly make those ones a bit harder to use though - but they are pretty rare so no big deal.

[snowleopard]

Good point.

So, let's summarise the pros and cons of TF and your higher-kinded version of MPTC.

Some examples of type signatures:

ab :: (Graph g, Vertex g ~ Char) => g
ab :: Graph g Char => g Char
ab = connect (vertex 'a') (vertex 'b')

overlays :: Graph g => [g] -> g
overlays :: Graph g a => [g a] -> g a

edges :: Graph g => [(Vertex g, Vertex g)] -> g
edges :: Graph g a => [(a, a)] -> g a

path :: Graph g => [Vertex g] -> g
path :: Graph g a => [a] -> g a

gmap :: Graph g => (a -> Vertex g) -> GraphFunctor a -> g
gmap :: Graph g b => (a -> b) -> GraphFunctor a -> g b

box :: (Graph g, Vertex g ~ (u, v)) => GraphFunctor u -> GraphFunctor v -> g
box :: Graph g (u, v) => GraphFunctor u -> GraphFunctor v -> g (u, v)

I'd say there is no clear winner here. MPTC signatures are usually a bit shorter, but TF may be easier to parse since Vertex g is quite readable/self-documentary. My weak vote goes to TF.

Dealing with non-fully parametric instances may require workarounds with MPTC. Here TF win.

Any other points to consider?

[ndmitchell]

MPTC is a much older, simpler and more common extension than TF. I suspect you are less likely to have type inference problems in corner cases, especially when composing things.

I find the MPTC much simpler to read than TF. Yes, Vertex isn't explicit, but as soon as you define more complex operations it is easier to keep track of. As examples of things mentioning more than one graph/vertex type:

replaceGraph :: (Graph g1, Graph g2, Vertex g1 ~ a, Vertex g2 ~ a) => g1 -> g2
replaceVertex :: (Graph g1, Graph g2, Vertex g1 ~ a, Vertex g2 ~ b) => g1 -> g2

replaceGraph :: (Graph g1 a, Graph g2 a) => g1 a -> g2 a
replaceVertex :: (Graph g a, Graph g b) => g a -> g b

What issues were you expecting with non-fully parametric instances?

[snowleopard]

As examples of things mentioning more than one graph/vertex type:

Indeed, these are good examples where MPTC is clearer.

What issues were you expecting with non-fully parametric instances?

Well, as discussed above, you can't make IntAdjacencyMap and () an instance without workarounds.

P.S.: Just to show why I care about strange things like () having a Graph instance -- in some cases () acts as the identity on graph operations, particularly various products:

-- Below ~~ stands for the equality up to an isomorphism, e.g. (x, ()) ~~ x
box x y         ~~ box y x
box x (box y z) ~~ box (box x y) z
box x ()        ~~ x
box x empty     ~~ empty -- i.e. empty is annihilating zero for the box operation!

[snowleopard]

Hmm, the following ConstraintKinds hack seems to work:

{-# LANGUAGE ConstraintKinds #-}

type Graphable g a = (Graph g, Vertex g ~ a)

edges :: Graphable g a => [(a, a)] -> g

Here g is not higher-kinded because the underlying type class isn't.

With this approach we can have both TF and MPTC like type signatures.

We can define Graphable g a in Algebra.Graph.Classes, or let users of the library define it themselves, which saves us from the struggle of finding a good name for this constraint synonym. (Not sure about the name Graphable, just reusing @ndmitchell's name.)

[ndmitchell]

You still don't get MPTC like type signatures - you get a simpler context in the examples above, but the signature itself is still clearer with MPTC (the bit changing is clearer).

For things like () you can make Const () instead and it behaves the same. It's definitely not as clear as TF though.

[snowleopard]

@ndmitchell Have a look at #9 -- higher-kinded class MonadPlus g => Graph g clearly gives us best type signatures, which can be used when working with Data.Graph and other fully parametric graph representations.

Furthermore, I just realised that we can make Relation an instance of higher-kinded graphs by postponing the actual evaluation which requires Ord a until we actually need it, say, to implement the Eq instance. This essentially means that we can turn pretty much all data structures into higher-kinded equivalents by hiding Data.Graph inside, which is used to build up fully parametric trees, and then at some collapsing these trees into more efficient representations. This collapsing will require various constraints like Ord a, but it doesn't have to be at the Graph instance declaration.

[snowleopard]

I think the solution we currently have is optimal: Algebra.Graph.Class defines a kind-* class, which is most general, and Algebra.Graph.HigherKinded.Class defines higher-kinded graphs with nice type signatures.

Users who don't care about type classes can happily use Algebra.Graph with nicest possible (monomorphic) type signatures.