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 |
| 220 | Wildcards can unify with function types, e.g. |
| 221 | {{{ |
| 222 | qux :: Int -> _ |
| 223 | qux i b = i == i && b |
| 224 | -- Inferred: Int -> Bool -> Bool |
| 225 | }}} |
| 226 | Additionally, when they are not instantiated to a monotype, they |
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 | }}} |
| 237 | Each wildcard will be independently instantiated (see |
| 238 | [#named-wildcards Named wildcards] for dependent instantiation), e.g. |
| 239 | the three wildcards in `bar2` are each instantiated to a different |
| 240 | type. |
| 241 | |
| 242 | As type wildcards can be generalised over, additional type variables |
| 243 | can be universally quantified. One should expect an implicit |
| 244 | 'wildcard' in the `forall` part of the type signature, e.g. |
| 245 | {{{ |
| 246 | bar3 :: forall a. a -> (a -> _) -> _ |
| 247 | bar3 x f = f x |
| 248 | -- Inferred: forall a b. a -> (a -> b) -> b |
| 249 | }}} |
| 250 | In addition to the explicitly quantified type variable `a`, the |
| 251 | inferred type now contains a new type variable `b`. As type variables |
| 252 | are implicitly universally quantified in Haskell, we chose not to make |
| 253 | this kind of `forall` 'wildcard' explicit. |
| 254 | |
| 255 | Wildcards can also unify with annotated type variables, e.g. |
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 | | |
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''' |
| 317 | GHC's constraint solver doesn't unify constraints with each other. |
| 318 | E.g. `Eq _` or `_ a` will never be unified with `Eq a`. The problem |
| 319 | the constraint solver is faced with is "deduce `Eq a` from `Eq _`, |
| 320 | figuring out what the `_` should be instantiated to". Or, worse, |
| 321 | "deduce `Eq a` from `_ a`" or something even less constrained. The |
| 322 | constraint solver is absolutely not set up to figure out how to fill |
| 323 | in existential variables in the "givens". |
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 | |