| 563 | == Partial Expression and Pattern Signatures == |
| 564 | |
| 565 | Wildcards should be allowed in expression and pattern signatures, e.g. |
| 566 | {{{ |
| 567 | bar1 :: _a -> Bool |
| 568 | bar1 x = (x :: _a) |
| 569 | -- Inferred: Bool -> Bool |
| 570 | |
| 571 | bar2 :: Bool -> _a |
| 572 | bar2 (x :: _a) = x |
| 573 | -- Inferred: Bool -> Bool |
| 574 | }}} |
| 575 | We do not intend to support an extra-constraints wildcard in such |
| 576 | signatures, as the implementation difficulties it poses don't outweigh |
| 577 | its usefulness. |
| 578 | |
| 579 | Wildcards occurring in a partial type signature are currently |
| 580 | quantified in their type signature, unless they (being named |
| 581 | wildcards) were already brought into scope by another partial type |
| 582 | signature. The question now is: where should wildcards occurring in |
| 583 | partial expression or pattern signatures be quantified? There a number |
| 584 | of options. Remember: we're only talking about wildcards that aren't |
| 585 | already in scope, and as unnamed wildcards can never already be in |
| 586 | scope, this question only concerns named wildcards (of course, the |
| 587 | [[span(!NamedWildcards, style=font-variant: small-caps)]] extension is |
| 588 | turned on in the examples below). |
| 589 | |
| 590 | 1. 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 | |
| 658 | 2. 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 | |
| 699 | 3. 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 | |
| 735 | Except for the possibly counter-intuitive behaviour in the `baz1` and |
| 736 | `baz2` examples, we believe that option 1 is preferable. |
| 737 | |
| 738 | |