Let's rework Data.Type.Equality.==

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
16 messages Options
Reply | Threaded
Open this post in threaded view
|

Let's rework Data.Type.Equality.==

David Feuer
The (==) type family in Data.Type.Equality was designed largely to calculate structural equality of types. However, limitations of GHC's type system at the type prevented this from being fully realized. Today, with TypeInType, we can actually do it, replacing the boatload of ad hoc instances like so:

type (a :: k) == (b :: k) = Equal k a b
infix 4 ==

type family Equal (k :: Type) (a :: k) (b :: k) where
 Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
        Equal (j -> k) f g && Equal j a b
 Equal k a a = 'True
 Equal k a b = 'False

This == behaves in a much more uniform way than the current one. I see two potential causes for complaint:

1. For types of kind *, the new version will sometimes fail to reduce when the old one succeeded (and vice versa). For example, GHC currently accepts

eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True
eqeq _ = Refl

while the proposed version does not.

2. Some users may want non-structural equality on their types for some reason. The only example in base is

type instance (a :: ()) == (b :: ()) = 'True

which consists two types of kind () the same even if they're stuck types. But perhaps someone wants to implement a non-trivial type-level data structure with a special notion of equality.


I don't think (1) is really worth worrying too much about. For (2), if users want to have control, we could at least use a mechanism similar to the above to make the obvious instances easier to write.

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

Re: Let's rework Data.Type.Equality.==

David Feuer
To be more specific about the ad hoc equality option, I'm thinking about something like this (if it doesn't compile, I'm sure something similar will):

type family (a :: k) == (b :: k) :: Bool
infix 4 ==

type family Equal (k :: Type) (a :: k) (b :: k) where
  Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
        Equal (j -> k) f g && (a == b)
  Equal k a a = 'True
  Equal k a b = 'False

type instance (a :: Type) == b = Equal Type a b
type instance (a :: Maybe k) == b = Equal Type a b
....

So for example, we'd get

'Just (x :: k) == 'Just y
=
Equal (k -> Maybe k) 'Just && x == y
=
x == y

On Aug 10, 2017 12:29 AM, "David Feuer" <[hidden email]> wrote:
The (==) type family in Data.Type.Equality was designed largely to calculate structural equality of types. However, limitations of GHC's type system at the type prevented this from being fully realized. Today, with TypeInType, we can actually do it, replacing the boatload of ad hoc instances like so:

type (a :: k) == (b :: k) = Equal k a b
infix 4 ==

type family Equal (k :: Type) (a :: k) (b :: k) where
 Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
        Equal (j -> k) f g && Equal j a b
 Equal k a a = 'True
 Equal k a b = 'False

This == behaves in a much more uniform way than the current one. I see two potential causes for complaint:

1. For types of kind *, the new version will sometimes fail to reduce when the old one succeeded (and vice versa). For example, GHC currently accepts

eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True
eqeq _ = Refl

while the proposed version does not.

2. Some users may want non-structural equality on their types for some reason. The only example in base is

type instance (a :: ()) == (b :: ()) = 'True

which consists two types of kind () the same even if they're stuck types. But perhaps someone wants to implement a non-trivial type-level data structure with a special notion of equality.


I don't think (1) is really worth worrying too much about. For (2), if users want to have control, we could at least use a mechanism similar to the above to make the obvious instances easier to write.


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

Re: Let's rework Data.Type.Equality.==

Ivan Lazar Miljenovic
On 10 August 2017 at 14:44, David Feuer <[hidden email]> wrote:

> To be more specific about the ad hoc equality option, I'm thinking about
> something like this (if it doesn't compile, I'm sure something similar
> will):
>
> type family (a :: k) == (b :: k) :: Bool
> infix 4 ==
>
> type family Equal (k :: Type) (a :: k) (b :: k) where
>   Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
>         Equal (j -> k) f g && (a == b)
>   Equal k a a = 'True
>   Equal k a b = 'False
>
> type instance (a :: Type) == b = Equal Type a b
> type instance (a :: Maybe k) == b = Equal Type a b

Since this is a closed type family, isn't doing any extra explicit
type instances illegal?

> ....
>
> So for example, we'd get
>
> 'Just (x :: k) == 'Just y
> =
> Equal (k -> Maybe k) 'Just && x == y
> =
> x == y
>
> On Aug 10, 2017 12:29 AM, "David Feuer" <[hidden email]> wrote:
>
> The (==) type family in Data.Type.Equality was designed largely to calculate
> structural equality of types. However, limitations of GHC's type system at
> the type prevented this from being fully realized. Today, with TypeInType,
> we can actually do it, replacing the boatload of ad hoc instances like so:
>
> type (a :: k) == (b :: k) = Equal k a b
> infix 4 ==
>
> type family Equal (k :: Type) (a :: k) (b :: k) where
>  Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
>         Equal (j -> k) f g && Equal j a b
>  Equal k a a = 'True
>  Equal k a b = 'False
>
> This == behaves in a much more uniform way than the current one. I see two
> potential causes for complaint:
>
> 1. For types of kind *, the new version will sometimes fail to reduce when
> the old one succeeded (and vice versa). For example, GHC currently accepts
>
> eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True
> eqeq _ = Refl
>
> while the proposed version does not.
>
> 2. Some users may want non-structural equality on their types for some
> reason. The only example in base is
>
> type instance (a :: ()) == (b :: ()) = 'True
>
> which consists two types of kind () the same even if they're stuck types.
> But perhaps someone wants to implement a non-trivial type-level data
> structure with a special notion of equality.
>
>
> I don't think (1) is really worth worrying too much about. For (2), if users
> want to have control, we could at least use a mechanism similar to the above
> to make the obvious instances easier to write.
>
>
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>



