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

Mon Nov 25 10:38:27 UTC 2019

I have posted on the ticket. The proposal text as it now stands does not support the idea of "just in the renamer", and I find the motivation lacking. Do we need all this power just to write `reflection`? Seems like overkill.

Yes, I agree that local types would often be nice. But would that nicety be covered by local modules (either proposal)?

Richard

> On Nov 25, 2019, at 8:15 AM, Simon Marlow <marlowsd at gmail.com> wrote:
> 
> 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 <mailto: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 <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/ghc-proposals/ghc-proposals/pull/273>
> > https://github.com/treeowl/ghc-proposals/blob/local-types/proposals/0000-local-types.md <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 <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 <mailto:mail at joachim-breitner.de>
> >  http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
> > 
> > 
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org <mailto:ghc-steering-committee at haskell.org>
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <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 <mailto:ghc-steering-committee at haskell.org>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee>
> _______________________________________________
> 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/8aee4a63/attachment-0001.html>