... | ... | @@ -45,19 +45,149 @@ A user declares a complete match using a `COMPLETE` pragma. The definition consi |
|
|
|
|
|
`COMPLETE` pragmas can appear in any module in which `con_1,..., con_n` are in scope. Specifically, they need not be in the defining module.
|
|
|
|
|
|
|
|
|
Optionally a user may also specify the type constructor of the patterns.
|
|
|
|
|
|
```
|
|
|
{-# COMPLETE con_1, ..., con_n :: T #-}
|
|
|
```
|
|
|
|
|
|
# Semantics
|
|
|
|
|
|
`COMPLETE` pragmas are only used in the pattern match checker.
|
|
|
|
|
|
|
|
|
For a given `COMPLETE` pragma, for a complete matching `c`, if a user writes a function which matches on all constructors in `c` then we consider the function to be total and the pattern match checker should not emit a warning.
|
|
|
For each `COMPLETE` pragma we identify the type of the set of conlikes.
|
|
|
|
|
|
|
|
|
For a `COMPLETE` pragma of type `T` with conlikes `c_1, ..., c_n`. If in a pattern match of type `T` we match on `c_1, ..., c_n` then
|
|
|
we assume that the match is covering. This means that the pattern match checker will no longer emit a warning about incomplete pattern matches.
|
|
|
|
|
|
`COMPLETE` pragmas are always imported and exported from modules.
|
|
|
|
|
|
`COMPLETE` pragmas only specify that a certain match is covering, because of this, we do not warn about redundant or inaccessible matches when the pattern match checking result arises
|
|
|
from checking against a `COMPLETE` pragma.
|
|
|
|
|
|
|
|
|
Different `COMPLETE` pragmas can mention overlapping sets of conlikes. If there is more than one relevant `COMPLETE` pragma then each is tried, if none of them result in a covering match then an error is reported
|
|
|
as described in the "Error Reporting" section.
|
|
|
|
|
|
|
|
|
There are no checks to ensure that the set of patterns is actually complete or covering in any way. It is up to the user to get it right.
|
|
|
|
|
|
`COMPLETE` pragmas are a new source of orphan modules. For example,
|
|
|
|
|
|
```
|
|
|
moduleMwhereimportN( pattern P, pattern Q){-# COMPLETE P, Q #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
where neither `P` nor `Q` is defined in M. Then every module that is
|
|
|
transitively "above" M would need to read `M.hi` just in case its
|
|
|
`COMPLETE` pragmas was relevant.
|
|
|
|
|
|
## Typing
|
|
|
|
|
|
|
|
|
We verify that the result types of each constructor in a complete match agrees with each other. This is a sanity check as users would never be able to match on all constructors if the set of patterns is inconsistent in this manner.
|
|
|
We refer to the leftmost type in the result type of a conlike as the rtc.
|
|
|
|
|
|
|
|
|
For example, the rtc of `P :: a -> b -> T a b` is `T`, the rtc of `P :: T` is `T` and the rtc of `P :: ... -> f Int` is a type variable `f`.
|
|
|
|
|
|
|
|
|
We distinguish between polymorphic and monomorphic conlikes.
|
|
|
|
|
|
- A monomorphic conlike is when the rtc is a type constructor.
|
|
|
- A polymorphic conlike is when the rtc is not a type constructor.
|
|
|
|
|
|
|
|
|
By the end of type checking, we must identify a type constructor to identify with each set of patterns.
|
|
|
|
|
|
|
|
|
In the case where there is at least one monomorphic pattern `P`, the rtc of `P` is the type constructor for the whole set of patterns.
|
|
|
Each monomorphic conlike must have the same rtc as `P`.
|
|
|
There is no requirement for polymorphic conlikes.
|
|
|
In addition, if the user specifies the type signature then the rtc of `P` must be the same as the type constructor specified by the type signature.
|
|
|
|
|
|
|
|
|
In the case where all the patterns are polymorphic, a user must provide a type signature but we accept the definition regardless of the type signature they provide.
|
|
|
The type constructor for the whole set of patterns is the type constructor as specified by the user. If the user does not provide a type signature then the definition is rejected as ambiguous.
|
|
|
|
|
|
|
|
|
This design is a consequence of the design of the pattern match checker. Complete sets of patterns must be identified relative to a type.
|
|
|
This is a sanity check as users would never be able to match on all constructors if the set of patterns is inconsistent in this manner.
|
|
|
|
|
|
### Examples of Typing
|
|
|
|
|
|
```
|
|
|
patternP::()patternP=(){-# COMPLETE P #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
Accepted, the type of the match is `()` as the rtc of `P` is `()`.
|
|
|
|
|
|
```
|
|
|
patternP::()patternP=(){-# COMPLETE P :: () #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
Accepted, the type of the match is `()` as the rtc of `P` is `()` and this is the same as the user specified type which is `()`.
|
|
|
|
|
|
```
|
|
|
patternP::()patternP=(){-# COMPLETE P :: Int #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
Rejected as the user specified type signature is not the same as the rtc of `P`. (`Int /= ()`)
|
|
|
|
|
|
```
|
|
|
patternP::()patternP=()patternQ::Maybe a
|
|
|
patternQ=Nothing{-# COMPLETE P, Q #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
Rejected: the rtc of `P` and `Q` is different.
|
|
|
|
|
|
```
|
|
|
patternP::()patternP=()patternQ::()patternQ=(){-# COMPLETE P, Q #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
Accepted, the type of the whole set is `()` as this is the rtc of both `P` and `Q`.
|
|
|
|
|
|
```
|
|
|
classC f where
|
|
|
match :: f a ->()patternP::C f => f a
|
|
|
patternP<-(match ->()){-# COMPLETE P #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
Rejected. All the conlikes are polymorphic but no type signature is provided
|
|
|
|
|
|
```
|
|
|
classC f where
|
|
|
match :: f a ->()patternP::C f => f a
|
|
|
patternP<-(match ->()){-# COMPLETE P :: () #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
Accepted. All the conlikes are polymorphic but a type signature is provided.
|
|
|
|
|
|
```
|
|
|
classC f where
|
|
|
match :: f a ->()patternP::C f => f a
|
|
|
patternP<-(match ->())patternQ::()patternQ=(){-# COMPLETE P, Q #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
Accepted. There is one polymorphic conlike `P` but there is also a monomorphic conlike `Q` which fixes the type of the whole set. Therefore the type of the whole match is `()`.
|
|
|
|
|
|
```
|
|
|
patternP::[Int]patternP=[5]patternQ::[Char]patternQ=['a']{-# COMPLETE P, Q #-}
|
|
|
```
|
|
|
|
|
|
|
|
|
Accepted. The rtc of `P` and `Q` is `[]`. This is despite the fact that `P` and `Q` could never be used in the same pattern match. The check is there as a convenience to the user.
|
|
|
|
|
|
# Examples
|
|
|
|
... | ... | @@ -73,42 +203,22 @@ patternN::Maybe a |
|
|
patternN=Nothing{-# COMPLETE N, Just #-}qux::Maybe a ->BoolquxN=Falsequx(Just x)=True
|
|
|
```
|
|
|
|
|
|
# Discussion
|
|
|
|
|
|
|
|
|
Obviously this feature allows nefarious users to define any set of patterns as complete. This is a consequence of the flexibility of the design.
|
|
|
|
|
|
## Error Messages
|
|
|
|
|
|
|
|
|
The pattern match checker checks each set of patterns individually and combines the results together at the end. The current naive algorithm tries to choose the result where the set of redundant and uncovered matches are both empty. If there is no such set then it prefers results with few uncovered cases, ties being broken by the number of redundant clauses.
|
|
|
When the pattern match checker requests a set of constructors for a type constructor `T`, we now return a list of sets which include the normal data constructor set and also any `COMPLETE` pragmas of type `T`.
|
|
|
We then try each of these sets, not warning if any of them are a perfect match. In the case the match isn't perfect, we select one of the branches of the search depending on how good the result is.
|
|
|
|
|
|
|
|
|
We write `C: R<n> U<m>` for the result of matching `C` which has `n` redundant matches and `m` uncovered cases.
|
|
|
The results are prioritised in this order.
|
|
|
|
|
|
1. Fewest uncovered clauses
|
|
|
1. Fewest redundant clauses
|
|
|
1. Fewest inaccessible clauses
|
|
|
1. Whether the match comes from a `COMPLETE` pragma or the build in set
|
|
|
|
|
|
For example, for two complete matchings `C1` and `C2`, then
|
|
|
|
|
|
<table><tr><th> Match Result 1 </th>
|
|
|
<th> Match Result 2 </th>
|
|
|
<th> Chosen Result </th>
|
|
|
<th> Reason
|
|
|
</th></tr>
|
|
|
<tr><th>`C1: R<0> U<0>`</th>
|
|
|
<th>`C2: R<n> U<m>`</th>
|
|
|
<th>`C1`</th>
|
|
|
<th>`C1` is a perfect matching so the function is total.
|
|
|
</th></tr>
|
|
|
<tr><th>`C1: R<1> U<1>`</th>
|
|
|
<th>`C2: R<0> U<2>`</th>
|
|
|
<th>`C1`</th>
|
|
|
<th>`C1` has fewer uncovered clauses.
|
|
|
</th></tr>
|
|
|
<tr><th>`C1: R<2> U<0>`</th>
|
|
|
<th>`C2: R<1> U<0>`</th>
|
|
|
<th>`C2`</th>
|
|
|
<th>`C1` and `C2` have the same number of uncovered clauses but `C2` has fewer redundant clauses
|
|
|
</th></tr></table>
|
|
|
of data constructors for a type constructor.
|
|
|
|
|
|
|
|
|
It may be desirable to produce a summary of the results in a more intelligent way. Exploration of this is left open for further discussion. |