[ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept

[Spiwack, Arnaud]

I think that the proposal makes a great job at listing the issues. It's
quite transparent about this, I'm not sure what I could add.

On Wed, Oct 27, 2021 at 11:29 AM Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> I was indeed confused! Apologies.
>
> But my main point remains: enumerating a list of inconvenient side effects
> and corner cases would be a great service.
>
> Simon
>
> PS: I am leaving Microsoft at the end of November 2021, at which point
> simonpj at microsoft.com will cease to work.  Use simon.peytonjones at gmail.com
> instead.  (For now, it just forwards to simonpj at microsoft.com.)
>
> |  -----Original Message-----
> |  From: Vladislav Zavialov (int-index) <vlad.z.4096 at gmail.com>
> |  Sent: 27 October 2021 10:10
> |  To: Simon Peyton Jones <simonpj at microsoft.com>
> |  Cc: Spiwack, Arnaud <arnaud.spiwack at tweag.io>; Richard Eisenberg
> |  <rae at richarde.dev>; ghc-steering-committee <ghc-steering-
> |  committee at haskell.org>
> |  Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall"
> |  in terms; rec: accept
> |
> |  Simon, perhaps you’re thinking of another proposal that is currently
> |  under committee’s consideration?
> |
> |  Arnaud was commenting on #281, and you seem to be talking about #425.
> |
> |  - Vlad
> |
> |  > On 27 Oct 2021, at 12:05, Simon Peyton Jones via ghc-steering-
> |  committee <ghc-steering-committee at haskell.org> wrote:
> |  >
> |  > There are a lot of inconvenient side effects and corner cases
> |  >
> |  > Arnaud, could you enumerate them?  Even if (as I strongly hope) we
> |  accept this proposal, it’s good to have a concrete list of things to
> |  bear in mind.   I for one do not have such list in my head.
> |  >
> |  > One principle that the proposal espouses (but perhaps does not call
> |  out explicitly) is that it should be possible to write an explicit
> |  binder for every in-scope variable.    So instead of
> |  >                 data T (a :: k -> k) = … I want to write
> |  >                 data T @k (a :: k -> k) = … with an explicit binder
> |  > for k.
> |  >
> |  > So I see the proposal as removing an ad-hoc wart in the language.
> |  But I may be blind to the “inconvenient side effects and corner cases”
> |  and I’d welcome a list of such cases.
> |  >
> |  > Simon
> |  >
> |  >
> |  > PS: I am leaving Microsoft at the end of November 2021, at which
> |  point
> |  > simonpj at microsoft.com will cease to work.
> |  > Usesimon.peytonjones at gmail.com instead.  (For now, it just forwards
> |  to
> |  > simonpj at microsoft.com.)
> |  >
> |  > From: ghc-steering-committee
> |  > <ghc-steering-committee-bounces at haskell.org> On Behalf Of Spiwack,
> |  > Arnaud
> |  > Sent: 27 October 2021 09:20
> |  > To: Richard Eisenberg <rae at richarde.dev>
> |  > Cc: ghc-steering-committee <ghc-steering-committee at haskell.org>
> |  > Subject: Re: [ghc-steering-committee] Proposal #281: Visible
> |  "forall"
> |  > in terms; rec: accept
> |  >
> |  > I've been struggling to have an opinion on this PR. I'm very
> |  sympathetic to the goal of the proposal (and this latest rendition of
> |  the proposal is a really good document). There are a lot of
> |  inconvenient side effects and corner cases (but, to be fair, these are
> |  not special to this proposal: they are inherent to the dependent types
> |  plan). But I'm fairly convinced that this is the best possible
> |  approach, or close enough.
> |  >
> |  >
> |  >
> |  > So yes, I don't really feel strongly about it. But on balance, I
> |  think that I'm in favour.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20211027/70bbd985/attachment-0001.html>