Checkable "minimal complete definitions"
#6028 (closed) suggested warning on cyclic unimplemented defaults. This doesn't work for the reasons mentioned there, among others (also e.g. `Alternative` has mutually recursive some and many methods, which shouldn't be warned about). Figuring out when to warn automatically seems hard.
But Haskell already has an ad-hoc mechanism for specifying which methods need to be implemented: A "minimal complete definition" specified in the comments of almost every class definition that has optional methods. Unfortunately comments are aren't compiler-checked. It seems that the simplest solution would be to specify these in a way that the compiler can understand.
The obvious approach is to add a pragma for it in the class definition. In particular, one could write a pragma for each "minimal set" of definitions, and the compiler could warn if none of them are implemented (and suggest which methods to implement). This lets us keep the convenience of default method implementations without losing safety. Without any pragmas, the compiler could fall back to the set "all methods without defaults", which is what it uses now.
It might look something like this:
class Functor m => Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
m >>= f = join (fmap f m)
join :: m (m a) -> m a
join m = m >>= id
{-# MINIMAL return, join #-}
{-# MINIMAL return, (>>=) #-}
class Eq a where
(==), (/=) :: a -> a -> Bool
x == y = not (x /= y)
x /= y = not (x == y)
{-# MINIMAL (==) #-}
{-# MINIMAL (/=) #-}Trac metadata
| Trac field | Value |
|---|---|
| Version | 7.6.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #6028 (closed) |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |
Activity
added Tfeature request Trac import labels
changed milestone to %7.8.1
I would prefer that the minimal implementation specification is a logical expression consisting of ANDs and ORs. This way we can better show, what has to be implemented always and where choices exist. That is, instead of
{-# MINIMAL return, join #-} {-# MINIMAL return, (>>=) #-}I prefer
{-# MINIMAL return AND (join OR (>>=)) #-}I also wonder whether it is possible for GHC to make some plausibility checks. E.g., if a method has no default implementation and is not mentioned in the MINIMAL specification, this should cause a warning.
Attached file
0001-Implement-checkable-minimal-complete-definitions-tra.patch(download).Patch to implement # MINIMAL # pragma and checking
I took it upon myself to implement this functionality. The attached patch adds support for a minimal pragma.
Here is an example:
class Monad f where return :: a -> f a fmap :: (a -> b) -> f a -> f b join :: f (f a) -> f a bind :: f a -> (a -> f b) -> f b {-# MINIMAL return, fmap, join #-} {-# MINIMAL return, bind #-} instance Monad Foo where return = undefined fmap = undefinedWill generate the warning:
Warning: No explicit implementation for some methods. Minimal complete definition: ‛return’, ‛fmap’, and ‛join’ or ‛return’, and ‛bind’ In the instance declaration for ‛Monad Foo’I took the simplest approach, where multiple pragmas give alternative minimal complete definitions. So they need to be specified in conjunctive normal form. There is not yet a check for whether all methods without a default are mentioned in each minimal complete definition, I plan to add that.
I decided to replace the old warnings for missing methods with this new style. If no MINIMAL pragma is given, a minimal complete definition is generated automatically based on the methods that don't have defaults.
Also, as you notice, right now all methods are reported in the warning. It might be better to generate a shorter warning that only mentions missing methods. But that would complicate the code a bit.
It is perhaps important to note that this changes the interface files, since the minimal complete definitions need to be stored.
It's disjunctive normal form, isn't it? I wanted to add, that a class like Floating would really benefit from logical formulas without a normal form. Expressing that 'log' can be expressed in terms of 'logBase' and vice versa is complicated because you have to repeat all remaining methods. And 'sinh' and 'cosh' can be expressed in terms of 'exp' and vice versa. Then it becomes a combinatorical problem to list all terms of the normal form.
Design: Lemming's point is an excellent one. I think a single MINIMAL pragma with an and/or structure is a very plausible (and more scalable) alternative. It's a bit more fiddly to implement, but not much.
Implementation
- Needs user documentation in due course
- The check currently happens in the type checker, which is already very complicated. Couldn't it happen in the renamer, which has less complex clutter. After all, we are only looking for
Nameshere, not types. - You've made minimal pragmas into a whole separate definition group, with consequential extra parameters. Couldn't they just be a form of
Sig, like SPECIALISE pragmas? It think that would be a lot simpler.
Simon
A good error message could be obtained by setting all variables for implemented methods to TRUE and simplify the logical expression using the simple laws "TRUE OR a = TRUE" and "TRUE AND a = a". E.g. if minimal definition specification is
((sin AND cos) OR tan) AND ((sinh AND cosh) OR exp)and "tan" is implemented, then error message should be:
Missing implementations: ((sinh AND cosh) OR exp)The same way we can do a plausibility check for MINIMAL pragmas: GHC could report whether there is a MINIMAL implementation that leaves a method unimplemented. It could work as follows: For every method without a default implementation set the corresponding variable to FALSE in the MINIMAL logic expression. If the expression can be reduced to FALSE, everything is ok, since this means that if the method is not implemented then the MINIMAL specification is not met. If the expressions does not reduce to FALSE, report an error with the simplified expression. E.g. if minimal definition specification is again
((sin AND cos) OR tan) AND ((sinh AND cosh) OR exp)and there are default implementations for "cos", "tan", "sinh", "cosh", "exp", but not for "pi" and "sin", then GHC should emit the warning:
"pi" would remain unimplemented, if you implement only ((sin AND cos) OR tan) AND ((sinh AND cosh) OR exp). "sin" would remain unimplemented, if you implement only (tan AND ((sinh AND cosh) OR exp)).Lemming:
I agree that a more expressive syntax could be useful. It would mean that we need to add a datatype for boolean formulas to Ghc, though.
data BooleanFormula a = Var a | And [a] | Or [a]Wrt. plausibility check for MINIMAL pragmas: Is this really worth it? Do we really need a warning to warn people that they might not be getting enough warnings? I would think that the people who use MINIMAL pragmas are experienced library writers, and they would use the feature carefully. IMO it is not worth the extra cost to add this check.
Simon:
I put the check in the type checker, because that is also where the current warnings spring from. You are right that it should be possible to move it to the renamer.
I was under the impression that
Sigis for things that are attached to a single name. Is that not true? After renaming, the minimal complete definition definitely needs to be a part ofClass. By that time there is nowhere else to put them.The reason that in the source syntax I also put the minimal complete definitions in
ClassDeclis that they don't make sense outside of a class. If I were to make them aSig, then the data type also allows them at top level. Now that I say that, I realize there is still aMinimalDefDconstructor forHsDecl, which should be removed since the parser already moves them into theClassDecl.@twanvl Due to Murphy's law every mistake that can be made will be made. :-) If you experiment with a class, e.g. add new methods or remove some default implementations you may easily forget to update the MINIMAL pragma. I hope that the warnings I proposed could be implemented relatively easy. I think there should also be the phrase "Possible fix: add default implementation or extend MINIMAL pragma."
I don't mind very much whether the pragma uses DNF or more complicated boolean expressions, but the uppercase OR/AND syntax seems very grating to me (also, it could be valid Haskell syntax: what if you define an associated type called AND or OR?). Some syntax like "|" and "," (which already mean "or" and "and", and are already reserved) seems more reasonable (and also easier to lay out in multiple lines).
I agree that everything without a default implementation should be required to be listed in a MINIMAL pragma (if you use one at all; this behavior is like ExplicitForall). After all, the informal "minimal complete definition" in documentation specifies everything you need to implement. The pragma isn't just for the compiler, it's for the reader.
Trac metadata
This might be a bit of feature creep, but I thought I would try to archive a bit of #haskell discussion: it might be worth thinking about how to do cross-class MINIMAL pragmas. For example, imagine a world where we had something like this:
{-# LANGUAGE DefaultSignatures #-} class Functor f where fmap :: (a -> b) -> (f a -> f b) default fmap :: Traversable f => (a -> b) -> (f a -> f b) fmap = getId . traverse (Id . f) class Functor f => Traversable f where traverse :: Applicative f => (a -> f b) -> t a -> f (t b) traverse f = sequenceA . fmap f sequenceA :: Applicative f => t (f a) -> f (t a) sequenceA = traverse idI might like to be able to say that either "fmap and sequenceA" or "traverse" are okay minimal definitions for the two classes together.
twanl: your points are valid, but I still vote for putting it in
Sig. TheSPECIALISE instancepragmas for an instance decl are inSig, for example (SpecInstSigconstructor). AndGenericSigis valid only in a class decl, and nowhere else. It's true that, as a result, theSigdata type isn't as precise as it could be, but lumping them together reduces the number of fields, arguments, and plumbing. A judgement call, I agree, but doing it this way would be consistent with what we have.Once we get all the way to a
Class, then indeed we need a special purpose field. I'm only talking aboutHsSyn.mentioned in issue #8017 (closed)
Twan did an implementation, and there was some ensuing discussion (above) about
- The design
- Aspects of the implementation
- In the end it needs documentation and tests
I think it's a useful feature, but it needs someone to run with it. I'm sure Twan wouldn't mind if someone took up when he left off.
Simon
I found some time to polish the patch. I tried to address the points mentioned on this ticket.
- The pragma is now parsed as a Sig instead of a separate declaration.
- The minimal complete definitions are now specified with a boolean formula. For example
{-# MINIMAL return, ((>>=) | (join,fmap)) #-}- A warning is generated if the MINIMAL pragma does not cover all methods without defaults.
- I have added documentation to the user_guide.
- I have added some tests to the testsuite.
The things I did not do:
- dmwit sugested that the check should also extend to parent classes. I did not implement this, because it would complicate the patch significantly. Right now names are resolved locally to a class, and the information about whether a method is implemented is also kept per instance.
- simonpj sugested that the check be moved from the typechecker to the renamer. However, to check that an instance satisfies the minimal complete definition, you need the
Class. But that is only known after (or during) typechecking. The typechecker also does things like collecting default implementations. All of that is needed before the minimal complete check can be performed. In the end the inTcInstDclcheck is only a couple of lines, I doubt it can be done much simpler.
Some other remarks:
- I put the function
defaultClassMinimalDef, which constructs a default minimal complete definition, inBuildTyCl. It would be more at home inTcClassDcl. But there is also a function in vectorize that constructs Classes and so it also needs defaultClassMinimalDef. - I had to change the interface format. So a full rebuild is needed.
- It would be nice to include the minimal complete definitions in Haddock documentation.
Attached file
0001-Implement-checkable-minimal-complete-definitions-tra.v2.patch(download).Attached file
0001-Tests-for-MINIMAL-pragma-7633.patch(download).testsuite patch
I just read through the patch, and it seems to be useful and well-done.
Minor point: The call to
warnMissingMethodOrATcan be removed instead of just commenting it out.There is a new call to
mkClassin http://git.haskell.org/ghc.git/blob/17a868afa169c52d8525a95cbed87b2fc12044c6:/compiler/prelude/TysWiredIn.lhs#l478, so the patch needs to be updated again slightly.mentioned in commit b549d689
mentioned in commit bd42c9df
mentioned in commit b6d90d10
mentioned in commit f9007960
mentioned in commit 1c5fee15
mentioned in commit 1b608a0d
twanvl: I feel that work you've done could use more comments. Could you add some more explanation what and why the code does? I'm thinking mostly about !BooleanFormula module - there is no comment explaining its purpose ("Boolean formulas without negation (qunatifier free)" is a bit criptic!) and design decisions that you've made (in 2 or 3 months you will not remeber them!). Thanks
mentioned in commit 690b7e49
mentioned in commit 1320fd2e
Twan, looking at module
BooleanFormulaI see various functions likemkAndandmkOrthat seem to be enforcing some invariants on theBooleanFormulatype. There is the notion of a formula being "simplified". But what precisely is that notion? If I usemkAndetc, what properties does the resultingBooleanFormulahave?For example, I think there will be no immediately-nested
AndorOrconstructors. But what else?Why are these invariants important?
It would be great if you could add some
Note [Blah...]notes in theBooleanFormulamodule to explain. Thanks!Simon
Replying to [ticket:7633#comment:75129 simonpj]:
The implementation has a special case for methods whose name starts with an underscore. The user guide doesn't mention this. Could it please do so?
Btw, I noticed the documentation added contains the following paragraph:
<para>If no MINIMAL pragma is used, then all methods without a default will be requried, excluding methods with a name that starts with an underscore.</para>Replying to [ticket:7633#comment:75131 hvr]:
<para>If no MINIMAL pragma is used, then all methods without a default will be requried, excluding methods with a name that starts with an underscore.</para>Should be: "requried" -> "required"
The exclusion of underscored identifiers would make more sense, if there is a barrier for using underscored identifiers as suggested in #4959.
mentioned in commit ab86ebd2
As far as I can tell the only remaining work is adding comments to source code, as in ticket:7633#comment:74884 and ticket:7633#comment:75128.
assigned to @trac-twanvl
Attached file
0001-Added-comments-to-BooleanFormula-to-explain-the-expr.patch(download).Commenting the BooleanFormula code
mentioned in commit 332eba9d
mentioned in issue #8854 (closed)
Interested in an experience report? I added MINIMAL pragmas to numeric-prelude classes. I did several mistakes when transferring human description to MINIMAL pragma, mostly mixing up comma and bar. These mistakes were revealed by instances that gave wrong alarms. However one alarm was serious and spotted a missing method implementation in a cycle of default definitions.
added Pnormal label
