GHC/SuperClass: Difference between revisions
m (add example from the ghc-users thread) |
(add further material from the original ghc-users thread) |
||
Line 1: | Line 1: | ||
[in draft May 2017] | [in draft May 2017] | ||
This page brings together several techniques using ''SuperClass'' Constraints. That is, Constraints delared in the context of a class. | |||
== Expressive Power of SuperClass Constraints == | |||
Superclass constraints are not subject to the Paterson conditions[https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instance-termination]. | |||
That is, superclass constraints can be written that are not permitted as instance constraints. | |||
* (Superclass constraints are required to be non-cyclic, which ensures they're terminating.) | |||
These constraints are valid SuperClass, but not per Instance: | |||
<Haskell> | |||
class (F a b ~ b) => C a b ... | |||
-- equivalently | |||
class (D a b b) => C a b ... | |||
</Haskell> | |||
Sometimes even though you have a type function, you can use knowledge of the result to 'improve' the parameters -- that is, a limited form of injectivity. | |||
* The classic case is adding type-level Naturals. | |||
* Maybe even type-level Boolean And: | |||
** if the result is True, so must be the params. | |||
** if the result is False,<br>and you know one param is True,<br>the other must be False. | |||
** but that can't be a function, because<br>if the result is False<br>and you know one param is False,<br>that tells nothing about the other param. | |||
<Haskell> | |||
</Haskell> | |||
== Functional dependency-like behaviour through superclass constraints == | |||
There's an idiom that's briefly mentioned in the User Guide under Equality constraints [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#equality-constraints], but is more general and more powerful. | There's an idiom that's briefly mentioned in the User Guide under Equality constraints [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#equality-constraints], but is more general and more powerful. | ||
Line 24: | Line 55: | ||
=== Formal Description === | |||
== | |||
Constraints in the class context can achieve the effect of Functional dependencies even without the explicit vertical bar and dependency arrow syntax in the class declaration. Either: | Constraints in the class context can achieve the effect of Functional dependencies even without the explicit vertical bar and dependency arrow syntax in the class declaration. Either: |
Revision as of 23:50, 30 May 2017
[in draft May 2017]
This page brings together several techniques using SuperClass Constraints. That is, Constraints delared in the context of a class.
Expressive Power of SuperClass Constraints
Superclass constraints are not subject to the Paterson conditions[1]. That is, superclass constraints can be written that are not permitted as instance constraints.
- (Superclass constraints are required to be non-cyclic, which ensures they're terminating.)
These constraints are valid SuperClass, but not per Instance:
class (F a b ~ b) => C a b ...
-- equivalently
class (D a b b) => C a b ...
Sometimes even though you have a type function, you can use knowledge of the result to 'improve' the parameters -- that is, a limited form of injectivity.
- The classic case is adding type-level Naturals.
- Maybe even type-level Boolean And:
- if the result is True, so must be the params.
- if the result is False,
and you know one param is True,
the other must be False. - but that can't be a function, because
if the result is False
and you know one param is False,
that tells nothing about the other param.
Functional dependency-like behaviour through superclass constraints
There's an idiom that's briefly mentioned in the User Guide under Equality constraints [2], but is more general and more powerful.
You get the power from a combination of extensions:
- -XMultiParamTypeClasses [3]
- Superclass constraints, which can also be MultiParam [4]
- -XFunctionalDependencies [5]
- and/or superclass Equality constraints with Type families, having the effect of FunDeps [6]
- The overall effect can satisfy the FunDep Coverage conditions, which means you might not need -XUndecidableInstances [7]
The User Guide [8] says:
Equality constraints can also appear in class and instance contexts. The former enable a simple translation of programs using functional dependencies into programs using family synonyms instead.
That's not wrong; but by talking about "class and instance contexts" in the same breath does fail to emphasise that:
- whereas Instance constraints don't apply until after the instance has been selected
(And it's a common newbie mistake to think they restrict the selection.) - superclass constraints apply during type improvement before selecting instances
as described here [9] "superclass context is critical ..." [thanks @DFeuer] - This behaviour means that even if you don't explicitly put a FunDep
| ... -> ...
on a class:- If you put a superclass equality constraint on a class, that induces a FunDep as explained in [10];
but just as much - If you put a superclass class constraint on a class, and that superclass has a FunDep, that also induces a FunDep.
- and so on for a superclass constraint of a superclass constraint of a superclass constraint ....
- If you put a superclass equality constraint on a class, that induces a FunDep as explained in [10];
Formal Description
Constraints in the class context can achieve the effect of Functional dependencies even without the explicit vertical bar and dependency arrow syntax in the class declaration. Either:
- Using an Equality constraint to a Type family [11]; or
- A superclass constraint that does have an explicit Functional dependency.
- Or a superclass constraint which is itself constrained in one of those ways.
A class declaration of the form
class C a b | a -> b
can equivalently be given as
class (F a ~ b) => C a b where
type F a
That is, we represent every functional dependency (FD) a1 .. an -> b
by an FD type family F a1 .. an
and a superclass context equality F a1 .. an ~ b
, essentially giving a name to the functional dependency. [See [12]; using (~)
needs -XTypeFamilies or -XGADTs.] In class instances, we define the type instances of FD families in accordance with the class head.
Or class C
can equivalently be given as
class (D a b) => C a b ...
class D a b | a -> b
-- or
class (G a ~ b) => D a b where
type G a
The class instances for D
will closely follow those for C
. So there is not much gain in expressivity. Consider also:
class (D a c) => E a b c ...
-- class D as above
for which the D
instances will be more compact than E
.
Note that D
might not declare any methods, but merely be used for type improvement.
Method signatures for class C
are not affected by either of these ways for achieving dependencies.
Here's a fancier example of a pseudo-FunDep, reference this thread: [13].
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies,
FlexibleInstances #-}
type family F a
class (F a ~ (b, c) ) => C a b c where -- (b, c) !!
f1 :: a -> b
f2 :: a -> c
-- Uses of `f1` happily improve the type for `b`.
-- Uses of `f2` happily improve the type for `c`.
Is this power made clear in the theoretical literature? It's kinda implicit in the TypeFamilies2008 [14] paper; but note that was written concurrently with Type Families development; and published before the work was completed. Specifically, supporting Type Families and (~)
in superclass constraints was delivered a long time after the rest of the work.