Type-level generics

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

Type-level generics

David Feuer-2
I've been thinking for several weeks that it might be useful to offer
type-level generics. That is, along with

to :: Rep a k -> a
from :: a -> Rep a

perhaps we should also derive

type family To (r :: Rep a x) :: a
type family From (v :: a) :: Rep a x

This would allow us to use generic programming at the type level
For example, we could write a generic ordering family:

class OrdK (k :: Type) where
  type Compare (x :: k) (y :: k) :: Ordering
  type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From y)

instance OrdK Nat where
  type Compare x y = CmpNat x y

instance OrdK Symbol where
  type Compare x y = CmpSymbol x y

instance OrdK [a] -- No implementation needed!

type family GenComp k (x :: k) (y :: k) :: Ordering where
  GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y
  GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y
  GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n
  GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n
  GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT
  GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT
  GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) =
    PComp (GenComp (x p) x1 x2) (y p) y1 y2
  GenComp (U1 p) _ _ = 'EQ
  GenComp (V1 p) _ _ = 'EQ

type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering where
  PComp 'EQ k x y = GenComp k x y
  PComp x _ _ _ = x

For people who want to play around with the idea, here are the definitions of To and From
for lists:

  To ('M1 ('L1 ('M1 'U1))) = '[]
  To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) = x ': xs
  From '[] = 'M1 ('L1 ('M1 'U1))
  From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))

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

Re: Type-level generics

David Feuer-2
One other thing I should add. We'd really, really like to have isomorphism
evidence:

  toThenFrom :: pr p -> To (From x :: Rep a p) :~: (x :: a)
  fromThenTo :: pr1 a -> pr2 (r :: Rep a p) -> From (To r :: a) :~: (r :: Rep a p)

I believe these would make the To and From families considerably more
useful. Unfortunately, while I'm pretty sure those are completely legit for
any Generic-derived types, I don't think there's ever any way to prove
them in Haskell! Ugh.

On Thursday, August 31, 2017 3:37:15 PM EDT David Feuer wrote:

> I've been thinking for several weeks that it might be useful to offer
> type-level generics. That is, along with
>
> to :: Rep a k -> a
> from :: a -> Rep a
>
> perhaps we should also derive
>
> type family To (r :: Rep a x) :: a
> type family From (v :: a) :: Rep a x
>
> This would allow us to use generic programming at the type level
> For example, we could write a generic ordering family:
>
> class OrdK (k :: Type) where
>   type Compare (x :: k) (y :: k) :: Ordering
>   type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From y)
>
> instance OrdK Nat where
>   type Compare x y = CmpNat x y
>
> instance OrdK Symbol where
>   type Compare x y = CmpSymbol x y
>
> instance OrdK [a] -- No implementation needed!
>
> type family GenComp k (x :: k) (y :: k) :: Ordering where
>   GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y
>   GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y
>   GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n
>   GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n
>   GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT
>   GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT
>   GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) =
>     PComp (GenComp (x p) x1 x2) (y p) y1 y2
>   GenComp (U1 p) _ _ = 'EQ
>   GenComp (V1 p) _ _ = 'EQ
>
> type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering where
>   PComp 'EQ k x y = GenComp k x y
>   PComp x _ _ _ = x
>
> For people who want to play around with the idea, here are the definitions of To and From
> for lists:
>
>   To ('M1 ('L1 ('M1 'U1))) = '[]
>   To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) = x ': xs
>   From '[] = 'M1 ('L1 ('M1 'U1))
>   From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))
>
> David


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

Re: Type-level generics

Oleg Grenrus
Seems that by making a class you can "prove" by requiring this isomorphism:

    class (To r ~ v, From v ~ r) -- , To (From v :: Rep a x) ~ v)
        => TypeGeneric a (r :: Rep a x) (v :: a)
      where
        type To r :: a
        type From v :: Rep a x

See attachment or [1] for the whole file.

Cheers, Oleg

[1]: https://gist.github.com/phadej/fab7c627efbca5cba16ba258c8f10337

On 31.08.2017 23:22, David Feuer wrote:

> One other thing I should add. We'd really, really like to have isomorphism
> evidence:
>
>   toThenFrom :: pr p -> To (From x :: Rep a p) :~: (x :: a)
>   fromThenTo :: pr1 a -> pr2 (r :: Rep a p) -> From (To r :: a) :~: (r :: Rep a p)
>
> I believe these would make the To and From families considerably more
> useful. Unfortunately, while I'm pretty sure those are completely legit for
> any Generic-derived types, I don't think there's ever any way to prove
> them in Haskell! Ugh.
>
> On Thursday, August 31, 2017 3:37:15 PM EDT David Feuer wrote:
>> I've been thinking for several weeks that it might be useful to offer
>> type-level generics. That is, along with
>>
>> to :: Rep a k -> a
>> from :: a -> Rep a
>>
>> perhaps we should also derive
>>
>> type family To (r :: Rep a x) :: a
>> type family From (v :: a) :: Rep a x
>>
>> This would allow us to use generic programming at the type level
>> For example, we could write a generic ordering family:
>>
>> class OrdK (k :: Type) where
>>   type Compare (x :: k) (y :: k) :: Ordering
>>   type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From y)
>>
>> instance OrdK Nat where
>>   type Compare x y = CmpNat x y
>>
>> instance OrdK Symbol where
>>   type Compare x y = CmpSymbol x y
>>
>> instance OrdK [a] -- No implementation needed!
>>
>> type family GenComp k (x :: k) (y :: k) :: Ordering where
>>   GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y
>>   GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y
>>   GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n
>>   GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n
>>   GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT
>>   GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT
>>   GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) =
>>     PComp (GenComp (x p) x1 x2) (y p) y1 y2
>>   GenComp (U1 p) _ _ = 'EQ
>>   GenComp (V1 p) _ _ = 'EQ
>>
>> type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering where
>>   PComp 'EQ k x y = GenComp k x y
>>   PComp x _ _ _ = x
>>
>> For people who want to play around with the idea, here are the definitions of To and From
>> for lists:
>>
>>   To ('M1 ('L1 ('M1 'U1))) = '[]
>>   To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) = x ': xs
>>   From '[] = 'M1 ('L1 ('M1 'U1))
>>   From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))
>>
>> David
>
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

type-generics.hs (3K) Download Attachment
signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Type-level generics

Ryan Scott
In reply to this post by David Feuer-2
While we're on the topic, I'll mention that at one point I attempted
to modify the singletons [1] library so that it would automatically
generate promoted (i.e., type-level) and singled versions of Generic
instances for any data type that derived Generic. I wasn't successful,
since it turns out singletons are difficult to adapt to data types
with higher-kinded types [2] and type classes with associated type
families [3], but I did manage to write some examples on a very
limited subset of GHC.Generics in this gist [4].

The promoted version of Generic (PGeneric) in that gist works pretty
much identically to Oleg's version, but with one notable difference: I
don't attempt to put the Generic laws as a superclass of PGeneric.
Instead, I make the laws class methods of the singled version of
Generic (SGeneric). I found it more convenient to do it this way since
I needed to pattern-match on these proofs directly in a generic
implementation of decidable equality, but I'm sure this isn't the only
way it could be done.

Speaking of which, it astounds me that the Generic laws aren't
documented in the Haddocks! We really should do that.

Ryan S.
-----
[1] http://hackage.haskell.org/package/singletons
[2] See the extended discussion in
https://github.com/goldfirere/singletons/issues/150
[3] https://github.com/goldfirere/singletons/issues/198
[4] https://gist.github.com/RyanGlScott/daeb63be7885244d9882dcbb1bbc10cc
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Type-level generics

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

Before starting with generics support at the type level, please first
improve the generics support at the value level. When I looked at it the
last time, there were some apparent leftovers in the form of types or
type parameters never used. In addition, it seems awkward that you have
to pass these p-parameters around when working with types of kind *, and
that there is no possibility to work with types with more than one
parameter. I think that GHC’s approach to generics is very good in
general, but that the GHC.Generics module looks a bit unpolished and ad-
hoc at the moment. Maybe it would be possible to solve the
abovementioned problems using TypeInType.

All the best,
Wolfgang

Am Donnerstag, den 31.08.2017, 15:37 -0400 schrieb David Feuer:

> I've been thinking for several weeks that it might be useful to offer
> type-level generics. That is, along with
>
> to :: Rep a k -> a
> from :: a -> Rep a
>
> perhaps we should also derive
>
> type family To (r :: Rep a x) :: a
> type family From (v :: a) :: Rep a x
>
> This would allow us to use generic programming at the type level
> For example, we could write a generic ordering family:
>
> class OrdK (k :: Type) where
>   type Compare (x :: k) (y :: k) :: Ordering
>   type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From
> y)
>
> instance OrdK Nat where
>   type Compare x y = CmpNat x y
>
> instance OrdK Symbol where
>   type Compare x y = CmpSymbol x y
>
> instance OrdK [a] -- No implementation needed!
>
> type family GenComp k (x :: k) (y :: k) :: Ordering where
>   GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y
>   GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y
>   GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n
>   GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n
>   GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT
>   GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT
>   GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) =
>     PComp (GenComp (x p) x1 x2) (y p) y1 y2
>   GenComp (U1 p) _ _ = 'EQ
>   GenComp (V1 p) _ _ = 'EQ
>
> type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering
> where
>   PComp 'EQ k x y = GenComp k x y
>   PComp x _ _ _ = x
>
> For people who want to play around with the idea, here are the
> definitions of To and From
> for lists:
>
>   To ('M1 ('L1 ('M1 'U1))) = '[]
>   To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) = x ': xs
>   From '[] = 'M1 ('L1 ('M1 'U1))
>   From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))
>
> David
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Type-level generics

Evan Laforge
On Fri, Sep 1, 2017 at 2:23 PM, Wolfgang Jeltsch
<[hidden email]> wrote:
> Hi!
>
> Before starting with generics support at the type level, please first
> improve the generics support at the value level. When I looked at it the
> last time, there were some apparent leftovers in the form of types or
> type parameters never used. In addition, it seems awkward that you have

I was just about to complain about this myself, since every year or so
I go fail to figure out GHC.Generics after tripping over lots of out
of date documentation, confusing type aliases, and obsolete aliases,
and wrong examples, but I just looked again and it seems like
GHC.Generics got a major update in ghc 8.  It looks like there's still
one confusing reference to Par0: "Note how Par0 and Rec0 both being
mapped to K1 allows us to define a uniform instance here. " but at
least it's not tangled up in the already very confusing examples and
signatures.  I think that sentence can be deleted entirely now?  I
have no idea what it's trying to express.

So thanks to whoever did that.  I'll give it another try.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Type-level generics

Ryan Scott
In reply to this post by David Feuer-2
Several good points were brought up. Let me go through them and try to
make sense of what I can:

> When I looked at it the last time, there were some apparent leftovers in the form of types or type parameters never used.

Are you referring to the `p` type parameters that are found in most of
the data types in GHC.Generics? If so, they are most definitely
used—try deriving Generic1 to see this in action! It's true that in
the context of Generic (without the 1 at the end) the `p` isn't used,
but this is by design, as this allows us to share the same
representation types across Generic and Generic1.

> there is no possibility to work with types with more than one parameter.

Quite true. But I posit that engineering GHC.Generics to work with
more than one type parameter at a time is much harder than it sounds.
After all, to profitably work with even a *single* type parameter
(what Generic1 does), we must bring in three additional representation
types: Par1, Rec1, and (:.:), depending on where in the datatype the
last type parameter occurs. If we wanted to have, say, Generic2, we'd
similarly need to be able to work with many more combinations of type
parameter positions, such as:

* data Foo1 a b = Foo1 a b
* data Foo2 a b = Foo2 (Either a b)
* data Foo3 a b = Foo3 (Either b a)
* etc.

A naïve approach would be to tack on another type parameter at the end
of every representation type, and introduce more types to deal with
all the combinations of the first and second type parameter that could
arise. But this approach doesn't scale well—after all, at what number
N do you stop introducing new representation types? So extending
GHC.Generics to deal with more than one type parameter is far from
obvious to me (let alone whether it could be made backwards compatible
with the current API).

> the GHC.Generics module looks a bit unpolished and ad-hoc at the moment.

Yes, quite literally everything in GHC.Generics is one large, ad hoc
hack. But it's also a darn useful one :)

> It looks like there's still one confusing reference to Par0: "Note how Par0 and Rec0 both being mapped to K1 allows us to define a uniform instance here. " but at least it's not tangled up in the already very confusing examples and signatures.  I think that sentence can be deleted entirely now?

Indeed, an earlier part of the documentation in that module mentions
that Par0 was deprecated (and removed, in fact), so we really
shouldn't be mentioning it elsewhere. I'll remove that sentence.

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

Re: Type-level generics

Wolfgang Jeltsch-3
Am Samstag, den 02.09.2017, 11:35 -0400 schrieb Ryan Scott:
> > When I looked at it the last time, there were some apparent
> > leftovers in the form of types or type parameters never used.
>
> Are you referring to the `p` type parameters that are found in most of
> the data types in GHC.Generics?

No, there were really unused things.

> If so, they are most definitely used—try deriving Generic1 to see this
> in action!

I know that they are needed for Generic1, but they are not needed for
Generic.

> It's true that in the context of Generic (without the 1 at the end)
> the `p` isn't used, but this is by design, as this allows us to share
> the same representation types across Generic and Generic1.

It would be great if we could employ kind polymorphism or even type-in-
type to have a single set of representation types, but still no unused
parameters.