--
Ivan Lazar Miljenovic
[hidden email]
http://IvanMiljenovic.wordpress.com
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Let's rework Data.Type.Equality.==

David Feuer
(==), in that option, is an open type family, and Equal (more likely a synonym dealing with its kind) is a helper function. Note that Equality, in this version, calls == to deal with arguments.

type DefaultEq (a :: k) (b :: k) = Equal k a b

Then if con1 and con2 are constructors,

DefaultEq (con1 a b) (con2 c d) =
  (con1 exactly equals con2) && a == c && b == d

The == for the kinds of a/c and b/d could be anything a user wishes.

On Aug 10, 2017 1:35 AM, "Ivan Lazar Miljenovic" <[hidden email]> wrote:
On 10 August 2017 at 14:44, David Feuer <[hidden email]> wrote:
> To be more specific about the ad hoc equality option, I'm thinking about
> something like this (if it doesn't compile, I'm sure something similar
> will):
>
> type family (a :: k) == (b :: k) :: Bool
> infix 4 ==
>
> type family Equal (k :: Type) (a :: k) (b :: k) where
>   Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
>         Equal (j -> k) f g && (a == b)
>   Equal k a a = 'True
>   Equal k a b = 'False
>
> type instance (a :: Type) == b = Equal Type a b
> type instance (a :: Maybe k) == b = Equal Type a b

Since this is a closed type family, isn't doing any extra explicit
type instances illegal?

> ....
>
> So for example, we'd get
>
> 'Just (x :: k) == 'Just y
> =
> Equal (k -> Maybe k) 'Just && x == y
> =
> x == y
>
> On Aug 10, 2017 12:29 AM, "David Feuer" <[hidden email]> wrote:
>
> The (==) type family in Data.Type.Equality was designed largely to calculate
> structural equality of types. However, limitations of GHC's type system at
> the type prevented this from being fully realized. Today, with TypeInType,
> we can actually do it, replacing the boatload of ad hoc instances like so:
>
> type (a :: k) == (b :: k) = Equal k a b
> infix 4 ==
>
> type family Equal (k :: Type) (a :: k) (b :: k) where
>  Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
>         Equal (j -> k) f g && Equal j a b
>  Equal k a a = 'True
>  Equal k a b = 'False
>
> This == behaves in a much more uniform way than the current one. I see two
> potential causes for complaint:
>
> 1. For types of kind *, the new version will sometimes fail to reduce when
> the old one succeeded (and vice versa). For example, GHC currently accepts
>
> eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True
> eqeq _ = Refl
>
> while the proposed version does not.
>
> 2. Some users may want non-structural equality on their types for some
> reason. The only example in base is
>
> type instance (a :: ()) == (b :: ()) = 'True
>
> which consists two types of kind () the same even if they're stuck types.
> But perhaps someone wants to implement a non-trivial type-level data
> structure with a special notion of equality.
>
>
> I don't think (1) is really worth worrying too much about. For (2), if users
> want to have control, we could at least use a mechanism similar to the above
> to make the obvious instances easier to write.
>
>
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>



--
Ivan Lazar Miljenovic
[hidden email]
http://IvanMiljenovic.wordpress.com

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

Re: Let's rework Data.Type.Equality.==

David Feuer
By the way.... the nicest version of the ad hoc equality would probably use a kind class:

class TEq (k :: Type) where
  type (==) (a :: k) (b :: k) :: Bool
  type a == b = DefaultEq a b

So then you could write

instance TEq (Maybe k)
instance TEq (Either j k)
instance TEq [k]
instance TEq (j -> k)
instance TEq () where
  type _ == _ = 'True

etc.

On Aug 10, 2017 1:46 AM, "David Feuer" <[hidden email]> wrote:
(==), in that option, is an open type family, and Equal (more likely a synonym dealing with its kind) is a helper function. Note that Equality, in this version, calls == to deal with arguments.

type DefaultEq (a :: k) (b :: k) = Equal k a b

Then if con1 and con2 are constructors,

DefaultEq (con1 a b) (con2 c d) =
  (con1 exactly equals con2) && a == c && b == d

The == for the kinds of a/c and b/d could be anything a user wishes.

