[ghc-steering-committee] Proposal #273: Local Types, Recommendation: needs revision

[Simon Marlow]

Having written a little C++ recently (yeah I know) where you can have local
type definitions, it feels entirely natural and I started to notice the
lack of them in Haskell. So I support the proposal.

My intuition is that we ought to be able to treat local types in the same
way as local variables: they are entities with scoping rules enforced by
the renamer. That is, a local type would be an ordinary TyCon with a Name
and so forth. Having only read your email and not the proposal, that sounds
the same as Arnuad's suggestion.

Cheers
Simon


On Sat, 23 Nov 2019 at 16:32, Eric Seidel <eric at seidel.io> wrote:

> Hi all,
>
> I am the shepherd for proposal #273: Local Types (
> https://github.com/ghc-proposals/ghc-proposals/pull/273).
>
> This proposal would add support for local type and instance (class and
> type-family) definitions as a means of addressing the Configurations
> Problem, which as I understand it is essentially "How can we *implicitly*
> pass around dynamically determined values in a safe manner?" The
> `reflection` package provides an answer to this question with its `Reifies`
> class, but the implementation relies on `unsafeCoerce` and the
> implementation details of how GHC represents single-method class
> dictionaries. The proposal argues that we could safely implement the
> `reflection` package with local types and instances, if only Haskell had
> such things! As a motivation I find this pretty compelling.
>
> The proposal introduces a few restrictions on local types and instances,
> and functions that contain them, primarily as a means of providing a
> no-escape property: local types must not be able to escape their defining
> scope. There are a couple ways this could happen. (1) The defining function
> could return a value of some local type. This is prohibited unless the
> value is wrapped in an existential, as otherwise the function simply could
> not be typed. (2) More interestingly, a type class with a functional
> dependency or a type family could leak the local type to the outer scope.
> Consider the following:
>
> ```
> type family F x
>
> foo x = x
>   where
>   data T
>   type instance F Int = T
>
> bar :: F Int
> bar = ???
> ```
>
> What type should `bar` have? The proposal says that all instances are
> still global, which would mean `bar :: T`, which is absurd. To avoid cases
> like this, the proposal introduces a restriction on local instances that
> says local types may not be determined by types from an outer scope (either
> via fundeps or type families). I believe these two restrictions are
> sufficient to guarantee the no-escape property.
>
> I think the key question that is left unanswered by the proposal is how
> exactly we might implement local types in GHC. The proposal (as a
> guideline, not necessarily an implementation strategy) to think of local
> types as global types that are implicitly indexed by the type and value
> parameters of its defining function. But GHC does not yet have dependent
> types, so this is not a workable implementation strategy. Another possible
> strategy would be to add type/instance definitions to Core, but as Simon PJ
> points out this would be a tremendous amount of work, so also not a
> practical direction for the short-term. Lastly, Arnaud suggests that we
> treat local types like global types that are only defined in the local
> scope, i.e. let the renamer deal with them entirely. Local instances are
> different as they must capture locally-bound variables, but there's nothing
> conceptually difficult about constructing new instances dynamically (this
> is what ImplicitParams does). There are some remaining questions around how
> to ensure the optimizer doesn't incorrectly swap two instances for a local
> type, but these seem tractable.
>
> I think Arnaud's suggestion is a promising and feasible strategy for
> implementing this proposal without new research, so my recommendation is
> that we return the proposal for revision and recommend the author
> incorporate Arnaud's suggestions.
>
> As usual, please provide technical feedback on the PR, and feedback on my
> recommendation here on the mailing list.
>
> Eric
>
> On Mon, Nov 4, 2019, at 03:21, Joachim Breitner wrote:
> > Dear Committee,
> >
> > this is your secretary speaking:
> >
> > Local Types
> > has been updated by David Feuer
> > https://github.com/ghc-proposals/ghc-proposals/pull/273
> >
> https://github.com/treeowl/ghc-proposals/blob/local-types/proposals/0000-local-types.md
> >
> > I propose Eric as the shepherd.
> >
> > Please reach consensus as described in
> > https://github.com/ghc-proposals/ghc-proposals#committee-process
> > I suggest you make a recommendation, in a new e-mail thread with the
> > proposal number in the subject, about the decision, maybe point out
> > debatable points, and assume that anyone who stays quiet agrees with
> > you.
> >
> > Thanks,
> > Joachim
> > --
> > Joachim Breitner
> >  mail at joachim-breitner.de
> >  http://www.joachim-breitner.de/
> >
> >
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> >
> > Attachments:
> > * signature.asc
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20191125/37bb458f/attachment.html>