Difference between revisions of "GHC/SuperClass"
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> |
||
+ | |||
+ | |||
⚫ | |||
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.