Changes between Version 5 and Version 6 of PartialTypeSignatures


Ignore:
Timestamp:
Mar 14, 2014 1:55:09 PM (14 months ago)
Author:
thomasw
Comment:

Incorporate comments and responses into the text

Legend:

Unmodified
Added
Removed
Modified
  • PartialTypeSignatures

    v5 v6  
    184184== Our Design == 
    185185 
     186A good way to think of a partial type signature is as follows. If a 
     187function has a type signature, GHC checks that it has ''exactly'' that 
     188type. But if it has a ''partial'' type signature GHC proceeds exactly 
     189as if it were inferring the type for the function (especially 
     190including generalisation), except that it additionally forces the 
     191function's type to have the shape given by the partial type signature. 
     192 
    186193We now describe the syntax and the semantics of our partial type 
    187194signatures. 
     
    201208We call wildcards occurring within the monotype (`tau`) part of the 
    202209type signature ''type wildcards''. Type wildcards can be instantiated 
    203 to concrete types like `Bool` or `Maybe [Bool]`, e.g. 
     210to any monotype like `Bool` or `Maybe [Bool]`, e.g. 
    204211{{{ 
    205212not' :: Bool -> _ 
     
    211218-- Inferred: Maybe [Bool] 
    212219}}} 
    213 '''SLPJ''' What is a "concrete type"?  I think you mean this: a type wildcard can be instantiated to any monotype.  '''End SLPJ''' 
    214 '''thomasw''' Exactly. '''End thomasw''' 
    215  
    216 Additionally, when they are not constrained to a particular type, they 
     220Wildcards can unify with function types, e.g. 
     221{{{ 
     222qux :: Int -> _ 
     223qux i b = i == i && b 
     224-- Inferred: Int -> Bool -> Bool 
     225}}} 
     226Additionally, when they are not instantiated to a monotype, they 
    217227will be generalised over, e.g. 
    218228{{{ 
     
    220230bar x = x 
    221231-- Inferred: forall a. a -> a 
    222 }}} 
    223 '''SLPJ''' What does "when they are not constrained to a particular type" mean?  Presumably this would also work: 
    224 {{{ 
     232 
    225233bar2 :: _ -> _ -> _ 
    226234bar2 x f = f x 
    227 -- Inferred: forall a b. a -> (a->b) -> b 
    228 }}} 
    229 Also you should make clear that  
    230  * each wildcard is independently instantiated; in `bar2`, the three wildcards are each instantiated to a different type. 
    231  * In effect, whenever you have a type wildcard there is a wild-card in the `forall` part too.  For example you could say 
    232 {{{ 
    233 bar2 :: forall a. a -> (a -> _) -> _ 
    234 bar2 x f = f x 
    235 -- Inferred: forall a b. a -> (a->b) -> b 
    236 }}} 
    237   and that would work too.  (I hope.) 
    238  
    239 '''End SLPJ'''. 
    240  
    241 '''thomasw''' "when they are not constrained to a particular type" = they are not instantiated to a monotype. 
    242 Both examples work exactly as you would hope. Indeed, (unnamed) wildcards are instantiated independently, unlike named wildcards. Yes, type wildcards can be generalised over and can result in extra `forall` quantified type variables. As type variables are implicitly universally quantified in Haskell, we chose not to make this `forall` 'wildcard' explicit. 
    243 '''End thomasw''' 
    244  
    245  
    246  
    247  
    248 Wildcards can unify with function types, e.g. 
    249 {{{ 
    250 qux :: Int -> _ 
    251 qux i b = i == i && b 
    252 -- Inferred: Int -> Bool -> Bool 
    253 }}} 
    254 And annotated type variables, e.g. 
     235-- Inferred: forall a b. a -> (a -> b) -> b 
     236}}} 
     237Each wildcard will be independently instantiated (see 
     238[#named-wildcards Named wildcards] for dependent instantiation), e.g. 
     239the three wildcards in `bar2` are each instantiated to a different 
     240type. 
     241 
     242As type wildcards can be generalised over, additional type variables 
     243can be universally quantified. One should expect an implicit 
     244'wildcard' in the `forall` part of the type signature, e.g. 
     245{{{ 
     246bar3 :: forall a. a -> (a -> _) -> _ 
     247bar3 x f = f x 
     248-- Inferred: forall a b. a -> (a -> b) -> b 
     249}}} 
     250In addition to the explicitly quantified type variable `a`, the 
     251inferred type now contains a new type variable `b`. As type variables 
     252are implicitly universally quantified in Haskell, we chose not to make 
     253this kind of `forall` 'wildcard' explicit. 
     254 
     255Wildcards can also unify with annotated type variables, e.g. 
    255256{{{ 
    256257filter' :: _ -> [a] -> [a] 
     
    283284}}} 
    284285 
    285 '''SLPJ''' I think an easier way to explain it would be this. If a function has a type signature, GHC 
    286 checks that it has ''exactly'' that type.  But if it has a ''partial'' type signature GHC proceeds exactly as if it were inferring the type for the function (especially including generalisation), except that it additionally forces the function's type to have the shape given  
    287 by the partial type signature. 
    288 '''End SLPJ''' 
    289  
    290 '''thomasw''' Correct. '''End thomasw''' 
    291  
    292 '''SLPJ''' Can wildcards appear under higher rank foralls? 
    293 {{{ 
    294 f :: (forall a. _ -> a) -> b -> b 
    295 }}} 
    296 I think that seems jolly complicated.  At least, it would be Far Too Complicated if the nested `forall` was supposed to be extended, say thus 
    297 {{{ 
    298 -- Inferred  f :: (forall a c. c -> a) -> b -> b 
    299 }}} 
    300 Also I think it would be very hard to support 
    301 {{{ 
    302 f :: (forall a. _ => a -> a) -> b -> b 
    303 }}} 
    304 '''End SLPJ''' 
    305  
    306 '''thomasw''' We agree, this is exactly what we discuss [#nested-extra-constraints here] and [#higher-rank-types here]. 
    307 '''End thomasw''' 
    308  
    309286=== Constraint Wildcards === 
     287 
     288'''NOTE''': we no longer intend to support constraint wildcards as 
     289described below. Only [#named-wildcards named wildcards] also 
     290occurring in monotype and an [#extra-constraints-wildcard extra-constraints wildcard] 
     291will be allowed. 
    310292 
    311293'''SLPJ''' I'm honestly not sure it's worth the complexity you have here. The 
     
    333315-- Inferred type: forall a b. Two a b -> a -> a 
    334316}}} 
    335 A problem with constraint wildcards is that GHC's type constraint 
    336 solver doesn't unify constraints with each other. E.g. `Eq _` or `_ a` 
    337 will never be unified with `Eq a`.  
    338  
    339 '''SLPJ''' 
    340 I don't find that a helpful explanation.  It's more like this.  The problem the 
    341 constraint solver is faced with is "deduce Eq x from Eq _, figuring out what the 
    342 _ should be instantiated to".  Or, worse, "deduce Eq x from (_ x)" or something  
    343 even less constrained.  The constraint solver is absolutely not set up to 
    344 figure out how to fill in existential variables in the "givens". 
    345 '''End SLPJ''' 
    346  
    347 '''thomasw''' A much clearer explanation indeed. '''End thomasw''' 
     317GHC's constraint solver doesn't unify constraints with each other. 
     318E.g. `Eq _` or `_ a` will never be unified with `Eq a`. The problem 
     319the constraint solver is faced with is "deduce `Eq a` from `Eq _`, 
     320figuring out what the `_` should be instantiated to". Or, worse, 
     321"deduce `Eq a` from `_ a`" or something even less constrained. The 
     322constraint solver is absolutely not set up to figure out how to fill 
     323in existential variables in the "givens". 
    348324 
    349325So the following program will not 
     
    378354[#issue-constraint-wildcards later]. 
    379355 
    380 === Extra-constraints Wildcard === 
     356=== Extra-constraints Wildcard === #extra-constraints-wildcard 
    381357 
    382358A third kind of wildcard we propose is the ''extra-constraints 
     
    587563== Questions and issues == #issue-constraint-wildcards 
    588564 
    589 * [=#issue-constraint-wildcards] '''Constraint wildcards''': Wildcards in constraints sometimes 
    590   behave in a confusing way. As explained above, the reason is that 
    591   GHC's type constraint solver doesn't unify constraints with each 
    592   other. E.g. `Eq _` or `_ a` will never be unified with `Eq a`. So 
    593   the following program will not work: 
    594   {{{ 
    595   -- Neither partial type signature will work 
    596   impossible :: Eq _ => a -> a -> Bool 
    597   impossible :: _  a => a -> a -> Bool 
    598   impossible x y = x == y 
    599   -- Actual type: forall a. Eq a => a -> a -> Bool 
    600   }}} 
    601   One might expect that the wildcard `_` in the annotated constraint 
    602   `Eq _` would be unified with the required `Eq a` constraint, but 
    603   unfortunately, this doesn't work. Rather, we get an error about the 
    604   unsatisfiable `Eq a` constraint. 
    605   [[br]][[br]] 
    606   That does not mean wildcards in constraints are useless though. The 
    607   examples `fstIsBool`, `secondParam`, `somethingShowable` and 
    608   `somethingShowable'` above all use them in ways that will work and 
    609   may be useful. 
    610   [[br]][[br]] 
    611   In summary, we are not fully sure about whether or not to allow 
    612   wildcards in constraints. They can be useful, but their behaviour 
    613   may be confusing to users. One possible restriction is to disallow 
    614   unnamed wildcards in constraints and only allow named wildcards in 
    615   constraints when they also occur in the monotype. 
     565* [=#issue-constraint-wildcards] '''Constraint wildcards''': 
     566  '''NOTE''': we no longer intend to support constraint wildcards. 
     567  Only [#named-wildcards named wildcards] also occurring in monotype 
     568  and an [#extra-constraints-wildcard extra-constraints wildcard] 
     569  will be allowed. The examples below demonstrating the named wildcard 
     570  in the constraints look useful to us (and already work in the 
     571  implementation). 
     572  {{{ 
     573  somethingShowable :: Show _x => _x -> _ 
     574  somethingShowable x = show x 
     575  -- Inferred type: Show x => x -> String 
     576    
     577  somethingShowable' :: Show _x => _x -> _ 
     578  somethingShowable' x = show (not x) 
     579  -- Inferred type: Bool -> String 
     580  }}} 
     581 
    616582 
    617583* [=#issue-named-wildcards-scope] '''The scope of named wildcards''': 
     
    720686  }}} 
    721687 
    722 * [=#higher-rank-types] '''Higher-rank types''': Consider the following partial type 
    723   signature: 
     688* [=#higher-rank-types] '''Higher-rank types''': Consider the 
     689  following partial type signature: 
    724690  {{{ 
    725691  forall a. a -> (forall b. (b, _c) -> b) -> Int 
    726692  }}} 
    727   We believe that generalising over the `_c` named wildcard in the 
    728   should lead to a top-level quantification (where `a` is quantified) 
    729   of the resulting type variable: 
     693  We believe that generalising over the `_c` named wildcard should 
     694  lead to a top-level quantification (where `a` is quantified) of the 
     695  resulting type variable: 
    730696  {{{ 
    731697  forall a tw_c. a -> (forall b. (b, tw_c) -> b) -> Int 
     
    738704  The latter is equivalent to inferring higher-rank types, which, as 
    739705  we mentioned before, is not something we can do. 
     706  [[br]][[br]] 
     707  Additionally, we do not allow an extra-constraints wildcard in a 
     708  nested 'forall', e.g. 
     709  {{{ 
     710  f :: (forall a. _ => a -> a) -> b -> b 
     711  }}}