Let's make all interfaces verified by default, i.e. rename VerifiedMonad to Monad and Monad to UnverifiedMonad #4739
Comments
nickdrozd
added a commit
to nickdrozd/Idris-dev
that referenced
this issue
Apr 6, 2020
Previously there were interfaces for Semigroup, Monoid, etc, that were
just syntactic in nature, requiring only that operations like <+> or
elements like neutral exist. There was a corresponding set of
"verified" interfaces requiring that the expected laws actually hold.
Thus Semigroup required that the <+> operation exist, while
VerifiedSemigroup required that that operation actually be
associative.
Such an arrangement is annoying for two reasons.
First, extra paperwork. If I want to show that something really is a
semigroup, I have to write two implementation blocks, the "plain"
version and the "verified" version. On the other side, if I want to
add a new interface, then in order to keep with the existing style I
need to write both a "plain" version and a "verified" version. In some
cases, like AbelianGroup, the "plain" interface is empty, since it
doesn't add any new syntactic elements.
Second, proof. Suppose a type has been declared to be a Semigroup, but
VerifiedSemigroup hasn't been implemented for it. What can be assumed
about that type? Is its <+> operation associative or not? If it isn't,
why call it a semigroup? If it is, why not prove it? And if it can't
be proved, how do we know that it's true? The big selling point of
Idris is its expressive type system and strong compile-time
guarantees, so let's take advantage of that and verify by default.
Fixing the interfaces is easy -- just move the "verified" requirements
into the "plain" interface, and that's it.
In some cases there were implementations of the "verified" interfaces,
and those could also easily be copied over. More challenging are the
cases for which there were no verified implementations. There are
three ways of dealing with them:
(1) Come up with the required proofs. This was done, for example,
with `Semigroup a => Semigroup (Vect n a)` etc in
contrib/Data/Matrix/Algebraic.idr, and also with easy ones like
Maybe and Endomorphism.
(2) Replace the interface with an "unverified" version, thereby
highlighting the fact that the expected properties have not been
proven. This was done with a few complicated data structures in
contrib, like MaxiphobicHeap and SortedBag, as well as with
primitive numeric types like Integer.
(3) Assert without proof that the laws hold using believe_me and
really_believe_me. This was done for cases in prelude and base
for which proofs are impossible (eg String) or not obvious (eg
Morphism and Kleislimorphism). Needless to say, these proofs
should be implemented where possible. If these assertions are
disliked, I would be happy to convert them to "unverified".
Note that this change only applies to those interfaces that belong to
"abstract algebra": semigroups, monoids, groups, and so on. There is a
whole other set of "plain"/"verified" interfaces dealing with
structures from "category theory". Those should also undergo this
unification, but I don't know how to do it just yet.
nickdrozd
added a commit
to nickdrozd/Idris-dev
that referenced
this issue
Apr 13, 2020
Previously there were interfaces for Semigroup, Monoid, etc, that were
just syntactic in nature, requiring only that operations like <+> or
elements like neutral exist. There was a corresponding set of
"verified" interfaces requiring that the expected laws actually hold.
Thus Semigroup required that the <+> operation exist, while
VerifiedSemigroup required that that operation actually be
associative.
Such an arrangement is annoying for two reasons.
First, extra paperwork. If I want to show that something really is a
semigroup, I have to write two implementation blocks, the "plain"
version and the "verified" version. On the other side, if I want to
add a new interface, then in order to keep with the existing style I
need to write both a "plain" version and a "verified" version. In some
cases, like AbelianGroup, the "plain" interface is empty, since it
doesn't add any new syntactic elements. This is pointless.
Second, proof. Suppose a type has been declared to be a Semigroup, but
VerifiedSemigroup hasn't been implemented for it. What can be assumed
about that type? Is its <+> operation associative or not? If it isn't,
why call it a semigroup? If it is, why not prove it? And if it can't
be proved, how do we know that it's true? The big selling point of
Idris is its expressive type system and strong compile-time
guarantees, so let's take advantage of that and verify by default.
Fixing the interfaces is easy -- just move the "verified" requirements
into the "plain" interface, and that's it.
In some cases there already existed implementations of the "verified"
interfaces, and those could also easily be copied over. More
challenging are the cases for which there do not exist verified
implementations. There are four ways of dealing with them:
(1) Come up with the required proofs. This was done, for example,
with `Semigroup a => Semigroup (Vect n a)` etc in
contrib/Data/Matrix/Algebraic.idr, and also with easy ones like
Maybe and Endomorphism. A really nice one is the new
implementation of `Ring t => Ring (Complex t)`.
(2) Assert without proof that the laws hold using believe_me. This
was done for all primitive types, including String and Integer,
since primitive types are not amenable to proof.
(3) Add postulates asserting that the laws hold. This was done for
nonprimitive datatypes for which I couldn't figure out proofs,
including Isomorphism and Morphism. I am pretty sure that the
laws hold for these cases.
(4) Revoke the name Semigroup, Monoid, etc. This was done for a few
data structures in contrib, like SortedMap and its descendants.
I am skeptical that these structures really are what they say
they are.
Note that updating an existing interface to be verified does not
require writing any proofs -- it can be done just by asserting that
the required properties hold, either with explicit postulates or with
belive_me (or even really_believe_me). There are a variety of examples
of updated implementations in this PR.
This change only applies to those interfaces that belong to "abstract
algebra": semigroups, monoids, groups, and so on. There is a whole
other set of "plain"/"verified" interfaces dealing with structures
from "category theory", like monad and functor. Those should also
undergo this unification, but I don't know how to do it just yet.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
One can find definition of VerifiedMonad here
Idris-dev/libs/contrib/Interfaces/Verified.idr
Line 170 in bc1c500
The text was updated successfully, but these errors were encountered: