FWIW, I agree with Andrew Martin on this one. On Jul 8, 2017 9:26 PM, "Andrew Martin" wrote:

Just wanted to weigh in with my two cents. I also prefer to use the module system for the most part rather than prefixing function names with something that indicates the data type they operate on. However, when it comes to types, I would much rather they have different names. I like that the data constructor of :~~: is HRefl. However, for the functions sym, trans, etc., I would rather have a Data.Type.Equality.Hetero that exports all of these without any kind of prefixes on them. Then there's the question of where we export :~~: from. It could be exported only from the Hetero module, or it could be exported from both.

Sent from my iPhone

...

On Jul 8, 2017, at 7:56 PM, Wolfgang Jeltsch wrote:

Hi!

Unfortunately, my wish has not been granted, as I wanted the data constructor of (:~~:) to be named Refl and (:~~:) to be defined in a separate module. I see that there are no heterogeneous versions of sym, trans, and so on in base at the moment. If they will be available at some time, how will they be called? Will they be named hsym, htrans, and so on? This would be awful, in my opinion.

In Haskell, we have the module system for qualification. I very well understand the issues Julien Moutinho pointed out. For example, you cannot have a module that just reexports all the functions from Data.Sequence and Data.Map, because you would get name clashes.

However, I think that the solution to these kinds of problems is to fix the module system. An idea would be to allow for exporting qualified names. Then a module could import Data.Sequence and Data.Map qualified as Seq and Map, respectively, and export Seq.empty, Map.empty, and so on.

If we try to work around those issues with the module system by putting qualification into the actual identifiers in the form of single letters (like in mappend, HRef, and so on), we will be stuck with this workaround forever, even if the module system will be changed at some time, because identifiers in core libraries are typically not changed. Just imagine, we would have followed this practice for the containers package. We would have identifiers like “smap”, “munion”, “imintersection”, and so on.

All the best, Wolfgang

Am Freitag, den 07.07.2017, 08:15 -0700 schrieb Ryan Scott:

...

Sorry for only just discovering this thread now. A lot of this discussion is in fact moot, since (:~~:) already is in base! Specifically, it's landing in Data.Type.Equality [1] in the next version of base (bundled with GHC 8.2). Moreover, it's constructor is named HRefl, so your wish has been granted ;)

As for why it's being introduced in base, it ended up being useful for the new Type-indexed Typeable that's also landing in GHC 8.2. In particular, the eqTypeRep function [2] must return heterogeneous equality (:~~:), not homogeneous equality (:~:), since it's possible that you'll compare two TypeReps with different kinds.

Ryan S. ----- [1] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718 d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37 [2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718 d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>

---

Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

---

Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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?

Hi! I agree with you, Andrew, that types should have different names. However, (H)Refl is not a type. It is a data constructor; so it is a special kind of value and as such very similar to sym, trans, and friends. The similarity of Refl to the ordinary functions of the Heterogeneous module becomes even more obvious when considering that Refl is a proof, like sym, trans, and so on. All the best, Wolfgang Am Samstag, den 08.07.2017, 21:25 -0400 schrieb Andrew Martin:

Just wanted to weigh in with my two cents. I also prefer to use the module system for the most part rather than prefixing function names with something that indicates the data type they operate on. However, when it comes to types, I would much rather they have different names. I like that the data constructor of :~~: is HRefl. However, for the functions sym, trans, etc., I would rather have a Data.Type.Equality.Hetero that exports all of these without any kind of prefixes on them. Then there's the question of where we export :~~: from. It could be exported only from the Hetero module, or it could be exported from both.

Sent from my iPhone

...

On Jul 8, 2017, at 7:56 PM, Wolfgang Jeltsch wrote:

Hi!

Unfortunately, my wish has not been granted, as I wanted the data constructor of (:~~:) to be named Refl and (:~~:) to be defined in a separate module. I see that there are no heterogeneous versions of sym, trans, and so on in base at the moment. If they will be available at some time, how will they be called? Will they be named hsym, htrans, and so on? This would be awful, in my opinion.

In Haskell, we have the module system for qualification. I very well understand the issues Julien Moutinho pointed out. For example, you cannot have a module that just reexports all the functions from Data.Sequence and Data.Map, because you would get name clashes.

However, I think that the solution to these kinds of problems is to fix the module system. An idea would be to allow for exporting qualified names. Then a module could import Data.Sequence and Data.Map qualified as Seq and Map, respectively, and export Seq.empty, Map.empty, and so on. 

If we try to work around those issues with the module system by putting qualification into the actual identifiers in the form of single letters (like in mappend, HRef, and so on), we will be stuck with this workaround forever, even if the module system will be changed at some time, because identifiers in core libraries are typically not changed. Just imagine, we would have followed this practice for the containers package. We would have identifiers like “smap”, “munion”, “imintersection”, and so on.

All the best, Wolfgang

Am Freitag, den 07.07.2017, 08:15 -0700 schrieb Ryan Scott:

...

Sorry for only just discovering this thread now. A lot of this discussion is in fact moot, since (:~~:) already is in base! Specifically, it's landing in Data.Type.Equality [1] in the next version of base (bundled with GHC 8.2). Moreover, it's constructor is named HRefl, so your wish has been granted ;)

