Heterogeneous equality into base?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
28 messages Options
12
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Heterogeneous equality into base?

Wolfgang Jeltsch-3
Hi!

The module Data.Type.Equality in the base package contains the type
(:~:) for homogeneous equality. However, a type for heterogeneous
equality would be very useful as well. I would define such a type as
follows:

> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}

> data (a :: k) :~~: (b :: l) where

>     Refl :: a :~~: a

Is there already such a type in the base package? If not, does it make
sense to file a feature request (or would such a proposal be likely to
not being accepted for some reason)?

All the best,
Wolfgang
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

David Feuer
That seems generally reasonable to me. It'll need the usual discussion
process here and then it can be added to `base`. However, I think it
should not be added to `Data.Type.Equality`, but rather to a new
module, perhaps `Data.Type.Equality.Heterogeneous`. That module will
then be able to offer the full complement of basic functions (sym,
trans, ...) without stepping on the pre-existing names. I imagine
you'll also want one or two extra casting operations, and conversions
between `:~:` and `:~~:`. Also, you have called the constructor of
this type HRefl in the past, which strikes me as better than Refl.

David

On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch
<[hidden email]> wrote:

> Hi!
>
> The module Data.Type.Equality in the base package contains the type
> (:~:) for homogeneous equality. However, a type for heterogeneous
> equality would be very useful as well. I would define such a type as
> follows:
>
>> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
>>
>> data (a :: k) :~~: (b :: l) where
>>
>>     Refl :: a :~~: a
>
> Is there already such a type in the base package? If not, does it make
> sense to file a feature request (or would such a proposal be likely to
> not being accepted for some reason)?
>
> All the best,
> Wolfgang
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Eric Mertens
This seems like the kind of thing that first should be fleshed out in its own package. Is there some reason that this module would need to be in base?

On Thu, Jul 6, 2017 at 1:56 PM David Feuer <[hidden email]> wrote:
That seems generally reasonable to me. It'll need the usual discussion
process here and then it can be added to `base`. However, I think it
should not be added to `Data.Type.Equality`, but rather to a new
module, perhaps `Data.Type.Equality.Heterogeneous`. That module will
then be able to offer the full complement of basic functions (sym,
trans, ...) without stepping on the pre-existing names. I imagine
you'll also want one or two extra casting operations, and conversions
between `:~:` and `:~~:`. Also, you have called the constructor of
this type HRefl in the past, which strikes me as better than Refl.

David

On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch
<[hidden email]> wrote:
> Hi!
>
> The module Data.Type.Equality in the base package contains the type
> (:~:) for homogeneous equality. However, a type for heterogeneous
> equality would be very useful as well. I would define such a type as
> follows:
>
>> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
>>
>> data (a :: k) :~~: (b :: l) where
>>
>>     Refl :: a :~~: a
>
> Is there already such a type in the base package? If not, does it make
> sense to file a feature request (or would such a proposal be likely to
> not being accepted for some reason)?
>
> All the best,
> Wolfgang
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

David Menendez-2
In reply to this post by Wolfgang Jeltsch-3
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.

On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch
<[hidden email]> wrote:

> Hi!
>
> The module Data.Type.Equality in the base package contains the type
> (:~:) for homogeneous equality. However, a type for heterogeneous
> equality would be very useful as well. I would define such a type as
> follows:
>
>> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
>>
>> data (a :: k) :~~: (b :: l) where
>>
>>     Refl :: a :~~: a
>
> Is there already such a type in the base package? If not, does it make
> sense to file a feature request (or would such a proposal be likely to
> not being accepted for some reason)?
>
> All the best,
> Wolfgang
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries



--
Dave Menendez <[hidden email]>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Wolfgang Jeltsch-3
In reply to this post by David Feuer
Hi!

From https://wiki.haskell.org/Library_submissions, I understood that the
discussion should take place on the GHC Trac and will be moved to the
Libraries Mailing List only in serious cases. Is this the
case?(Interestingly, the link on the aforementioned page contains a
bogus URL. However, I do not know for sure the correct URL to fix this.)

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”).

I will try to come up with an initial implementation of this new
Data.Type.Equality.Heterogeneous module.

All the best,
Wolfgang

Am Donnerstag, den 06.07.2017, 16:55 -0400 schrieb David Feuer:

> That seems generally reasonable to me. It'll need the usual discussion
> process here and then it can be added to `base`. However, I think it
> should not be added to `Data.Type.Equality`, but rather to a new
> module, perhaps `Data.Type.Equality.Heterogeneous`. That module will
> then be able to offer the full complement of basic functions (sym,
> trans, ...) without stepping on the pre-existing names. I imagine
> you'll also want one or two extra casting operations, and conversions
> between `:~:` and `:~~:`. Also, you have called the constructor of
> this type HRefl in the past, which strikes me as better than Refl.
>
> David
>
> On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch
> <[hidden email]> wrote:
> >
> > Hi!
> >
> > The module Data.Type.Equality in the base package contains the type
> > (:~:) for homogeneous equality. However, a type for heterogeneous
> > equality would be very useful as well. I would define such a type as
> > follows:
> >
> > >
> > > {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
> > >
> > > data (a :: k) :~~: (b :: l) where
> > >
> > >     Refl :: a :~~: a
> >
> > Is there already such a type in the base package? If not, does it
> > make sense to file a feature request (or would such a proposal be
> > likely to not being accepted for some reason)?
> >
> > All the best,
> > Wolfgang
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Wolfgang Jeltsch-3
In reply to this post by David Menendez-2
Hi!

Yes, I have some code that uses this heterogeneous equality type
apparently successfully. I will try to explain the idea behind this code
a bit.

There is a kind-polymorphic class Q that contains an associated type
synonym family that maps instances of Q to types of kind *. This type
synonym family shall be injective, and there should be actual witness of
this injectivity. This is achieved by requiring every instantiation of Q
to provide a heterogeneous equality proof of some kind. The equality
must be heterogeneous, because Q is kind-polymorphic.

Here is some code that illustrates the idea in more detail:

> {-# LANGUAGE GADTs,
>              PolyKinds,
>              TypeFamilies,
>              TypeOperators,
>              UndecidableInstances,
>              UndecidableSuperClasses #-}

> import GHC.Exts (Constraint)

> -- * Heterogeneous equality

> data (a :: l) :~~: (b :: k) where

>     Refl :: a :~~: a

> transLike :: a :~~: c -> b :~~: c -> a :~~: b
> transLike Refl Refl = Refl

> -- * Interface

> type family C a :: k -> Constraint

> class C (F q) q => Q q where

>     type F q :: *

>     eq :: (Q q', F q ~ F q') => q :~~: q'

> -- * Implementation for []/Bool

> class ListQ q where

>     listEq :: q :~~: []

> instance ListQ [] where

>     listEq = Refl

> type instance C Bool = ListQ

> instance Q [] where

>     type F [] = Bool

>     eq = transLike listEq listEq

The central thing is the eq method, whose complete type is as follows:

    forall q q' . (Q q, Q q', F q ~ F q') => q :~~: q'

All the best,
Wolfgang

Am Donnerstag, den 06.07.2017, 17:15 -0400 schrieb David Menendez:

> 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.
>
> On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch
> <[hidden email]> wrote:
> >
> > Hi!
> >
> > The module Data.Type.Equality in the base package contains the type
> > (:~:) for homogeneous equality. However, a type for heterogeneous
> > equality would be very useful as well. I would define such a type as
> > follows:
> >
> > >
> > > {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
> > >
> > > data (a :: k) :~~: (b :: l) where
> > >
> > >     Refl :: a :~~: a
> > Is there already such a type in the base package? If not, does it
> > make
> > sense to file a feature request (or would such a proposal be likely
> > to
> > not being accepted for some reason)?
> >
> > All the best,
> > Wolfgang
> > _______________________________________________
> > Libraries mailing list
> > [hidden email]
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Richard Eisenberg-4
Hi Ben,

This discussion of heterogeneous equality in base may be of interest to you. Did you have to use a similar definition to get the new Typeable stuff working? I would imagine so. If you indeed did, that would provide a good argument for exporting this definition from base.

Separately from seeking Ben's input, I am in favor of this addition. If (:~:) is in base, (:~~:) should be, too.

Thanks,
Richard

> On Jul 6, 2017, at 6:10 PM, Wolfgang Jeltsch <[hidden email]> wrote:
>
> Hi!
>
> Yes, I have some code that uses this heterogeneous equality type
> apparently successfully. I will try to explain the idea behind this code
> a bit.
>
> There is a kind-polymorphic class Q that contains an associated type
> synonym family that maps instances of Q to types of kind *. This type
> synonym family shall be injective, and there should be actual witness of
> this injectivity. This is achieved by requiring every instantiation of Q
> to provide a heterogeneous equality proof of some kind. The equality
> must be heterogeneous, because Q is kind-polymorphic.
>
> Here is some code that illustrates the idea in more detail:
>
>> {-# LANGUAGE GADTs,
>>               PolyKinds,
>>               TypeFamilies,
>>               TypeOperators,
>>               UndecidableInstances,
>>               UndecidableSuperClasses #-}
>>  
>> import GHC.Exts (Constraint)
>>  
>> -- * Heterogeneous equality
>>  
>> data (a :: l) :~~: (b :: k) where
>>  
>>      Refl :: a :~~: a
>>  
>> transLike :: a :~~: c -> b :~~: c -> a :~~: b
>> transLike Refl Refl = Refl
>>  
>> -- * Interface
>>  
>> type family C a :: k -> Constraint
>>  
>> class C (F q) q => Q q where
>>  
>>      type F q :: *
>>  
>>      eq :: (Q q', F q ~ F q') => q :~~: q'
>>  
>> -- * Implementation for []/Bool
>>  
>> class ListQ q where
>>  
>>      listEq :: q :~~: []
>>  
>> instance ListQ [] where
>>  
>>      listEq = Refl
>>  
>> type instance C Bool = ListQ
>>  
>> instance Q [] where
>>  
>>      type F [] = Bool
>>  
>>      eq = transLike listEq listEq
>
> The central thing is the eq method, whose complete type is as follows:
>
>     forall q q' . (Q q, Q q', F q ~ F q') => q :~~: q'
>
> All the best,
> Wolfgang
>
> Am Donnerstag, den 06.07.2017, 17:15 -0400 schrieb David Menendez:
>> 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.
>>
>> On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch
>> <[hidden email]> wrote:
>>>
>>> Hi!
>>>
>>> The module Data.Type.Equality in the base package contains the type
>>> (:~:) for homogeneous equality. However, a type for heterogeneous
>>> equality would be very useful as well. I would define such a type as
>>> follows:
>>>
>>>>
>>>> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
>>>>
>>>> data (a :: k) :~~: (b :: l) where
>>>>
>>>>     Refl :: a :~~: a
>>> Is there already such a type in the base package? If not, does it
>>> make
>>> sense to file a feature request (or would such a proposal be likely
>>> to
>>> not being accepted for some reason)?
>>>
>>> All the best,
>>> Wolfgang
>>> _______________________________________________
>>> Libraries mailing list
>>> [hidden email]
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Julien Moutinho
In reply to this post by Wolfgang Jeltsch-3
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 :]

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

signature.asc (1011 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Ryan Scott
In reply to this post by Wolfgang Jeltsch-3
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.

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Wolfgang Jeltsch-3
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/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37
> [2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

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 <[hidden email]> 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/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37
>> [2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

David Feuer
FWIW, I agree with Andrew Martin on this one.

On Jul 8, 2017 9:26 PM, "Andrew Martin" <[hidden email]> 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 <[hidden email]> 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/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37
>> [2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Carter Schonwald
I think it also needs to be available to all clients of new typeable too! right?

On Sat, Jul 8, 2017 at 9:37 PM, David Feuer <[hidden email]> wrote:
FWIW, I agree with Andrew Martin on this one.

On Jul 8, 2017 9:26 PM, "Andrew Martin" <[hidden email]> 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 <[hidden email]> 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/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37
>> [2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Wolfgang Jeltsch-3
In reply to this post by Andrew Martin
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 <[hidden email]
> > fo> 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
> > [hidden email]
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Oleg Grenrus
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 <[hidden email]> 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 <[hidden email]
fo> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Edward Kmett-2
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]
fo> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Richard Eisenberg-4

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

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Edward Kmett-2
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 <[hidden email]> wrote:


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

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

Ryan Scott
In reply to this post by Wolfgang Jeltsch-3
I also agree that we should keep HRefl a distinct name, and moreover, we should keep :~: and :~~: as distinct datatypes.

I'm also on-board with the idea that we should introduce a separate Data.Type.Equality.Hetero module that reexports :~~: and defines heterogeneous counterparts for sym, trans, etc. from Data.Type.Equality. I don't have a strong opinion on how they should be named (e.g., sym vs. hsym).

Ryan S.

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Heterogeneous equality into base?

David Feuer
There's another version of heterogeneous equality that takes its
arguments in the other order. I'm not sure if this is generally useful
enough to want to include.

-- (:~~:) :: forall j k. j -> k -> *

data OtherEquality :: forall j. j -> forall k. k -> Type where
  OtherRefl :: OtherEquality a a

On Mon, Jul 10, 2017 at 11:24 AM, Ryan Scott <[hidden email]> wrote:

> I also agree that we should keep HRefl a distinct name, and moreover, we
> should keep :~: and :~~: as distinct datatypes.
>
> I'm also on-board with the idea that we should introduce a separate
> Data.Type.Equality.Hetero module that reexports :~~: and defines
> heterogeneous counterparts for sym, trans, etc. from Data.Type.Equality. I
> don't have a strong opinion on how they should be named (e.g., sym vs.
> hsym).
>
> Ryan S.
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
12
Loading...