Hi libraries@, My 2 cents inlined below :) ~~julm Le jeu. 06 juil. 2017 à 17:15:36 -0400, David Menendez a écrit :
Do you have any code examples that use heterogeneous equality? In the past, GHC has been less flexible with kind variables than with type variables, so I’m not sure what this would enable. I have been using (:~~:) to return two proofs when two type-indexed runtime representations of types are equal: one proof for the equality of kinds, and another proof for the equality of types. For instance, this can be seen in eqVarKi, eqConstKi, and eqTypeKi in https://hackage.haskell.org/package/symantic-6.3.0.20170703/
It's also done here: https://ghc.haskell.org/trac/ghc/wiki/Typeable#Step4:Decomposingarbitrarytyp... Le ven. 07 juil. 2017 à 00:47:50 +0300, Wolfgang Jeltsch a écrit :
I also think that creating a new module Data.Type.Equality.Heterogeneous is the way to go. I would call the constructor of (:~~:) Refl, not HRefl. If you need to distinguish between the Refl of (:~:) and the Refl of (:~~:), you can qualify the name using the module system.
I think it is generally better to use the module system for qualifying names than putting the qualification into the identifiers like in “HRefl”. The module system is made to express qualification. On the other hand, qualification in identifiers is typically done with single letters to save space, which is not very descriptive and quickly results in ambiguities (for example, “m” means “monoid” in “mappend”, but “monad” in “mplus”).
By myself I came up with the name KRefl, but changed it to HRefl to reduce cognitive efforts, when I discovered Richard's thesis which is introducing it. http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf I'm using both Refl and HRefl in the same package, so I prefer to name the latter HRefl instead of H.Refl, to keep a flat namespace which allows open imports and re-exports in parent modules. This also makes grep-ing/web-searching easier, and Haddock generated docs more readable (because there the module paths are hidden). https://www.reddit.com/r/haskell/comments/6j2t1o/on_naming_things_library_de... This said, some of these concerns may not apply to base. Cheers :]