[Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
Anthony Clayden
anthony_clayden at clear.net.nz
Sun May 14 09:51:51 UTC 2017
> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote:
>
> ... [in] closed type families. (We
> would also have to eliminate non-linear patterns,
> replacing them with some other first-class test for
> equality.
> AntC's proposed disequality constraints then become
> straightforward pattern guards.
Guards don't have to be just disequalities.
If you want to eliminate non-linear patterns,
use _equality_ guards. Full example:
> type family F a b where
> F a a = a
> F Int b = b
> F a Bool = a
>
Translates to:
> type instance F a b | a ~ b = a
> type instance F a b | a ~ Int, a /~ b = b
> type instance F a b | b ~ Bool, a /~ Int, a /~ b = a
(Each instance after the first
has disequality guards to negate the earlier instances'
equalities., i.e. the earlier instances 'shadow' the
overlap.)
> It's currently unclear to me how to do this
> right. ...
>
Assuming we have a primitive type-level
equality test (?~), returning type-level Bool;
we can use helper functions.
The first instance desugars to a call
> ... = F_a_b_Eq (a ?~ b) a b
> type instance F_a_b_Eq True a b = a
(Needs UndecidableInstances.)
> Section 5.13.2 of my thesis dwells on this, without
> much in the way of a concrete way forward.)
We use type equality testing all the time.
In fact instance selection relies on it.
5.13.2 says: "they [equality testing rules] cannot handle
the case where Equals a a reduces to True,
where a is locally bound type variable."
?? I thought GHC's equality test
requires types to be grounded,
i.e. not merely type vars,
in order to be judged equal.
Or did that change recently?
Isn't that to do with impredicativity
and the dreaded monomorphism:
the same typevar might get a different
forall-qualified type in different use sites.
Contrast types can be judged dis-equal
without necessarily being grounded.
[HList paper section 9 refers.]
AntC
More information about the Haskell-Cafe
mailing list