[Haskell-cafe] Injective type families for GHC
vogt.adam at gmail.com
Tue Feb 10 22:13:57 UTC 2015
On Tue, Feb 10, 2015 at 6:38 AM, Jan Stolarek <jan.stolarek at p.lodz.pl> wrote:
>> I don't know how realistic this is but a constraint (HLength x ~
>> HLength y) would ideally have the same result as SameLength x y.
> I'm not sure if I understand that part. HLength is not injective. How would injectivity help here?
I agree it's not injective. But my impression is that injective TFs
pretty much allow ghc to replace a constraint
TF a b ~ result
(TF_getResult a b ~ result, TF_getB result a ~ b)
Where instances of:
type family TF a b | result a -> b, a b -> result -- or whatever the
notation actually is
define instances of ordinary type families TF_getB and TF_getResult.
So it's a move in the same direction to replace (HLength x ~ HLength
y) with SameLength x y. While I don't know how the code for SameLength
might be derived from the definition of HLength, that substitution
seems safe so long as (HLength x ~ HLength y) is still checked. I can
see that substitution happening in a type checker plugin, but it would
be nice if it was part of the language.
More information about the Haskell-Cafe