Joachim Breitner | 18 Aug 19:45 2013
Picon

Marking type constructor arguments as nominal (e.g. Set)

Hi,

now that roles are in HEAD, I could play around a bit with it. They were
introduced to solve the unsoundness of newtype deriving, but there is
also the problem of abstraction: If I define a set type based on an ord
instance, e.g.

        data Set a = Set a -- RHS here just for demonstration

the I don’t want my users to replace a "Set Int" by a "Set (Down Int)",
even though the latter is a newtype of the former. This can be prevented
by forcing the role of "a" to be Nominal (and not Representational, as
it is by default). What I just noticed is that one does not even have to
introduce new syntax for it, one can just use:

        type family NominalArg x
        type instance (NominalArg x) = x
        data Set' a = Set' (NominalArg a)

and get different roles; here the excerpt from --show-iface (is there an
easier way to see role annotations):

        5b7b2f7c3883ef0d9fc7934ac56c4805
          data Set a <at> R
        [..]
        8e15d783d58c18b8205191ed3fd87e27
          data Set' a <at> N

The type family does not get into the way, e.g.

(Continue reading)

Nicolas Frisby | 18 Aug 22:00 2013
Picon

Re: Marking type constructor arguments as nominal (e.g. Set)

Is the non-injectivity not an issue here because the type family application gets immediately simplified?


On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner <mail <at> joachim-breitner.de> wrote:
Hi,

now that roles are in HEAD, I could play around a bit with it. They were
introduced to solve the unsoundness of newtype deriving, but there is
also the problem of abstraction: If I define a set type based on an ord
instance, e.g.

        data Set a = Set a -- RHS here just for demonstration

the I don’t want my users to replace a "Set Int" by a "Set (Down Int)",
even though the latter is a newtype of the former. This can be prevented
by forcing the role of "a" to be Nominal (and not Representational, as
it is by default). What I just noticed is that one does not even have to
introduce new syntax for it, one can just use:

        type family NominalArg x
        type instance (NominalArg x) = x
        data Set' a = Set' (NominalArg a)

and get different roles; here the excerpt from --show-iface (is there an
easier way to see role annotations):

        5b7b2f7c3883ef0d9fc7934ac56c4805
          data Set a <at> R
        [..]
        8e15d783d58c18b8205191ed3fd87e27
          data Set' a <at> N

The type family does not get into the way, e.g.

        conv (Set a) = Set' a

works as usual.

(I now also notice that the parser actually supports role annotations...
but still a nice, backward-compatible trick here).

Greetings,
Joachim

--
Joachim “nomeata” Breitner
  mail <at> joachim-breitner.dehttp://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Joachim Breitner | 18 Aug 22:37 2013
Picon

Re: Marking type constructor arguments as nominal (e.g. Set)

Hi,

not sure – where would injectivity be needed?

Greetings,
Joachim

Am Sonntag, den 18.08.2013, 15:00 -0500 schrieb Nicolas Frisby:
> Is the non-injectivity not an issue here because the type family
> application gets immediately simplified?
>
> 
> On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner
> <mail <at> joachim-breitner.de> wrote:
>         Hi,
>         
>         now that roles are in HEAD, I could play around a bit with it.
>         They were
>         introduced to solve the unsoundness of newtype deriving, but
>         there is
>         also the problem of abstraction: If I define a set type based
>         on an ord
>         instance, e.g.
>         
>                 data Set a = Set a -- RHS here just for demonstration
>         
>         the I don’t want my users to replace a "Set Int" by a "Set
>         (Down Int)",
>         even though the latter is a newtype of the former. This can be
>         prevented
>         by forcing the role of "a" to be Nominal (and not
>         Representational, as
>         it is by default). What I just noticed is that one does not
>         even have to
>         introduce new syntax for it, one can just use:
>         
>                 type family NominalArg x
>                 type instance (NominalArg x) = x
>                 data Set' a = Set' (NominalArg a)
>         
>         and get different roles; here the excerpt from --show-iface
>         (is there an
>         easier way to see role annotations):
>         
>                 5b7b2f7c3883ef0d9fc7934ac56c4805
>                   data Set a <at> R
>                 [..]
>                 8e15d783d58c18b8205191ed3fd87e27
>                   data Set' a <at> N
>         
>         The type family does not get into the way, e.g.
>         
>                 conv (Set a) = Set' a
>         
>         works as usual.
>         
>         (I now also notice that the parser actually supports role
>         annotations...
>         but still a nice, backward-compatible trick here).
>         
>         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
>         
>         _______________________________________________
>         Glasgow-haskell-users mailing list
>         Glasgow-haskell-users <at> haskell.org
>         http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>         
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users <at> haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

--

-- 
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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Nicolas Frisby | 18 Aug 22:54 2013
Picon

Re: Marking type constructor arguments as nominal (e.g. Set)

Non-injectivity of type families sometimes hinders type inference. Consider

> Set' (Set.singleton 'c')

Naively, we only know that (Char ~ NominalArg a). Since type families are not necessarily injective, this usually means we cannot determine the type variable `a' from this constraint. However, since the NominalArg instance is parametric in `a', I suspect GHC might successfully infer (Char ~ a) in this case.

… A quick ghci test confirms that GHC does infer (Char ~ a) here. I apologize for not just experimenting in the first place, but maybe this email will save someone slightly more time than is required to read it. :P

On Sun, Aug 18, 2013 at 3:37 PM, Joachim Breitner <mail <at> joachim-breitner.de> wrote:
Hi,

not sure – where would injectivity be needed?

Greetings,
Joachim

Am Sonntag, den 18.08.2013, 15:00 -0500 schrieb Nicolas Frisby:
> Is the non-injectivity not an issue here because the type family
> application gets immediately simplified?
>
>
> On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner
> <mail <at> joachim-breitner.de> wrote:
>         Hi,
>
>         now that roles are in HEAD, I could play around a bit with it.
>         They were
>         introduced to solve the unsoundness of newtype deriving, but
>         there is
>         also the problem of abstraction: If I define a set type based
>         on an ord
>         instance, e.g.
>
>                 data Set a = Set a -- RHS here just for demonstration
>
>         the I don’t want my users to replace a "Set Int" by a "Set
>         (Down Int)",
>         even though the latter is a newtype of the former. This can be
>         prevented
>         by forcing the role of "a" to be Nominal (and not
>         Representational, as
>         it is by default). What I just noticed is that one does not
>         even have to
>         introduce new syntax for it, one can just use:
>
>                 type family NominalArg x
>                 type instance (NominalArg x) = x
>                 data Set' a = Set' (NominalArg a)
>
>         and get different roles; here the excerpt from --show-iface
>         (is there an
>         easier way to see role annotations):
>
>                 5b7b2f7c3883ef0d9fc7934ac56c4805
>                   data Set a <at> R
>                 [..]
>                 8e15d783d58c18b8205191ed3fd87e27
>                   data Set' a <at> N
>
>         The type family does not get into the way, e.g.
>
>                 conv (Set a) = Set' a
>
>         works as usual.
>
>         (I now also notice that the parser actually supports role
>         annotations...
>         but still a nice, backward-compatible trick here).
>
>         Greetings,
>         Joachim
>
>         --
>         Joachim “nomeata” Breitner
>           mail <at> joachim-breitner.dehttp://www.joachim-breitner.de/
>           Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
>           Debian Developer: nomeata <at> debian.org
>
>         _______________________________________________
>         Glasgow-haskell-users mailing list
>         Glasgow-haskell-users <at> haskell.org
>         http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users <at> haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

--
Joachim “nomeata” Breitner
  mail <at> joachim-breitner.dehttp://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 19 Aug 03:24 2013

Re: Marking type constructor arguments as nominal (e.g. Set)

The recommended way to do this (force a Nominal parameter) is

