Changes between Version 10 and Version 11 of PartialTypeSignatures


Ignore:
Timestamp:
Apr 16, 2014 2:50:04 PM (11 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