search

glaebhoerl / type-eq

Type equality evidence you can carry around
http://hackage.haskell.org/package/type-eq
Other
5 stars 2 forks source link

Offer opaque ways to use equality #8

Open treeowl opened 7 years ago

treeowl commented 7 years ago

As far as I can tell, the library doesn't currently offer fully general ways to eliminate equality without leaning on GHC's fancy equality constraint propagation. The bare-bones basic function is

-- | Eliminate equality evidence
useEq :: a :~: b -> f a -> f b
useEq Refl x = x
treeowl commented 7 years ago

I've edited the description above because I realized one piece was silly.

glaebhoerl commented 7 years ago

This library has been essentially superseded by the Data.Type.Equality module in base, so maybe that would be a better place to add this?

For the record, what's the use case?

treeowl commented 7 years ago

Completeness, mostly. But someone could choose to restrict themselves, avoiding gcastWith, and therefore limit their language extension support needs to Rank2Types.

On Nov 11, 2016 5:34 AM, "Gábor Lehel" notifications@github.com wrote:

This library has been essentially superseded by the Data.Type.Equality https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-Type-Equality.html module in base, so maybe that would be a better place to add this?

For the record, what's the use case?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/glaebhoerl/type-eq/issues/8#issuecomment-259929366, or mute the thread https://github.com/notifications/unsubscribe-auth/ABzi_VDCxUEXuWuNYpUTOzopO-NItSiAks5q9ESdgaJpZM4KvXN4 .

glaebhoerl commented 7 years ago

I don't maintain this any more in any case, but I'd be happy to give you commit access if you want it.