On Aug 10, 2017 1:35 AM, "Ivan Lazar Miljenovic" <[hidden email]> wrote:
On 10 August 2017 at 14:44, David Feuer <[hidden email]> wrote:
> To be more specific about the ad hoc equality option, I'm thinking about
> something like this (if it doesn't compile, I'm sure something similar
> will):
>
> type family (a :: k) == (b :: k) :: Bool
> infix 4 ==
>
> type family Equal (k :: Type) (a :: k) (b :: k) where
>   Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
>         Equal (j -> k) f g && (a == b)
>   Equal k a a = 'True
>   Equal k a b = 'False
>
> type instance (a :: Type) == b = Equal Type a b
> type instance (a :: Maybe k) == b = Equal Type a b

Since this is a closed type family, isn't doing any extra explicit
type instances illegal?

> ....
>
> So for example, we'd get
>
> 'Just (x :: k) == 'Just y
> =
> Equal (k -> Maybe k) 'Just && x == y
> =
> x == y
>
> On Aug 10, 2017 12:29 AM, "David Feuer" <[hidden email]> wrote:
>
> The (==) type family in Data.Type.Equality was designed largely to calculate
> structural equality of types. However, limitations of GHC's type system at
> the type prevented this from being fully realized. Today, with TypeInType,
> we can actually do it, replacing the boatload of ad hoc instances like so:
>
> type (a :: k) == (b :: k) = Equal k a b
> infix 4 ==
>
> type family Equal (k :: Type) (a :: k) (b :: k) where
>  Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
>         Equal (j -> k) f g && Equal j a b
>  Equal k a a = 'True
>  Equal k a b = 'False
>
> This == behaves in a much more uniform way than the current one. I see two
> potential causes for complaint:
>
> 1. For types of kind *, the new version will sometimes fail to reduce when
> the old one succeeded (and vice versa). For example, GHC currently accepts
>
> eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True
> eqeq _ = Refl
>
> while the proposed version does not.
>
> 2. Some users may want non-structural equality on their types for some
> reason. The only example in base is
>
> type instance (a :: ()) == (b :: ()) = 'True
>
> which consists two types of kind () the same even if they're stuck types.
> But perhaps someone wants to implement a non-trivial type-level data
> structure with a special notion of equality.
>
>
> I don't think (1) is really worth worrying too much about. For (2), if users
> want to have control, we could at least use a mechanism similar to the above
> to make the obvious instances easier to write.
>
>
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>



--
Ivan Lazar Miljenovic
[hidden email]
http://IvanMiljenovic.wordpress.com

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

Re: Let's rework Data.Type.Equality.==

David Feuer
You can see the two main approaches in
https://phabricator.haskell.org/D3835 and
https://phabricator.haskell.org/D3837

On Thu, Aug 10, 2017 at 1:57 AM, David Feuer <[hidden email]> wrote:

> By the way.... the nicest version of the ad hoc equality would probably use
> a kind class:
>
> class TEq (k :: Type) where
>   type (==) (a :: k) (b :: k) :: Bool
>   type a == b = DefaultEq a b
>
> So then you could write
>
> instance TEq (Maybe k)
> instance TEq (Either j k)
> instance TEq [k]
> instance TEq (j -> k)
> instance TEq () where
>   type _ == _ = 'True
>
> etc.
>
> On Aug 10, 2017 1:46 AM, "David Feuer" <[hidden email]> wrote:
>>
>> (==), in that option, is an open type family, and Equal (more likely a
>> synonym dealing with its kind) is a helper function. Note that Equality, in
>> this version, calls == to deal with arguments.
>>
>> type DefaultEq (a :: k) (b :: k) = Equal k a b
>>
>> Then if con1 and con2 are constructors,
>>
>> DefaultEq (con1 a b) (con2 c d) =
>>   (con1 exactly equals con2) && a == c && b == d
>>
>> The == for the kinds of a/c and b/d could be anything a user wishes.
>>
>> On Aug 10, 2017 1:35 AM, "Ivan Lazar Miljenovic"
>> <[hidden email]> wrote:
>>>
>>> On 10 August 2017 at 14:44, David Feuer <[hidden email]> wrote:
>>> > To be more specific about the ad hoc equality option, I'm thinking
>>> > about
>>> > something like this (if it doesn't compile, I'm sure something similar
>>> > will):
>>> >
>>> > type family (a :: k) == (b :: k) :: Bool
>>> > infix 4 ==
>>> >
>>> > type family Equal (k :: Type) (a :: k) (b :: k) where
>>> >   Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
>>> >         Equal (j -> k) f g && (a == b)
>>> >   Equal k a a = 'True
>>> >   Equal k a b = 'False
>>> >
>>> > type instance (a :: Type) == b = Equal Type a b
>>> > type instance (a :: Maybe k) == b = Equal Type a b
>>>
>>> Since this is a closed type family, isn't doing any extra explicit
>>> type instances illegal?
>>>
>>> > ....
>>> >
>>> > So for example, we'd get
>>> >
>>> > 'Just (x :: k) == 'Just y
>>> > =
>>> > Equal (k -> Maybe k) 'Just && x == y
>>> > =
>>> > x == y
>>> >
>>> > On Aug 10, 2017 12:29 AM, "David Feuer" <[hidden email]> wrote:
>>> >
>>> > The (==) type family in Data.Type.Equality was designed largely to
>>> > calculate
>>> > structural equality of types. However, limitations of GHC's type system
>>> > at
>>> > the type prevented this from being fully realized. Today, with
>>> > TypeInType,
>>> > we can actually do it, replacing the boatload of ad hoc instances like
>>> > so:
>>> >
>>> > type (a :: k) == (b :: k) = Equal k a b
>>> > infix 4 ==
>>> >
>>> > type family Equal (k :: Type) (a :: k) (b :: k) where
>>> >  Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
>>> >         Equal (j -> k) f g && Equal j a b
>>> >  Equal k a a = 'True
>>> >  Equal k a b = 'False
>>> >
>>> > This == behaves in a much more uniform way than the current one. I see
>>> > two
>>> > potential causes for complaint:
>>> >
>>> > 1. For types of kind *, the new version will sometimes fail to reduce
>>> > when
>>> > the old one succeeded (and vice versa). For example, GHC currently
>>> > accepts
>>> >
>>> > eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True
>>> > eqeq _ = Refl
>>> >
>>> > while the proposed version does not.
>>> >
>>> > 2. Some users may want non-structural equality on their types for some
>>> > reason. The only example in base is
>>> >
>>> > type instance (a :: ()) == (b :: ()) = 'True
>>> >
>>> > which consists two types of kind () the same even if they're stuck
>>> > types.
>>> > But perhaps someone wants to implement a non-trivial type-level data
>>> > structure with a special notion of equality.
>>> >
>>> >
>>> > I don't think (1) is really worth worrying too much about. For (2), if
>>> > users
>>> > want to have control, we could at least use a mechanism similar to the
>>> > above
>>> > to make the obvious instances easier to write.
>>> >
>>> >
>>> >
>>> > _______________________________________________
>>> > Libraries mailing list
>>> > [hidden email]
>>> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>> >
>>>
>>>
>>>
>>> --
>>> Ivan Lazar Miljenovic
>>> [hidden email]
>>> http://IvanMiljenovic.wordpress.com
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Let's rework Data.Type.Equality.==

Ryan Scott
In reply to this post by David Feuer
Personally, I'd be more inclined towards latter approach (in
https://phabricator.haskell.org/D3837). After all, one of the key
properties of (==) (for which the Haddocks even make a special note)
is that it does not attempt to provide an instance that works for
every possible kind. Indeed, as you've discovered, there are cases
when it doesn't make sense to use DefaultEq, such as for ().

I'll tentatively give my support for D3837, although I'd be curious to
hear what Richard has to say about this (since I'm reasonably
confident he gave (==) its current implementation).

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

Re: Let's rework Data.Type.Equality.==

David Feuer
I tend to agree with you, although I don't think () is a compelling argument. Rather,  it reuses the name == that Haskellers are accustomed to defining flexibly. But for that same reason, as well as the convenience, I do think we should consider using a kind class. That way things at the type level look pretty much like they do at the term level.

On Aug 10, 2017 10:59 AM, "Ryan Scott" <[hidden email]> wrote:
Personally, I'd be more inclined towards latter approach (in
https://phabricator.haskell.org/D3837). After all, one of the key
properties of (==) (for which the Haddocks even make a special note)
is that it does not attempt to provide an instance that works for
every possible kind. Indeed, as you've discovered, there are cases
when it doesn't make sense to use DefaultEq, such as for ().

I'll tentatively give my support for D3837, although I'd be curious to
hear what Richard has to say about this (since I'm reasonably
confident he gave (==) its current implementation).

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
Reply | Threaded
Open this post in threaded view
|

Re: Let's rework Data.Type.Equality.==

Richard Eisenberg-4
tl;dr: I like David's first version, D3835.

There is a fundamental tension in the definition of (==): Should it be reflexive or not? By "reflexive" here, I mean that (a == a) reduces to True, even if you know nothing further about a. The current definition of (==) is reflexive in this way for types of kind Type, but not for any of the other concrete instances (except the one for ()).

We can't currently have our cake and it eat, too: as David points out in this thread, (==) is either reflexive or structurally recursive. It can't do both. Possibly a solution to #4259 (https://ghc.haskell.org/trac/ghc/ticket/4259) would allow us to have (==) that is both reflexive and structurally recursive, but I have no idea how to do it.

I agree that the current choice of implementation for (==) is inconsistent in this regard and is perhaps foolish. I have no principled argument for why it is the way it is. But I wonder if we're better off embracing the distinction between a reflexive (==) and a structurally recursive (==) and provide both, with different names. Or, we could just decide to go with the structurally recursive one, which seems to be more useful, especially as I have become much more skeptical of non-linear patterns (necessary for the reflexive (==)). In particular, I don't have a good story for how they would work in Dependent Haskell. Section 5.13.2 of my thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf) contains some technical discussion of the challenges, but that section may not be digestible on its own. 

The point of difference between David's two proposed changes is extensibility: that is, could someone decide to have a custom equality operator on a user-defined type? This is indeed a reasonable thing to want -- for example, you could imagine a record system that stores names of fields and their types in a type-level list, but that list should really be regarded as a set. However, worms lurk under this stone. If we have a more flexible notion of equality, how can we be sure that this more inclusive equality is always respected? Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context, everything still works. Sadly, there is no way to guarantee such a property. If (==) is to be useful in a type system, we would need such a guarantee. (By "useful", I mean that this is implementable: reifyEq :: ((a == b) ~ True, Typeable a, Typeable b) => a :~: b.) This brings us to the doorstep of higher inductive types -- a door that might be fun to enter, but is a long long way off.

In sum, I argue for David's first, inextensible version.

By the way, nothing about this requires TypeInType. If I had thought of David's version (that splits apart type applications) in 2013, I probably would have implemented (==) that way.

Richard

On Aug 10, 2017, at 9:00 PM, David Feuer <[hidden email]> wrote:

I tend to agree with you, although I don't think () is a compelling argument. Rather,  it reuses the name == that Haskellers are accustomed to defining flexibly. But for that same reason, as well as the convenience, I do think we should consider using a kind class. That way things at the type level look pretty much like they do at the term level.

On Aug 10, 2017 10:59 AM, "Ryan Scott" <[hidden email]> wrote:
Personally, I'd be more inclined towards latter approach (in
https://phabricator.haskell.org/D3837). After all, one of the key
properties of (==) (for which the Haddocks even make a special note)
is that it does not attempt to provide an instance that works for
every possible kind. Indeed, as you've discovered, there are cases
when it doesn't make sense to use DefaultEq, such as for ().

I'll tentatively give my support for D3837, although I'd be curious to
hear what Richard has to say about this (since I'm reasonably
confident he gave (==) its current implementation).

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


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

Re: Let's rework Data.Type.Equality.==

Carter Schonwald
The close family with nonlinear matching does seem simpler.  Like I can comfortably read it and understand what it does reasonably well and have uniform expectations of what it means. 

That said, I'm open to be swayed otherwise.  The 

On Fri, Aug 11, 2017 at 11:44 AM Richard Eisenberg <[hidden email]> wrote:
tl;dr: I like David's first version, D3835.

There is a fundamental tension in the definition of (==): Should it be reflexive or not? By "reflexive" here, I mean that (a == a) reduces to True, even if you know nothing further about a. The current definition of (==) is reflexive in this way for types of kind Type, but not for any of the other concrete instances (except the one for ()).

We can't currently have our cake and it eat, too: as David points out in this thread, (==) is either reflexive or structurally recursive. It can't do both. Possibly a solution to #4259 (https://ghc.haskell.org/trac/ghc/ticket/4259) would allow us to have (==) that is both reflexive and structurally recursive, but I have no idea how to do it.

I agree that the current choice of implementation for (==) is inconsistent in this regard and is perhaps foolish. I have no principled argument for why it is the way it is. But I wonder if we're better off embracing the distinction between a reflexive (==) and a structurally recursive (==) and provide both, with different names. Or, we could just decide to go with the structurally recursive one, which seems to be more useful, especially as I have become much more skeptical of non-linear patterns (necessary for the reflexive (==)). In particular, I don't have a good story for how they would work in Dependent Haskell. Section 5.13.2 of my thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf) contains some technical discussion of the challenges, but that section may not be digestible on its own. 

The point of difference between David's two proposed changes is extensibility: that is, could someone decide to have a custom equality operator on a user-defined type? This is indeed a reasonable thing to want -- for example, you could imagine a record system that stores names of fields and their types in a type-level list, but that list should really be regarded as a set. However, worms lurk under this stone. If we have a more flexible notion of equality, how can we be sure that this more inclusive equality is always respected? Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context, everything still works. Sadly, there is no way to guarantee such a property. If (==) is to be useful in a type system, we would need such a guarantee. (By "useful", I mean that this is implementable: reifyEq :: ((a == b) ~ True, Typeable a, Typeable b) => a :~: b.) This brings us to the doorstep of higher inductive types -- a door that might be fun to enter, but is a long long way off.

In sum, I argue for David's first, inextensible version.

By the way, nothing about this requires TypeInType. If I had thought of David's version (that splits apart type applications) in 2013, I probably would have implemented (==) that way.

Richard

On Aug 10, 2017, at 9:00 PM, David Feuer <[hidden email]> wrote:

I tend to agree with you, although I don't think () is a compelling argument. Rather,  it reuses the name == that Haskellers are accustomed to defining flexibly. But for that same reason, as well as the convenience, I do think we should consider using a kind class. That way things at the type level look pretty much like they do at the term level.

On Aug 10, 2017 10:59 AM, "Ryan Scott" <[hidden email]> wrote:
Personally, I'd be more inclined towards latter approach (in
https://phabricator.haskell.org/D3837). After all, one of the key
properties of (==) (for which the Haddocks even make a special note)
is that it does not attempt to provide an instance that works for
every possible kind. Indeed, as you've discovered, there are cases
when it doesn't make sense to use DefaultEq, such as for ().

I'll tentatively give my support for D3837, although I'd be curious to
hear what Richard has to say about this (since I'm reasonably
confident he gave (==) its current implementation).

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

_______________________________________________
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
|

Re: Let's rework Data.Type.Equality.==

Phil Ruffwind
In reply to this post by Richard Eisenberg-4
On Fri, Aug 11, 2017, at 11:39, Richard Eisenberg wrote:
> If we have a more flexible notion of equality, how can we be sure that this
> more inclusive equality is always respected? Specifically, you would want
> this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context,
> everything still works.

Not too familiar with this area, but I recall at one point realizing
that the
only kind of user-defined equality that is consistent with Leibniz
equality is
when the difference occurs in rigid type variables.  That is, whereas
you
can't make Set (A, B) == Set (B, A) since they are observably different,
you
can (sometimes) make F a == F b if a and b are existentially quantified
variables (no-one would be the wiser).
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Let's rework Data.Type.Equality.==

David Feuer
In reply to this post by Richard Eisenberg-4
On Aug 11, 2017 9:39 AM, "Richard Eisenberg" <[hidden email]> wrote:

But I wonder if we're better off dxaa aembracing the distinction between a reflexive (==) and a structurally recursive (==) and provide both, with different names.

I don't think it would be bad to offer a canonical reflexive equality test. There are probably situations where having such a thing would be marginally useful. In particular,

MyEqual a b ~ 'False

isn't quite the same ass Alaska

YourEqual a b ~ 'False

even if the two type families are defined the same.

Or, we could just decide to go with the structurally recursive one, which seems to be more useful, especially as I have become much more skeptical of non-linear patterns (necessary Aziz a a add as ad ahs asf as s for the reflexive (==)).

I'm a bit fuzzy on this. Don't *both* of my versions rely essentially on nonlinear patterns to compare constructors? I suppose it might c always xd Hz


In particular, I don't have a good story for how they would work in Dependent Haskell. Section 5.13.2 of my thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf) contains some technical discussion of the challenges, but that section may not be digestible on its own. 

The point of difference between David's two proposed changes is extensibility: that is, could someone decide to have a custom equality operator on a user-defined type? This is indeed a reasonable thing to want -- for example, you could imagine a record system that stores names of fields and their types in a type-level list, but that list should really be regarded as a set. However, worms lurk under this stone. If we have a more flexible notion of equality, how can we be sure that this more inclusive equality is always respected? Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context, everything still works. Sadly, there is no way to guarantee such a property. If (==) is to be useful in a type system, we would need such a guarantee. (By "useful", I mean that this is implementable: reifyEq :: ((a == b) ~ True, Typeable a, Typeable b) => a :~: b.) This brings us to the doorstep of higher inductive types -- a door that might be fun to enter, but is a long long way off.

In sum, I argue for David's first, inextensible version.

By the way, nothing about this requires TypeInType. If I had thought of David's version (that splits apart type applications) in 2013, I probably would have implemented (==) that way.

Richard

On Aug 10, 2017, at 9:00 PM, David Feuer <[hidden email]> wrote:

I tend to agree with you, although I don't think () is a compelling argument. Rather,  it reuses the name == that Haskellers are accustomed to defining flexibly. But for that same reason, as well as the convenience, I do think we should consider using a kind class. That way things at the type level look pretty much like they do at the term level.

On Aug 10, 2017 10:59 AM, "Ryan Scott" <[hidden email]> wrote:
Personally, I'd be more inclined towards latter approach (in
https://phabricator.haskell.org/D3837). After all, one of the key
properties of (==) (for which the Haddocks even make a special note)
is that it does not attempt to provide an instance that works for
every possible kind. Indeed, as you've discovered, there are cases
when it doesn't make sense to use DefaultEq, such as for ().

I'll tentatively give my support for D3837, although I'd be curious to
hear what Richard has to say about this (since I'm reasonably
confident he gave (==) its current implementation).

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



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

Re: Let's rework Data.Type.Equality.==

Richard Eisenberg-4
Oops -- I guess that's true that your versions still rely on a non-linear pattern. I'm still fine with always using structural recursion, though.

Richard

On Aug 11, 2017, at 8:28 PM, David Feuer <[hidden email]> wrote:

On Aug 11, 2017 9:39 AM, "Richard Eisenberg" <[hidden email]> wrote:

But I wonder if we're better off dxaa aembracing the distinction between a reflexive (==) and a structurally recursive (==) and provide both, with different names.

I don't think it would be bad to offer a canonical reflexive equality test. There are probably situations where having such a thing would be marginally useful. In particular,

MyEqual a b ~ 'False

isn't quite the same ass Alaska

YourEqual a b ~ 'False

even if the two type families are defined the same.

Or, we could just decide to go with the structurally recursive one, which seems to be more useful, especially as I have become much more skeptical of non-linear patterns (necessary Aziz a a add as ad ahs asf as s for the reflexive (==)).

