We need to add role annotations for 7.8

Andreas Abel andreas.abel at ifi.lmu.de
Tue Mar 25 08:28:57 UTC 2014

Hash: SHA1

As someone completely oblivious on this development in Haskell until
now, but researching myself in the same direction (on the distinction
of computational, irrelevant, and parametric arguments in Agda), I am
allowing myself some comments on the process, and the syntax
discussion given in the paper


1. The alternative of using a pragma as syntax is dismissed with the

"We felt that, in several years, we would regret this
decision. Backwards-compatibility would no longer be an
issue, and we would be stuck with a pragma syntax for a
core language feature."

I strongly disagree.  One can introduce a pragma syntax first, for
smooth backward compatibility, and after the feature has passed the
test of time, still introduce a proper, "first-class" syntax.  If role
annotations become standard, introduction of a proper syntax instead
of ugly pragmas will be received with applause, unlike now, where you
burden ugly CPP-ifs onto the library developers.

You could do for now with a pragma-like declaration

 {-# TYPEROLE identifier role ... role #-}


 {-# TYPE_ROLE identifier role ... role #-}

instead of the declaration

  type role identifier role ... role

2. The chosen role names mean nothing to me.  It feels a bit like the
term "delegate" used in C# instead of just speaking of a higher-order
function.  Looking at the semantics, I find the following translation

  nominal = computational

    That is, the choice of type expression has a computational effect
(like a different implementation of Ord).

  representational = parametric

    The choice of type expression is parametric, i.e., does not lead
to other choices, but is purely propagated through.

Further, "representational" is a bit long for a keyword.  'nominal'
invokes the exact opposite association for me than it means.  In
nominal calculi (Pitts et al), everything is *parametric* in the
choice of names.

For introducing a non-backwards compatible language feature, this
process feels rushed, imho.

You might wanna pull the break before the release.


On 25.03.2014 04:26, Richard Eisenberg wrote:
> I have a few responses to various themes in this thread, but
> nothing terribly unexpected:
> - The introduction of roles is the end of the story that began with
> the discovery of bug #1496. The alternative would be to do away
> with GND. `coerce` is just a convenient application of roles, not
> the reason they were introduced.
> - The concrete syntax for role ascriptions was debated in public,
> in bug #8185. There is further discussion of the design choice in
> the appendix of the extended version of our recent draft paper on
> the subject: 
> www.cis.upenn.edu/~eir/papers/2014/coercible/coercible-ext.pdf 
> <http://www.cis.upenn.edu/~eir/papers/2014/coercible/coercible-ext.pdf>
I'm afraid it's too late now to make changes. I don't love what we
> ended up with, but I believe it's the best syntax that was
> proposed.
> - I agree with Simon that `coerce` is quite a bit safer than 
> `unsafeCoerce`. Under the assumption that all libraries are
> written correctly (that is, with proper role annotations), `coerce`
> is in fact fully safe.
> - I surely recognize why and how this causes a Major Pain for Mark,
> and for other library maintainers. I wish there were an easier
> solution. However, I will perhaps repeat others in saying that a
> library that doesn't add role annotations is no more wrong in 7.8
> than it was since GND was introduced. The only difference with 7.8
> is that, now, there is a way to be right.
> Richard
> On Mar 24, 2014, at 9:32 PM, Edward A Kmett wrote:
>> Fair enough. I did try to convey that in the following sentence
>> about how it at least enforces representational equality, but I
>> can see how my statement might be taken as understating the
>> importance of that property.
>> Sent from my iPhone
>> On Mar 24, 2014, at 6:57 PM, Simon Peyton Jones
>> <simonpj at microsoft.com <mailto:simonpj at microsoft.com>> wrote:
>>> In that light, `coerce` then can be viewed as a more friendly
>>> but still evil version of unsafeCoerce
>>> Coerce embodies one rather compelling improvement: *it is 
>>> type-sound.*  unsafeCoerce can cause arbitrary seg-faults etc.
>>>  ‘coerce’ cannot.  Call me an old-fashioned “well-typed
>>> programs don’t go wrong” man, but I think that’s a big plus.
>>> Much more than “an occasional situation improvement”.
>>> Granted, “type-sound” doesn’t guarantee “correct”, but then it
>>> never did.
>>> The role machinery doesn’t exactly hoist us on a dilemma – it
>>> merely exposes the dilemma that was there all the time.
>>> Simon
>>> *From:*Edward Kmett [mailto:ekmett at gmail.com] *Sent:* 24 March
>>> 2014 19:11 *To:* Mark Lentczner *Cc:* Simon Peyton Jones;
>>> libraries at haskell.org <mailto:libraries at haskell.org> Libraries;
>>> ghc-devs at haskell.org <mailto:ghc-devs at haskell.org> *Subject:*
>>> Re: We need to add role annotations for 7.8
>>> Mark,
>>> We're currently planning to retain the existing behavior of 
>>> GeneralizedNewtypeDeriving with regards to Safe Haskell. That
>>> is, Safe Haskell and GND still won't mix in 7.8 due to these
>>> same security concerns.
>>> I think a key observation with regards to
>>> GeneralizedNewtypeDeriving is with representational roles as
>>> default the new roles machinery with the representational
>>> default lets you write nothing you couldn't write before. No
>>> new security vulnerabilities are introduced. They were there
>>> all along!
>>> We're also disabling the Safe flag on Data.Coerce. In that
>>> light, `coerce` then can be viewed as a more friendly but still
>>> evil version of unsafeCoerce. It lets you write nothing you
>>> couldn't write before with `unsafeCoerce`. I view it as merely
>>> an occasional situational improvement over the existing
>>> unsafeCoerce in that it at least enforces representational
>>> equality.
>>> Making the default role annotation nominal comes at a very very
>>> real cost. Namely, *all* of generalized newtype deriving
>>> anywhere breaks, and everyone forever will have to put
>>> annotations in to fix it.
>>> The 'backwards' representational default puts the burden on a
>>> small minority of library authors.
>>> I'm not a huge fan of the representational machinery, in that
>>> it hoists us upon this dilemma, but given the choice between
>>> everyone paying in perpetuity and a small minority of skilled
>>> library authors adding a handful of annotations that for the
>>> most part have already been added, and which expose them to no
>>> more risk than they'd had before if they forget, I'm definitely
>>> in favor of the current solution.
>>> -Edward
>>> On Mon, Mar 24, 2014 at 11:26 AM, Mark Lentczner 
>>> <mark.lentczner at gmail.com <mailto:mark.lentczner at gmail.com>>
>>> wrote:
>>> Thanks for the pointers, Simon. I appologize for coming to
>>> this quite so late... I didn't realize the global impact of
>>> this feature.
>>> From a "meaning" perspective, I'm agnostic on the default.
>>> From a "engineering" perspective, I want a default that "does
>>> a good enough, reasonably safe thing" if programmers ignore
>>> the feature.
>>> The later is subtle as there are different vantage points for 
>>> different developers. In the Platform, we have many libraries 
>>> that we are encouraging both end-programmers, and other
>>> library authors to make use of and depend on extensively. This
>>> means those libraries have to work for both programmers that
>>> are ignoring the feature, and those that use it. In that later
>>> case, there is the even more subtle distinction of those that
>>> use the feature for their own code, and those that use it in
>>> libraries they make available.
>>> The later case is issue: It seems a real mess if a library
>>> author who wanted to use the new feature, had to circumvent a
>>> HP library because it didn't annotate. Similar thought
>>> experiment: What would be the downside if containers didn't
>>> annotate? Would that just make the feature unusable because
>>> everything uses containers?
>>> To put it more directly: with the satus-quo default of 
>>> representations, what is the down side if a library, a widely 
>>> used library, doesn't bother to annotate? What would be the
>>> loss if containers didn't annotate? (I know it did, this is
>>> the thought experiment... because I've got 30+ libraries in HP
>>> that are in this boat.)
>>> _______________________________________________ Libraries
>>> mailing list Libraries at haskell.org
>>> <mailto:Libraries at haskell.org> 
>>> http://www.haskell.org/mailman/listinfo/libraries
>> _______________________________________________ Libraries mailing
>> list Libraries at haskell.org <mailto:Libraries at haskell.org> 
>> http://www.haskell.org/mailman/listinfo/libraries
> _______________________________________________ Libraries mailing
> list Libraries at haskell.org 
> http://www.haskell.org/mailman/listinfo/libraries

- -- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/


More information about the Libraries mailing list