Changes between Version 10 and Version 11 of PartialTypeSignatures


Ignore:
Timestamp:
Apr 16, 2014 2:50:04 PM (16 months ago)
Author:
thomasw
Comment:

Discuss partial expression and pattern signatures

Legend:

Unmodified
Added
Removed
Modified
  • PartialTypeSignatures

    v10 v11  
    561561type signature.
    562562
     563== Partial Expression and Pattern Signatures ==
     564
     565Wildcards should be allowed in expression and pattern signatures, e.g.
     566{{{
     567bar1 :: _a -> Bool
     568bar1 x = (x :: _a)
     569-- Inferred: Bool -> Bool
     570
     571bar2 :: Bool -> _a
     572bar2 (x :: _a) = x
     573-- Inferred: Bool -> Bool
     574}}}
     575We do not intend to support an extra-constraints wildcard in such
     576signatures, as the implementation difficulties it poses don't outweigh
     577its usefulness.
     578
     579Wildcards occurring in a partial type signature are currently
     580quantified in their type signature, unless they (being named
     581wildcards) were already brought into scope by another partial type
     582signature. The question now is: where should wildcards occurring in
     583partial expression or pattern signatures be quantified? There a number
     584of options. Remember: we're only talking about wildcards that aren't
     585already in scope, and as unnamed wildcards can never already be in
     586scope, this question only concerns named wildcards (of course, the
     587[[span(!NamedWildcards, style=font-variant: small-caps)]] extension is
     588turned on in the examples below).
     589
     5901. Quantify wildcards in the partial '''expression or pattern
     591   signature''' they appear in. Consider the following example:
     592   {{{
     593   f :: _
     594   f x y = let p :: _
     595               p = (x :: _a)
     596               q :: _
     597               q = (y :: _a)
     598          in (p, q)
     599   -- Inferred:
     600   -- f :: forall tw_a tw_a1. tw_a -> tw_a1 -> (tw_a, tw_a1)
     601   --   p :: tw_a
     602   --   q :: tw_a1
     603   }}}
     604   Both times, the `_a` in the expression signature isn't in scope, so
     605   it is quantified once in each expression signature. This means that
     606   the two occurrences of `_a` don't refer to the same named wildcard.
     607   Still, this can be achieved by mentioning `_a` in a type signature
     608   (where `_a` will then be quantified) of a common higher-level
     609   binding:
     610   {{{
     611   f :: _a -> _
     612   f x y = let p :: _
     613               p = (x :: _a)
     614               q :: _
     615               q = (y :: _a)
     616          in (p, q)
     617   -- Inferred:
     618   -- f :: forall tw_a. tw_a -> tw_a -> (tw_a, tw_a)
     619   --   p :: tw_a
     620   --   q :: tw_a
     621   }}}
     622   Note that the first example is equivalent to the following program
     623   (changing `f`'s partial type signature will also cause the same
     624   change as in the example above):
     625   {{{
     626   f :: _
     627   f x y = let p :: _a
     628               p = x
     629               q :: _a
     630               q = y
     631          in (p, q)
     632   }}}
     633   The named wildcards quantified in a partial expression or pattern
     634   signature will be in scope in the expression or pattern to which
     635   the signature was attached:
     636   {{{
     637   foo = (\(x :: _a, y) -> y) :: _ -> _a
     638   -- Inferred: forall tw_a . (tw_a, tw_a) -> tw_a
     639   }}}
     640   Overall, this solution is the simplest, also to implement, and has
     641   a good ''power-to-weight'' ratio. However, what happens in the
     642   following examples might be counter-intuitive to some users:
     643   {{{
     644   baz1 x y = (x :: _a, y :: _a)
     645   baz2 (x :: _a) (y :: _a) = (x, y)
     646   -- Inferred for both:
     647   --   forall tw_a tw_a1. tw_a -> tw_a1 -> (tw_a, tw_a1)
     648   }}}
     649   In the examples above, every time an `_a` occurs, `_a` isn't yet in
     650   scope, and is thus quantified in each expression/pattern signature
     651   separately. Therefore, all occurrences of `_a` are distinct. This
     652   might be perceived counter-intuitive. Again, both occurrences in
     653   each binding can be made to refer to the same named wildcard by
     654   mentioning `_a` in a signature common to both expression
     655   signatures, e.g. by mentioning it in the type signature of `baz1`
     656   and `baz2`.
     657
     6582. Quantify wildcards in the '''type signature of the innermost enclosing binding'''.
     659   The first example of option 1 will behave exactly the same:
     660   {{{
     661   f :: _
     662   f x y = let p :: _
     663               p = (x :: _a)
     664               q :: _
     665               q = (y :: _a)
     666          in (p, q)
     667   -- Inferred:
     668   -- f :: forall tw_a tw_a1. tw_a -> tw_a1 -> (tw_a, tw_a1)
     669   --   p :: tw_a
     670   --   q :: tw_a1
     671   }}}
     672   Contrary to option 1, the last example will behave more
     673   intuitively:
     674   {{{
     675   baz1 x y = (x :: _a, y :: _a)
     676   baz2 (x :: _a) (y :: _a) = (x, y)
     677   -- Inferred for both:
     678   --   forall tw_a. tw_a -> tw_a -> (tw_a, tw_a)
     679   }}}
     680   In `baz1` and `baz2`, both occurrences of `_a` will refer to the
     681   same named wildcard.
     682
     683   However, what if there's no enclosing binding with a type
     684   signature, like in `baz1` and `baz2`? Quantifying the wildcards in
     685   the binding itself could solve this, but makes the implementation
     686   more complex.
     687
     688   Another downside has to do with the implementation. This option
     689   will require an extra renaming pass over the body of a binding that
     690   will extract the wildcards from the expression signatures to store
     691   them together with the wildcards mentioned in the type signature.
     692
     693   An alternative is an invasive refactoring of the functions that
     694   deal with renaming the bodies of a binding. It would involve
     695   threading a list of extracted wildcards through these functions. A
     696   lot more code (certainly more than we feel comfortable touching)
     697   would have to be touched to implement this.
     698
     6993. Quantify wildcards in the '''type signature of the top-level enclosing binding'''.
     700   This option changes the behaviour of the first example of options 1
     701   and 2, both occurrences of `_a` will refer to the same named
     702   wildcard.
     703   {{{
     704   f :: _
     705   f x y = let p :: _
     706               p = (x :: _a)
     707               q :: _
     708               q = (y :: _a)
     709          in (p, q)
     710   -- Inferred:
     711   -- f :: forall tw_a. tw_a -> tw_a -> (tw_a, tw_a)
     712   --   p :: tw_a
     713   --   q :: tw_a
     714   }}}
     715   Consider the following example:
     716   {{{
     717   foo o = let f :: (_a, _) -> _a
     718               f (u, _) = not u
     719               g (x :: _a) (xs :: [_a]) = x : xs
     720         in g (f o) []
     721   -- Inferred:
     722   -- foo :: forall a. (Bool, a) -> [Bool]
     723   --   f :: forall b. (Bool, b) -> Bool
     724   --   g :: Bool -> [Bool] -> [Bool]
     725   }}}
     726
     727   Is it intuitive in the example above that all occurrences of `_a`
     728   refer to the same named wildcard? What if `g` didn't have pattern
     729   signatures, but the partial type signature `g :: _a -> [_a] -> _`?
     730   Does it still make that much sense?
     731
     732   Besides the difference in scoping, this option is very similar to
     733   option 2. It shares its downsides as well.
     734
     735Except for the possibly counter-intuitive behaviour in the `baz1` and
     736`baz2` examples, we believe that option 1 is preferable.
     737
     738
    563739== Formalisation ==
    564740
    565 We worked out a rigorous formalisation of partial type signature
     741We worked out a rigorous formalisation of partial type signatures
    566742including typing rules, extending the existing formalisation of GHC's
    567743type inference system, [[span(!OutsideIn(X), style=font-variant: small-caps)]]
     
    678854
    679855
    680 * [=#issue-named-wildcards-scope] '''The scope of named wildcards''':
     856* [=#issue-named-wildcards-scope]'''The scope of named wildcards''':
    681857  We currently treat all named wildcards as scoped type variables,
    682858  i.e. if we mention a named wildcard in a top-level partial type