Heterogeneous equality into base?

[Richard Eisenberg]

> On Jul 9, 2017, at 8:31 PM, Edward Kmett <ekmett at gmail.com> wrote:
> 
> Heterogenous equality is a form of what Conor McBride calls "John Major" equality. 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". This means that anything going on in the world of homotopy type theory today can't be used in Haskell directly as univalence and axiom k are inconsistent. 
> 
> Some work has been put into pattern matching in Agda without axiom K. Do I expect that folks are going to run out and implement it in Haskell? No, but in general I want to be very clear in my code when I rely upon this extra power that Haskell grants us kinda by accident or fiat today as those results don't transfer, and could be dangerous to assume if we decide to go in a different direction in the far flung future.

This is all true, of course, but you'd be hard-pressed to detect or avoid all uses of Axiom K in Haskell. Note that (:~~:) is a perfectly ordinary GADT, and you (or a dependency of yours) might define a similar GADT that implicitly uses Axiom K when compared with MLTT.

Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170710/181603f2/attachment.html>