As for why it's being introduced in base, it ended up being useful for the new Type-indexed Typeable that's also landing in GHC 8.2. In particular, the eqTypeRep function [2] must return heterogeneous equality (:~~:), not homogeneous equality (:~:), since it's possible that you'll compare two TypeReps with different kinds.

Ryan S. ----- [1] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5 f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37 [2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5 f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>; 

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

I for one favor the HRefl constructor name for practical reasons. These types will commonly be used in similar scopes. Also, there is a theoretical quibble for why this shouldn't just replace :~: directly in any code that would otherwise use both and why both will be used in much the same code going forward: 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. -Edward Sent from my iPad

On Jul 9, 2017, at 5:35 PM, Oleg Grenrus wrote:

It's not only a value, it's also a pattern. We have PatternSynonyms, but IMHO it's not a strong argument for having constructors with a same name.

- Oleg

Sent from my iPhone

...

On 9 Jul 2017, at 22.47, Wolfgang Jeltsch wrote:

Hi!

I agree with you, Andrew, that types should have different names. However, (H)Refl is not a type. It is a data constructor; so it is a special kind of value and as such very similar to sym, trans, and friends. The similarity of Refl to the ordinary functions of the Heterogeneous module becomes even more obvious when considering that Refl is a proof, like sym, trans, and so on.

All the best, Wolfgang

Am Samstag, den 08.07.2017, 21:25 -0400 schrieb Andrew Martin:

...

Just wanted to weigh in with my two cents. I also prefer to use the module system for the most part rather than prefixing function names with something that indicates the data type they operate on. However, when it comes to types, I would much rather they have different names. I like that the data constructor of :~~: is HRefl. However, for the functions sym, trans, etc., I would rather have a Data.Type.Equality.Hetero that exports all of these without any kind of prefixes on them. Then there's the question of where we export :~~: from. It could be exported only from the Hetero module, or it could be exported from both.

Sent from my iPhone

...

On Jul 8, 2017, at 7:56 PM, Wolfgang Jeltsch wrote:

Hi!

Unfortunately, my wish has not been granted, as I wanted the data constructor of (:~~:) to be named Refl and (:~~:) to be defined in a separate module. I see that there are no heterogeneous versions of sym, trans, and so on in base at the moment. If they will be available at some time, how will they be called? Will they be named hsym, htrans, and so on? This would be awful, in my opinion.

In Haskell, we have the module system for qualification. I very well understand the issues Julien Moutinho pointed out. For example, you cannot have a module that just reexports all the functions from Data.Sequence and Data.Map, because you would get name clashes.

However, I think that the solution to these kinds of problems is to fix the module system. An idea would be to allow for exporting qualified names. Then a module could import Data.Sequence and Data.Map qualified as Seq and Map, respectively, and export Seq.empty, Map.empty, and so on.

If we try to work around those issues with the module system by putting qualification into the actual identifiers in the form of single letters (like in mappend, HRef, and so on), we will be stuck with this workaround forever, even if the module system will be changed at some time, because identifiers in core libraries are typically not changed. Just imagine, we would have followed this practice for the containers package. We would have identifiers like “smap”, “munion”, “imintersection”, and so on.

All the best, Wolfgang

Am Freitag, den 07.07.2017, 08:15 -0700 schrieb Ryan Scott:

...

Sorry for only just discovering this thread now. A lot of this discussion is in fact moot, since (:~~:) already is in base! Specifically, it's landing in Data.Type.Equality [1] in the next version of base (bundled with GHC 8.2). Moreover, it's constructor is named HRefl, so your wish has been granted ;)

As for why it's being introduced in base, it ended up being useful for the new Type-indexed Typeable that's also landing in GHC 8.2. In particular, the eqTypeRep function [2] must return heterogeneous equality (:~~:), not homogeneous equality (:~:), since it's possible that you'll compare two TypeReps with different kinds.

Ryan S. ----- [1] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5 f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37 [2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5 f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>;

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

---

Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

---

Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

I definitely agree that it'd be difficult if not near impossible to fully root out, even if we did decide it was worth the pain, which is very much up for debate. Sent from my iPad

On Jul 10, 2017, at 8:58 AM, Richard Eisenberg wrote:

...

On Jul 9, 2017, at 8:31 PM, Edward Kmett 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