I'm a bit fuzzy on this. Don't *both* of my versions rely essentially on nonlinear patterns to compare constructors? I suppose it might c always xd Hz


In particular, I don't have a good story for how they would work in Dependent Haskell. Section 5.13.2 of my thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf) contains some technical discussion of the challenges, but that section may not be digestible on its own. 

The point of difference between David's two proposed changes is extensibility: that is, could someone decide to have a custom equality operator on a user-defined type? This is indeed a reasonable thing to want -- for example, you could imagine a record system that stores names of fields and their types in a type-level list, but that list should really be regarded as a set. However, worms lurk under this stone. If we have a more flexible notion of equality, how can we be sure that this more inclusive equality is always respected? Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context, everything still works. Sadly, there is no way to guarantee such a property. If (==) is to be useful in a type system, we would need such a guarantee. (By "useful", I mean that this is implementable: reifyEq :: ((a == b) ~ True, Typeable a, Typeable b) => a :~: b.) This brings us to the doorstep of higher inductive types -- a door that might be fun to enter, but is a long long way off.

In sum, I argue for David's first, inextensible version.

By the way, nothing about this requires TypeInType. If I had thought of David's version (that splits apart type applications) in 2013, I probably would have implemented (==) that way.

Richard

On Aug 10, 2017, at 9:00 PM, David Feuer <[hidden email]> wrote:

I tend to agree with you, although I don't think () is a compelling argument. Rather,  it reuses the name == that Haskellers are accustomed to defining flexibly. But for that same reason, as well as the convenience, I do think we should consider using a kind class. That way things at the type level look pretty much like they do at the term level.

On Aug 10, 2017 10:59 AM, "Ryan Scott" <[hidden email]> wrote:
Personally, I'd be more inclined towards latter approach (in
https://phabricator.haskell.org/D3837). After all, one of the key
properties of (==) (for which the Haddocks even make a special note)
is that it does not attempt to provide an instance that works for
every possible kind. Indeed, as you've discovered, there are cases
when it doesn't make sense to use DefaultEq, such as for ().

I'll tentatively give my support for D3837, although I'd be curious to
hear what Richard has to say about this (since I'm reasonably
confident he gave (==) its current implementation).

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




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

Re: Let's rework Data.Type.Equality.==

David Feuer
In reply to this post by David Feuer
Wow, that email really got garbled. I was in the process of drafting it when I sent it accidentally and then went off into the mountains and forgot about it. Sorry about that! I had a few more things to say.

First, it might be possible to get away from the non-linear pattern using a version of generics. In particular, if we derive Rep and From type families for each type, we can define (==) by comparing generic representations. Or we could derive (==) directly. Moreover, the non-linear pattern approach won't help us define type-level Ord; for that we need either direct or generic-mediated derivation. Related: it's a bit annoying that when the case  ((f :: j -> k) (a :: j)) is rejected, we *know* that the type being matched must be a constructor, but we can't really do anything directly with that information.

Second, you write

> If we have a more flexible notion of equality, how can we be sure that this more inclusive equality is always respected?
> [...]
Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context, everything still works. 

How is this really different from the situation on the term level? User code must always take care to respect the quotient. You say (==) is only "useful" if we can produce

reifyEq :: ((a == b) ~ True, Typeable a, Typeable b) => a :~: b.

I'm not convinced that this is the only measure of utility, although it's an important one. That said, I suspect that the version of (==) in Data.Type.Equality should be the simple polykinded one; others would probably fit better elsewhere. Feel free to accept D3835 if you think we should just do that.

On Aug 11, 2017 6:28 PM, "David Feuer" <[hidden email]> wrote:
On Aug 11, 2017 9:39 AM, "Richard Eisenberg" <[hidden email]> wrote:

But I wonder if we're better off dxaa aembracing the distinction between a reflexive (==) and a structurally recursive (==) and provide both, with different names.

I don't think it would be bad to offer a canonical reflexive equality test. There are probably situations where having such a thing would be marginally useful. In particular,

MyEqual a b ~ 'False

isn't quite the same ass Alaska

YourEqual a b ~ 'False

even if the two type families are defined the same.

Or, we could just decide to go with the structurally recursive one, which seems to be more useful, especially as I have become much more skeptical of non-linear patterns (necessary Aziz a a add as ad ahs asf as s for the reflexive (==)).

I'm a bit fuzzy on this. Don't *both* of my versions rely essentially on nonlinear patterns to compare constructors? I suppose it might c always xd Hz


In particular, I don't have a good story for how they would work in Dependent Haskell. Section 5.13.2 of my thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf) contains some technical discussion of the challenges, but that section may not be digestible on its own. 