> {-# LANGUAGE RoleAnnotations #-}
> data Set a <at> N = Set a

The  <at> N annotation forces `a`'s role to be Nominal, as desired, but makes no other change to the type. Note
that role annotations can only "increase" roles -- you can't use role annotations to force, say, a type
parameter to a GADT to have role R. You can read http://ghc.haskell.org/trac/ghc/wiki/Roles or my
recent blog post http://typesandkinds.wordpress.com/2013/08/15/roles-a-new-feature-of-ghc/
for more introduction.

To see the roles that GHC assigns to type variables, I've used -ddump-tc. The role annotations are all
printed in the output.

Richard

On Aug 18, 2013, at 1:45 PM, Joachim Breitner wrote:

> Hi,
> 
> now that roles are in HEAD, I could play around a bit with it. They were
> introduced to solve the unsoundness of newtype deriving, but there is
> also the problem of abstraction: If I define a set type based on an ord
> instance, e.g.
> 
>        data Set a = Set a -- RHS here just for demonstration
> 
> the I don’t want my users to replace a "Set Int" by a "Set (Down Int)",
> even though the latter is a newtype of the former. This can be prevented
> by forcing the role of "a" to be Nominal (and not Representational, as
> it is by default). What I just noticed is that one does not even have to
> introduce new syntax for it, one can just use:
> 
>        type family NominalArg x
>        type instance (NominalArg x) = x
>        data Set' a = Set' (NominalArg a)
> 
> and get different roles; here the excerpt from --show-iface (is there an
> easier way to see role annotations):
> 
>        5b7b2f7c3883ef0d9fc7934ac56c4805
>          data Set a <at> R
>        [..]
>        8e15d783d58c18b8205191ed3fd87e27
>          data Set' a <at> N
> 
> The type family does not get into the way, e.g.
> 
>        conv (Set a) = Set' a
> 
> works as usual.
> 
> (I now also notice that the parser actually supports role annotations...
> but still a nice, backward-compatible trick here).
> 
> 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
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users <at> haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 19 Aug 10:34 2013
Picon

RE: Marking type constructor arguments as nominal (e.g. Set)

Correct. For the "newtype wrapper" stuff you could simply omit a "deriving( NT )" on Set.  But the role
annotation *also* prevents bogus newtype-deriving, as you are pointing out.  Eg

	class C a where
	  foo :: Set a -> a

	instance C Int where ...

	newtype Age = MkAge Int deriving( C )
		-- BOGUS deriving

Might you or Richard add an example like this to the user manual section?  It's far from obvious!

Simon

| -----Original Message-----
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| bounces <at> haskell.org] On Behalf Of Joachim Breitner
| Sent: 18 August 2013 18:46
| To: glasgow-haskell-users <at> haskell.org
| Subject: Marking type constructor arguments as nominal (e.g. Set)
| 
| Hi,
| 
| now that roles are in HEAD, I could play around a bit with it. They were
| introduced to solve the unsoundness of newtype deriving, but there is
| also the problem of abstraction: If I define a set type based on an ord
| instance, e.g.
| 
|         data Set a = Set a -- RHS here just for demonstration
| 
| the I don’t want my users to replace a "Set Int" by a "Set (Down Int)",
| even though the latter is a newtype of the former. This can be prevented
| by forcing the role of "a" to be Nominal (and not Representational, as
| it is by default). What I just noticed is that one does not even have to
| introduce new syntax for it, one can just use:
| 
|         type family NominalArg x
|         type instance (NominalArg x) = x
|         data Set' a = Set' (NominalArg a)
| 
| and get different roles; here the excerpt from --show-iface (is there an
| easier way to see role annotations):
| 
|         5b7b2f7c3883ef0d9fc7934ac56c4805
|           data Set a <at> R
|         [..]
|         8e15d783d58c18b8205191ed3fd87e27
|           data Set' a <at> N
| 
| The type family does not get into the way, e.g.
| 
|         conv (Set a) = Set' a
| 
| works as usual.
| 
| (I now also notice that the parser actually supports role annotations...
| but still a nice, backward-compatible trick here).
| 
| 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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane