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
-----BEGIN PGP SIGNED MESSAGE-----
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
http://www.cis.upenn.edu/~eir/papers/2014/coercible/coercible-ext.pdf
1. The alternative of using a pragma as syntax is dismissed with the
argument:
"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 #-}
or
{-# 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.
Cheers,
Andreas
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
http://www2.tcs.ifi.lmu.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/
iEYEARECAAYFAlMxPkkACgkQPMHaDxpUpLNc6QCeLSqyQE/huMc0cBMIL4oJbLQ1
pOgAn3cW4YmP2hrQoMwMtRcmJ6t6jML3
=DnVb
-----END PGP SIGNATURE-----
More information about the Libraries
mailing list