Advice about TcDeriv

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

Advice about TcDeriv

Joachim Breitner-2
Hi,

to support deriving NT instances properly, TcDeriv needs to be modified.
But there are some structural obstacles: So far, all classes which had
to be had the ?type of interest? as their only type argument. Therefore,
DerivSpec, the data structure in that file, carries information about
what instances to derive, in the field dc_tc :: TyCon.

But with NT it is different:
 * It has two parameters,
 * the type of interest is likely not the last parameter (e.g. NT Age Int)
 * and it can happen that there is a type variable in the last parameter
   (e.g. NT Int a => NT Age a).
All that is difficult to squeeze into the existing data structure.

The data type also has the ds_tys :: [Type] parameter, which contains
all type parameters to the class (e.g. [Int, a]). So at first I thought
about simply removing dc_tc and use the data from (last ds_tys) whenever
needed. But in the case of type families, ds_tc is not just the type
constructor of (last ds_tys), but rather what it resolves to.

So before I rewrite lots of code there, I?d like to get some advice:
Should I extend the DerivSpec to support multi-parameter-typeclasses
(and figure out how to support data families here), or rather bypass the
whole lot and handle NT instance generation separately? Or is there
maybe another, more elegant way?

Thanks,
Joachim

--
Joachim ?nomeata? Breitner
  mail at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130819/af0b5019/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Advice about TcDeriv

Simon Peyton Jones
The more I think about this, the more I wonder if we shouldn't treat NT in a similar way that we treat (~); that is, with built-in rules.  The point is, we use
   (a) roles, and
   (b) visibility of the data constructor
to control abstraction via existence/visibility of the instance. We don't really need a third mechanism
   (c) the presence or absence of a 'deriving' clause

Instead, it can syntactically be a class, but be treateded rather like the SingI class which has an infinite number of instances -- that is, the type checker has a built-in way of simplifying NT constraints.

For example, the typechecker simplifies
        [s] ~ [t]
to
        s ~ t
(This is just unification.)  Similarly it can simplify
        NT [s] [t]
to
        NT s t
(in a role-aware way, of course).

I think this will end up being a lot simpler than trying to push it through the full 'deriving' mechanism.

Does that make sense?

Simon


| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
| Joachim Breitner
| Sent: 19 August 2013 15:19
| To: ghc-devs
| Subject: Advice about TcDeriv
|
| Hi,
|
| to support deriving NT instances properly, TcDeriv needs to be modified.
| But there are some structural obstacles: So far, all classes which had
| to be had the ?type of interest? as their only type argument. Therefore,
| DerivSpec, the data structure in that file, carries information about
| what instances to derive, in the field dc_tc :: TyCon.
|
| But with NT it is different:
|  * It has two parameters,
|  * the type of interest is likely not the last parameter (e.g. NT Age
| Int)
|  * and it can happen that there is a type variable in the last parameter
|    (e.g. NT Int a => NT Age a).
| All that is difficult to squeeze into the existing data structure.
|
| The data type also has the ds_tys :: [Type] parameter, which contains
| all type parameters to the class (e.g. [Int, a]). So at first I thought
| about simply removing dc_tc and use the data from (last ds_tys) whenever
| needed. But in the case of type families, ds_tc is not just the type
| constructor of (last ds_tys), but rather what it resolves to.
|
| So before I rewrite lots of code there, I?d like to get some advice:
| Should I extend the DerivSpec to support multi-parameter-typeclasses
| (and figure out how to support data families here), or rather bypass the
| whole lot and handle NT instance generation separately? Or is there
| maybe another, more elegant way?
|
| Thanks,
| Joachim
|
| --
| Joachim ?nomeata? Breitner
|   mail at joachim-breitner.de ? http://www.joachim-breitner.de/
|   Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
|   Debian Developer: nomeata at debian.org

Reply | Threaded
Open this post in threaded view
|

Advice about TcDeriv

Joachim Breitner-2
Good morning,

Am Dienstag, den 20.08.2013, 07:24 +0000 schrieb Simon Peyton-Jones:

> The more I think about this, the more I wonder if we shouldn't treat
> NT in a similar way that we treat (~); that is, with built-in rules.
> The point is, we use
>    (a) roles, and
>    (b) visibility of the data constructor
> to control abstraction via existence/visibility of the instance. We
> don't really need a third mechanism
>    (c) the presence or absence of a 'deriving' clause
>
> Instead, it can syntactically be a class, but be treateded rather like
> the SingI class which has an infinite number of instances -- that is,
> the type checker has a built-in way of simplifying NT constraints.
>
> For example, the typechecker simplifies
> [s] ~ [t]
> to
> s ~ t
> (This is just unification.)  Similarly it can simplify
> NT [s] [t]
> to
> NT s t
> (in a role-aware way, of course).
>
> I think this will end up being a lot simpler than trying to push it
> through the full 'deriving' mechanism.
>
> Does that make sense?

it is certainly true that there are many obstacles when trying to use
the normal class mechanisms here.

One of the main reason we wanted to use (standalone) deriving instances
(or even the NT type constructor idea earlier) was to give library
authors a way to communicate their abstractions, to avoid the coercion
between (Set Int) and (Set (Down Int)). But thanks to Richard?s role
annotation, this can be prevented by annotating the Set?s type variables
with @N. So far so good.

Questions:
 * Will this annotation have other, possibly unwanted effects?
 * Should we also simplify constraints like (NT Age a) to (NT Int a)
automatically and built-in, or do we still want the user to first tell
us that we should do so?
 * What about the ?only do it if constructors are in scope? idea ? if
the typechecker creates these instances on the fly, it might do so for
modules where the constructors are not in scope (either because they are
private, or simply because they have not been imported).

Greetings,
Joachim



--
Joachim ?nomeata? Breitner
  mail at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130820/71937cea/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Advice about TcDeriv

Simon Peyton Jones
| Questions:
|  * Will this annotation have other, possibly unwanted effects?

The role annotation will have exactly the *right* effect; in particular, it'll prevent you saying
        class Foo a where
           foo :: Set a -> Set a

        instance Foo Int where ...
        newtype Age = MkAge Int deriving( Foo )

|  * Should we also simplify constraints like (NT Age a) to (NT Int a)
| automatically and built-in, or do we still want the user to first tell
| us that we should do so?

I think we should automatically simplify it.

|  * What about the ?only do it if constructors are in scope? idea ? if
| the typechecker creates these instances on the fly, it might do so for
| modules where the constructors are not in scope (either because they are
| private, or simply because they have not been imported).

It'll simplify (NT Age a) to (NT Int a) when, and only when, MkAge is in scope.  So visibility of the data constructor says just when you want that instance to work.  I think that seems fine to me.

Simon

| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
| Joachim Breitner
| Sent: 20 August 2013 08:37
| To: ghc-devs
| Subject: Re: Advice about TcDeriv
|
| Good morning,
|
| Am Dienstag, den 20.08.2013, 07:24 +0000 schrieb Simon Peyton-Jones:
| > The more I think about this, the more I wonder if we shouldn't treat
| > NT in a similar way that we treat (~); that is, with built-in rules.
| > The point is, we use
| >    (a) roles, and
| >    (b) visibility of the data constructor
| > to control abstraction via existence/visibility of the instance. We
| > don't really need a third mechanism
| >    (c) the presence or absence of a 'deriving' clause
| >
| > Instead, it can syntactically be a class, but be treateded rather like
| > the SingI class which has an infinite number of instances -- that is,
| > the type checker has a built-in way of simplifying NT constraints.
| >
| > For example, the typechecker simplifies
| > [s] ~ [t]
| > to
| > s ~ t
| > (This is just unification.)  Similarly it can simplify
| > NT [s] [t]
| > to
| > NT s t
| > (in a role-aware way, of course).
| >
| > I think this will end up being a lot simpler than trying to push it
| > through the full 'deriving' mechanism.
| >
| > Does that make sense?
|
| it is certainly true that there are many obstacles when trying to use
| the normal class mechanisms here.
|
| One of the main reason we wanted to use (standalone) deriving instances
| (or even the NT type constructor idea earlier) was to give library
| authors a way to communicate their abstractions, to avoid the coercion
| between (Set Int) and (Set (Down Int)). But thanks to Richard?s role
| annotation, this can be prevented by annotating the Set?s type variables
| with @N. So far so good.
|
| Questions:
|  * Will this annotation have other, possibly unwanted effects?
|  * Should we also simplify constraints like (NT Age a) to (NT Int a)
| automatically and built-in, or do we still want the user to first tell
| us that we should do so?
|  * What about the ?only do it if constructors are in scope? idea ? if
| the typechecker creates these instances on the fly, it might do so for
| modules where the constructors are not in scope (either because they are
| private, or simply because they have not been imported).
|
| Greetings,
| Joachim
|
|
|
| --
| Joachim ?nomeata? Breitner
|   mail at joachim-breitner.de ? http://www.joachim-breitner.de/
|   Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
|   Debian Developer: nomeata at debian.org

Reply | Threaded
Open this post in threaded view
|

Advice about TcDeriv

Joachim Breitner-2
Hi,

Am Dienstag, den 20.08.2013, 07:43 +0000 schrieb Simon Peyton-Jones:
> | Questions:
> |  * Will this annotation have other, possibly unwanted effects?
>
> The role annotation will have exactly the *right* effect;

great.

> |  * Should we also simplify constraints like (NT Age a) to (NT Int a)
> | automatically and built-in, or do we still want the user to first tell
> | us that we should do so?
>
> I think we should automatically simplify it.

ok, so in summary the user will never see instance declarations
referring to NT in any way, but just one function
        castNT :: NT a b => a -> b
which will just do the right thing (or nothing at all).

> |  * What about the ?only do it if constructors are in scope? idea ? if
> | the typechecker creates these instances on the fly, it might do so for
> | modules where the constructors are not in scope (either because they are
> | private, or simply because they have not been imported).
>
> It'll simplify (NT Age a) to (NT Int a) when, and only when, MkAge is
> in scope.  So visibility of the data constructor says just when you
> want that instance to work.  I think that seems fine to me.

I?m a bit uneasy about this; it means that one cannot export the ability
to do these casts without exposing everything.

Also it leads to a surprising behavior with regard to import lists:
Consider a module M which wants to use "castNT :: T -> [Int]" where
newtype T = T [Age]" is defined elsewhere. For this to work, I not only
have to "import ... (T(T))", but also "import ... (Age(MkAge))", even
though I don?t see anything about Age in my code.

Also, the typechecker will have to register a use of all these
constructors during typechecking ? is there precedence for that?

I guess we can start with this more restricted, but definitely safe
variant and see how much it hinders practical use.

Greetings,
Joachim

--
Joachim ?nomeata? Breitner
  mail at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130820/a5ea0e30/attachment.pgp>