Changes between Version 7 and Version 8 of PatternSynonyms/AssociatingSynonyms


Ignore:
Timestamp:
Nov 18, 2015 4:08:00 PM (4 years ago)
Author:
mpickering
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • PatternSynonyms/AssociatingSynonyms

    v7 v8  
    1 == Associating pattern synonyms with types ==
    2 
    3 This section is based upon #10653 and D1258.
     1== Bundlings pattern synonyms with types ==
     2
     3This section is based upon #10653 and D1258. The feature was implemented in [https://github.com/ghc/ghc/commit/96621b1b4979f449e873513e9de8d806257c9493 96621b1b4979f449e873513e9de8d806257c9493].
    44
    55Pattern synonyms allow for constructors to be defined, exported and imported separately from the types which they build.
    6 However, it is sometimes convenient to associate synonyms with types so that we can more closely model ordinary data constructors.
     6However, it is sometimes convenient to bundle synonyms with types so that we can more closely model ordinary data constructors.
    77
    88If we want to refactor to change the internal representation of this maybe-like type to use Maybe.
     
    3737will no longer work as importing `A(..)` will import the type `A` and the constructor `NewA`. We can explicitly import the
    3838new patterns but the usage of pattern synonyms should be transparent to the end user. What's needed is to be able to
    39 associate the new synonyms with a type such that client code is oblivious to this implementation.
     39bundle the new synonyms with a type such that client code is oblivious to this implementation.
    4040
    4141=== Proposal ===
     
    112112For any modules `M` `N`, if we import `N` from `M`,
    113113
    114 * The abbreviated form `T(..)` brings into scope all the constructors, methods or field names exported by `N` as well any patterns associated with `T` relative to `N`.
    115 * The explicit form `T(c1,...,cn)` can name any constructors, methods or field names exported by `N` as well as any patterns associated with `T` relative to `N`.
     114* The abbreviated form `T(..)` brings into scope all the constructors, methods or field names exported by `N` as well any patterns bundled with `T` relative to `N`.
     115* The explicit form `T(c1,...,cn)` can name any constructors, methods or field names exported by `N` as well as any patterns bundled with `T` relative to `N`.
    116116
    117117
    118118==== Typing ====
    119119
    120 WIP
    121 
    122 If we associate a pattern synonym `P` with a type `T` then we consider three separate cases depending on the type of `P`. '''RAE:''' To the right of `::` below, I assume you mean to refer only to the "result" part of the type, allowing arguments to the left of arrows. '''End RAE'''
    123 
    124 * If `P :: T t1 t2 .. tn` then `P` is an instance of `T. We completely ignore constraints in this case.
    125 * If `P :: f t1 t2 .. tn`, in other words, if `P` is polymorphic in `f`, then `f` must be brought into scope by a constraint. In this case we check that `T u1 ... un` is a subtype of `ReqTheta => f t1 t2 ... tn`. We must involve `ReqTheta` in the case that it contains equality constraints and/or type families. In the case that ReqTheta contains a class constraint, we require that the correct instance for `T` is in scope.
    126 
    127     '''RAE:''' I'm a little baffled here. What does "`f` must be brought into scope by a constraint" mean? Constraints aren't scoping constructs. You're checking whether `T u1 ... un` is a subtype of `ReqTheta => f t1 ... tn`. Call the first type `τ` and the second one `θ => σ`. In other words, you want `τ` to be more polymorphic than `θ => σ`. But this is still a little unclear. What type variables are allowed to be unified? Those in `τ`? Those in `θ => σ`? And by saying that `τ` is more polymorphic than `θ => σ`, that means that we're ''assuming'' `θ`. And indeed you mean that for `θ`'s equality constraints. But then you say that we check for the existence of class constraints, which makes it sound like we're not assuming `θ` after all.
    128 
    129     Further down, in the examples, you talk about the possibility of a later module introducing an orphan and claim that class constraints are ignored. But that conflicts with this statement here. '''End RAE'''
    130 
    131 * If `P :: F v1 .. vm` where `F` is a type family then unless `F v1 ... vm ~ T t1 t2 ... tn` we do not allow `P` to be associated with `T`.
    132 
    133     '''RAE:''' This might be more restrictive than you mean it to be. What if `F Int ~ T` and `F Bool ~ T` but `F Char ~ Q`? According to your spec, you require that `F` have a "universal" instance... which means that `F` is as expressive as a vanilla type synonym. '''End RAE'''
    134 
    135 '''RAE:''' Given all of the deep, unending confusion around here, I propose the following, much simpler, scheme: Just use the first bullet above. It's exceedingly
    136 simple, obviously safe, intuitive to users, and easy to implement. It misses out on some more exotic type system features. But no one is asking to write pattern synonyms with these exotic features and then associate them! When they do ask, we can relax restrictions appropriately, armed with real use cases. I'm also worried that, in many of these exotic cases, type-correct synonyms are in fact impossible to write at all. This is another reason to wait for use cases. It's really easy to relax these restrictions later -- no breakage required. '''End RAE'''
     120It proved quite a challenge to precisely specify which pattern synonyms
     121should be allowed to be bundled with which type constructors.
     122In the end it was decided to be quite liberal in what we allow. Below is
     123how Simon described the implementation.
     124
     125> Personally I think we should Keep It Simple.  All this talk of
     126> satisfiability makes me shiver.  I suggest this: allow T( P ) in all
     127> situations except where `P`'s type is ''visibly incompatible'' with
     128> `T`.
     129
     130> What does "visibly incompatible" mean?  `P` is visibly incompatible
     131> with
     132>     `T` if
     133>       * `P`'s type is of form `... -> S t1 t2`
     134>       * `S` is a data/newtype constructor distinct from `T`
     135
     136> Nothing harmful happens if we allow `P` to be exported with
     137> a type it can't possibly be useful for, but specifying a tighter
     138> relationship is very awkward as you have discovered.
     139
     140Note that this allows *any* pattern synonym to be bundled with any
     141datatype type constructor. For example, the following pattern `P` can be
     142bundled with any type.
     143
     144{{{
     145pattern P :: (A ~ f) => f
     146}}}
     147
     148So we provide basic type checking in order to help the user out,
     149pattern synonyms are defined with definite type constructors, but don't
     150actually prevent a library author completely confusing their users if
     151they want to.
     152
    137153
    138154A few examples are included for clarification in the final section.
     
    292308}}}
    293309
    294 Pattern `P` has type `f`, when solving the required constraints we find that
    295 `A ~ f` so `P :: A` and hence we allow the export.
     310Pattern `P` has no visibly obvious type so we allow it to be bundled with any type constructor.
    296311
    297312{{{#!hs
     
    315330}}}
    316331
    317 In this example, `P` is once again polymorphic in the constructor `f`. It might
    318 seem that we should only allow `P` when there is an instance for `C Identity`
    319 in scope. However, we completely ignore class constraints as a user may
    320 provide an orphan instance which allows the pattern to be used. Despite this,
    321 it is more conservative and perhaps less surprising to require that the correct
    322 instance is in scope.
    323 
    324 It may seen like we should not allow any synonym which is polymorphic in the
    325 constructor to be associated with a type but this is too strict. The previous
    326 example showed a synonym which was polymorphic in `f` but `f` has arity 0. In
    327 general, we see that equality constraints mean that we have to do at least some
    328 constraint solving even if it is a very strange way to define a pattern synonym.
    329 
    330 For example, we certainly do not want to allow the following association.
     332In this example, `P` is once again polymorphic in the constructor `f` so it can be bundled with any type constructor.
     333
     334
     335We certainly do not want to allow the following association but we do anyway as the type is not visibly different.
    331336
    332337{{{#!hs
     
    371376
    372377We should only allow `P` to be associated with `A` due to the superclass constraint
    373 `f ~ A`.
     378`f ~ A` but it can be bundled with any type constructor as it is not visibly different.
    374379
    375380===== Type Families =====
     
    390395}}}
    391396
    392 There are no instances for `F` but a client module which imports `A` and `P`
    393 could provide such an instance which then may or may not type check.
    394 
    395 Like classes, unless `F Bool` is defined then we should not allow `P` to be associated with `A`.
     397We can bundle `P` with any type constructor as the type is not visibly different.
    396398
    397399
     
    460462but without depending on `old-rep`. More generally, an author may want to write a `*-compat` package for two packages which they do
    461463not control. Having to define these synonyms at the definition site is too restrictive for this case .
     464
     465
     466
     467
     468{{{#!comment
     469Old typing
     470
     471If we associate a pattern synonym `P` with a type `T` then we consider three separate cases depending on the type of `P`. '''RAE:''' To the right of `::` below, I assume you mean to refer only to the "result" part of the type, allowing arguments to the left of arrows. '''End RAE'''
     472
     473* If `P :: T t1 t2 .. tn` then `P` is an instance of `T. We completely ignore constraints in this case.
     474* If `P :: f t1 t2 .. tn`, in other words, if `P` is polymorphic in `f`, then `f` must be brought into scope by a constraint. In this case we check that `T u1 ... un` is a subtype of `ReqTheta => f t1 t2 ... tn`. We must involve `ReqTheta` in the case that it contains equality constraints and/or type families. In the case that ReqTheta contains a class constraint, we require that the correct instance for `T` is in scope.
     475
     476    '''RAE:''' I'm a little baffled here. What does "`f` must be brought into scope by a constraint" mean? Constraints aren't scoping constructs. You're checking whether `T u1 ... un` is a subtype of `ReqTheta => f t1 ... tn`. Call the first type `τ` and the second one `θ => σ`. In other words, you want `τ` to be more polymorphic than `θ => σ`. But this is still a little unclear. What type variables are allowed to be unified? Those in `τ`? Those in `θ => σ`? And by saying that `τ` is more polymorphic than `θ => σ`, that means that we're ''assuming'' `θ`. And indeed you mean that for `θ`'s equality constraints. But then you say that we check for the existence of class constraints, which makes it sound like we're not assuming `θ` after all.
     477
     478    Further down, in the examples, you talk about the possibility of a later module introducing an orphan and claim that class constraints are ignored. But that conflicts with this statement here. '''End RAE'''
     479
     480* If `P :: F v1 .. vm` where `F` is a type family then unless `F v1 ... vm ~ T t1 t2 ... tn` we do not allow `P` to be associated with `T`.
     481
     482    '''RAE:''' This might be more restrictive than you mean it to be. What if `F Int ~ T` and `F Bool ~ T` but `F Char ~ Q`? According to your spec, you require that `F` have a "universal" instance... which means that `F` is as expressive as a vanilla type synonym. '''End RAE'''
     483
     484'''RAE:''' Given all of the deep, unending confusion around here, I propose the following, much simpler, scheme: Just use the first bullet above. It's exceedingly
     485simple, obviously safe, intuitive to users, and easy to implement. It misses out on some more exotic type system features. But no one is asking to write pattern synonyms with these exotic features and then associate them! When they do ask, we can relax restrictions appropriately, armed with real use cases. I'm also worried that, in many of these exotic cases, type-correct synonyms are in fact impossible to write at all. This is another reason to wait for use cases. It's really easy to relax these restrictions later -- no breakage required. '''End RAE'''
     486}}}