The point of difference between David's two proposed changes is extensibility: that is, could someone decide to have a custom equality operator on a user-defined type? This is indeed a reasonable thing to want -- for example, you could imagine a record system that stores names of fields and their types in a type-level list, but that list should really be regarded as a set. However, worms lurk under this stone. If we have a more flexible notion of equality, how can we be sure that this more inclusive equality is always respected? Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context, everything still works. Sadly, there is no way to guarantee such a property. If (==) is to be useful in a type system, we would need such a guarantee. (By "useful", I mean that this is implementable: reifyEq :: ((a == b) ~ True, Typeable a, Typeable b) => a :~: b.) This brings us to the doorstep of higher inductive types -- a door that might be fun to enter, but is a long long way off.

In sum, I argue for David's first, inextensible version.

By the way, nothing about this requires TypeInType. If I had thought of David's version (that splits apart type applications) in 2013, I probably would have implemented (==) that way.

Richard

On Aug 10, 2017, at 9:00 PM, David Feuer <[hidden email]> wrote:

I tend to agree with you, although I don't think () is a compelling argument. Rather,  it reuses the name == that Haskellers are accustomed to defining flexibly. But for that same reason, as well as the convenience, I do think we should consider using a kind class. That way things at the type level look pretty much like they do at the term level.

On Aug 10, 2017 10:59 AM, "Ryan Scott" <[hidden email]> wrote:
Personally, I'd be more inclined towards latter approach (in
https://phabricator.haskell.org/D3837). After all, one of the key
properties of (==) (for which the Haddocks even make a special note)
is that it does not attempt to provide an instance that works for
every possible kind. Indeed, as you've discovered, there are cases
when it doesn't make sense to use DefaultEq, such as for ().

I'll tentatively give my support for D3837, although I'd be curious to
hear what Richard has to say about this (since I'm reasonably
confident he gave (==) its current implementation).

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




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

Re: Let's rework Data.Type.Equality.==

David Feuer
In reply to this post by David Feuer
Oh, one more thing, Richard. You say that this doesn't need
TypeInType, but I wasn't able to make the polykinded recursion work
without it. Could you show how that might be done? Maybe I missed
something.

On Thu, Aug 10, 2017 at 12:29 AM, David Feuer <[hidden email]> wrote:

> The (==) type family in Data.Type.Equality was designed largely to calculate
> structural equality of types. However, limitations of GHC's type system at
> the type prevented this from being fully realized. Today, with TypeInType,
> we can actually do it, replacing the boatload of ad hoc instances like so:
>
> type (a :: k) == (b :: k) = Equal k a b
> infix 4 ==
>
> type family Equal (k :: Type) (a :: k) (b :: k) where
>  Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
>         Equal (j -> k) f g && Equal j a b
>  Equal k a a = 'True
>  Equal k a b = 'False
>
> This == behaves in a much more uniform way than the current one. I see two
> potential causes for complaint:
>
> 1. For types of kind *, the new version will sometimes fail to reduce when
> the old one succeeded (and vice versa). For example, GHC currently accepts
>
> eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True
> eqeq _ = Refl
>
> while the proposed version does not.
>
> 2. Some users may want non-structural equality on their types for some
> reason. The only example in base is
>
> type instance (a :: ()) == (b :: ()) = 'True
>
> which consists two types of kind () the same even if they're stuck types.
> But perhaps someone wants to implement a non-trivial type-level data
> structure with a special notion of equality.
>
>
> I don't think (1) is really worth worrying too much about. For (2), if users
> want to have control, we could at least use a mechanism similar to the above
> to make the obvious instances easier to write.
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Let's rework Data.Type.Equality.==

David Feuer
In reply to this post by Richard Eisenberg-4
On Fri, Aug 11, 2017 at 11:39 AM, Richard Eisenberg <[hidden email]> wrote:
> If (==) is to be useful
> in a type system, we would need such a guarantee. (By "useful", I mean that
> this is implementable:
>
>   reifyEq :: forall a b. ((a == b) ~ True, Typeable a, Typeable b)
>           => a :~: b
[The above is edited slightly]

Let's get back to this for a moment. I tried actually implementing
this for the simple polykinded version you suggested on my
differential:

    infix 4 ==
    type family (a :: k) == (b :: k) :: Bool where
      f a == g b = f == g && a == b
      a == a = 'True
      _ == _ = 'False

Sadly, it doesn't seem to be possible to really do it properly. First,
there's no way
to prove (f == g) ~ 'True or (x == y) ~ 'True from just (f x == g y) ~
'True. The latter
reduces to (f == g && x == y) ~ 'True, but (&&) is not a constructive
"and", so we can't
actually extract any information from it. Thus we can't work from top to bottom.

Second, pattern matching on TypeReps can only expose
equality and not inequality (as we have no first-class notion of
inequality). So if we
try to work from bottom to top,

    foo :: TypeRep a -> TypeRep b -> Either ((a == b) :~: 'False) ((a
== b) :~: 'True)

we will get well and thoroughly stuck on the non-recursive cases.

So the only way I see to implement reifyEq is

    reifyEq = case eqTypeRep (typeRep :: TypeRep a) (typeRep :: TypeRep b) of
                Just HRefl -> Refl
                Nothing -> error "unreachable"

That doesn't really seem terribly satisfying.
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries