Heterogeneous equality into base?

[Oleg Grenrus]

Adam Chipala's CPDT book has a good chapter,
http://adam.chlipala.net/cpdt/html/Equality.html

It talks about Axiom K, and Jonh Mayor equality

- Oleg

On 18.07.2017 14:25, Artyom wrote:
>> In a more general type theory, HRefl doesn't imply Refl! You can't
> show HRefl implies Refl in MLTT. This extra power is granted by
> dependent pattern matching most dependent type theories or in Haskell by
> the way we implement ~. In Haskell, today, it works out because we have
> "uniqueness of identity proofs" or "axiom K".
>
> What does it mean that HRefl doesn't imply Refl? I tried to google Axiom
> K but quickly got lost :(
>
> I naively thought that HRefl is just Refl but without the “kinds have to
> be equal or else GHC will bark” restriction. Is there some situation (in
> current Haskell or some variant of Haskell) where we can have HRefl for
> a pair of types but not Refl?
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170718/0f957b72/attachment.sig>