> > there is no possibility to work with types with more than one
> > parameter.
>
> Quite true. But I posit that engineering GHC.Generics to work with
> more than one type parameter at a time is much harder than it sounds.
> After all, to profitably work with even a *single* type parameter
> (what Generic1 does), we must bring in three additional representation
> types: Par1, Rec1, and (:.:), depending on where in the datatype the
> last type parameter occurs. If we wanted to have, say, Generic2, we'd
> similarly need to be able to work with many more combinations of type
> parameter positions, such as:
>
> * data Foo1 a b = Foo1 a b
> * data Foo2 a b = Foo2 (Either a b)
> * data Foo3 a b = Foo3 (Either b a)
> * etc.

Actually, I am looking for something even bigger: not just a Generic2
class, but a Generic class that can deal with types of any arity.

> A naïve approach would be to tack on another type parameter at the end
> of every representation type, and introduce more types to deal with
> all the combinations of the first and second type parameter that could
> arise. But this approach doesn't scale well—after all, at what number
> N do you stop introducing new representation types?

We should nowhere stop, but allow an arbitrary number of parameters. ☺
Maybe through striving for a Generic class that works with arbitrary
arities, we will find some deeper pattern, which could relieve us from
having ad-hoc types such as the Foo1, Foo2, and so on you mention above.

> So extending GHC.Generics to deal with more than one type parameter is
> far from obvious to me

It is also far from obvious for me. 😉 I actually think that makin
g GHC.Generics more generic (making it work with types of arbitrary
arity) is a nice research task, not something than can be done very
easily.

>  (let alone whether it could be made backwards compatible with the
> current API).

It should not be backwards compatible. If we insist on backwards
compatibility, we can never arrive at a version that works with types of
any arity.

> > the GHC.Generics module looks a bit unpolished and ad-hoc at the
> > moment.
>
> Yes, quite literally everything in GHC.Generics is one large, ad hoc
> hack. But it's also a darn useful one :)

I am worried that people get so much used to the current interface that
it will be hard to change it for something better later. You already
argued in favor of backwards compatibility. ☹

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

Re: Type-level generics

Ryan Scott
In reply to this post by David Feuer-2
If you're willing to go a completely different route from
GHC.Generics, then you might be interested in the paper Generic
Programming with Multiple Parameters [1] (whose existence I just
learned of—thanks to Pedro, the author, for pointing it out to me). It
does present a single Generic class that is capable of working over
any number of type parameters, although the interface presented is
significantly more complex than the current GHC.Generics.

The only reason I mention backwards compatibility is that if we are
going to introduce a GHC.Generics 2.0 some day, it'd be nice to have a
way to subsume the old interface with the new one, and fortunately,
the aforementioned paper includes an algorithm for doing so. My hope
was that we'd be able to incorporate these ideas into a design that
also grants the ability to write Generic instances for GADTs, but I
don't think GHC has a fancy enough type system to do this
satisfactorily at the moment.

Ryan S.
-----
[1] http://dreixel.net/research/pdf/gpmp_colour.pdf
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Type-level generics

David Feuer-2
In reply to this post by David Feuer-2
Ah, nice. I was actually exploring the vague general idea behind that approach earlier this evening. Magalhães (unsurprisingly) has developed it much much further.



David Feuer
Well-Typed, LLP

-------- Original message --------
From: Ryan Scott <[hidden email]>
Date: 9/2/17 10:36 PM (GMT-05:00)
Subject: Re: Type-level generics

If you're willing to go a completely different route from
GHC.Generics, then you might be interested in the paper Generic
Programming with Multiple Parameters [1] (whose existence I just
learned of—thanks to Pedro, the author, for pointing it out to me). It
does present a single Generic class that is capable of working over
any number of type parameters, although the interface presented is
significantly more complex than the current GHC.Generics.

The only reason I mention backwards compatibility is that if we are
going to introduce a GHC.Generics 2.0 some day, it'd be nice to have a
way to subsume the old interface with the new one, and fortunately,
the aforementioned paper includes an algorithm for doing so. My hope
was that we'd be able to incorporate these ideas into a design that
also grants the ability to write Generic instances for GADTs, but I
don't think GHC has a fancy enough type system to do this
satisfactorily at the moment.

Ryan S.
-----
[1] http://dreixel.net/research/pdf/gpmp_colour.pdf
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

Re: Type-level generics

Wolfgang Jeltsch-3
In reply to this post by Ryan Scott
Am Samstag, den 02.09.2017, 22:36 -0400 schrieb Ryan Scott:
> If you're willing to go a completely different route from
> GHC.Generics, then you might be interested in the paper Generic
> Programming with Multiple Parameters [1] (whose existence I just
> learned of—thanks to Pedro, the author, for pointing it out to me). It
> does present a single Generic class that is capable of working over
> any number of type parameters, although the interface presented is
> significantly more complex than the current GHC.Generics.

Very interesting! I will go and read it.

All the best,
Wolfgang
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs