[Haskell-cafe] Equality constraints in type families
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Tue Mar 25 20:57:22 EDT 2008
Simon Peyton-Jones:
> | | However, I think I now understand what you are worried about.
> It is the
> | | interaction of type families and GHC's generalised type synonyms
> (i.e.,
> | | type synonyms that may be partially applied). I agree that it
> does lead
> | | to an odd interaction, because the outcome may depend on the
> order in
> | | which the type checker performs various operations. In
> particular,
> | | whether it first applies a type instance declaration to reduce a
> type
> | | family application or whether it first performs decomposition.
> |
> | yes, indeed, thanks! that was the central point of example one.
>
> Aha.
>
> Just to clarify, then, GHC's 'generalised type synonyms' behave like
> this.
>
> * H98 says that programmer-written types must obey certain
> constraints:
> - type synonym applications saturated
> - arguments of type applications are monotypes (apart from ->)
>
> * GHC says that these constraints must be obeyed only
> *after* the programmer-written type has been normalised
> by expanding saturated type synonyms
>
> http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#type-synonyms
>
> I regard this as a kind of pre-pass, before serious type checking
> takes place, so I don't think it should interact with type checking
> at all.
>
> I don't think this normalisation should include type families,
> although H98 type synonyms are a kind of degenerate case of type
> families.
>
> Would that design resolve this particular issue?
Not quite, but it refines my proposal of requiring that type synonyms
in the rhs of type instances need to be saturated. Let me elaborate.
The current implementation is wrong, as it permits
type S a b = a
type family F a :: * -> *
type instance F a = S a
Why do we need to forbid this type instance? Because it breaks the
confluence of equality constraint normalisation. Here are two
diverging normalisations:
(1)
F Int Bool ~ F Int Char
==> DECOMP
F Int ~ F Int, Bool ~ Char
==> FAIL
(2)
F Int Bool ~ F Int Char
==> TOP
S Int Bool ~ S Int Char
==> (expand type synonym)
Int ~ Int
==> TRIVIAL
However, here is a (somewhat silly) program that does have partially
applied type synonyms in a type instances' rhs and that is perfectly ok:
type S a b = a
type family F (a :: * -> *) b :: * -> *
type instance F a b = S (S a) b b
This is ok, because we can expand the type synonyms in the rhs of the
type instance
S (S a) b b = S a b = a
and get a valid type.
So, the crucial point is that, as you wrote,
> I don't think this normalisation should include type families,
> although H98 type synonyms are a kind of degenerate case of type
> families.
The only way to stratify the normalisation of type synonyms and type
families such that all type synonyms are expanded before any family
applications are normalised is by requiring that after normalising the
rhs of a type instance declaration *by itself*, we get a type that
only contains saturated applications of type synonyms. (As Claus
wrote, this is after all what we do for class instance heads.)
Manuel
More information about the Haskell-Cafe
mailing list