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

[Eric Seidel]

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