Heterogeneous equality into base?

[Julien Moutinho]

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:Decomposingarbitrarytypes

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_design/

This said, some of these concerns may not apply to base.
Cheers :]
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 992 bytes
Desc: Digital signature
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170707/fcb8438d/attachment.sig>