Changes between Version 5 and Version 6 of PartialTypeSignatures


Ignore:
Timestamp:
Mar 14, 2014 1:55:09 PM (17 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  }}}