-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 7/2/10 04:04 , Heinrich Apfelmus wrote:

Jorden M wrote:

...

C++ `Concepts', which almost made it into the C++0x standard, are roughly similar to Haskell type classes. The proposal for concepts in C++ had a feature called axioms, which allow the programmer to specify semantics on the functions the concept contains. This allows for enforcing things such as the Monad Laws, as well as letting the compiler make certain optimizations it may not have been able to make without axiomatic guarantees.

I have a hard time imagining that axioms are being used to prove properties about programs in a language such as C++... :) Any pointers?

I just took a look at it, and Concepts look to me like Haskell contexts/constraints; an example is:

concept LessThanComparable<typename T> { bool operator<(const T& x, const T& y); }

template<typename T> requires LessThanComparable<T> const T& min(const T& x, const T& y) { return x < y? x : y; }

which is obviously just an Ord costraint on min(). (My initial thought before looking at this was that it was programming by contract, or possibly just making invariants explicit; the latter wouldn't actually prove anything, though.) - -- brandon s. allbery [linux,solaris,freebsd,perl] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkwuAfYACgkQIn7hlCsL25URBQCeOsh3m3jfmifLeG8kzLC6Df74 PU4AoJwho/HN9IClcBw6RTN6kzVxRvX1 =B0SX -----END PGP SIGNATURE-----

On Fri, Jul 2, 2010 at 4:04 AM, Heinrich Apfelmus wrote:

Jorden M wrote:

...

C++ `Concepts', which almost made it into the C++0x standard, are roughly similar to Haskell type classes. The proposal for concepts in C++ had a feature called axioms, which allow the programmer to specify semantics on the functions the concept contains. This allows for enforcing things such as the Monad Laws, as well as letting the compiler make certain optimizations it may not have been able to make without axiomatic guarantees.

I have a hard time imagining that axioms are being used to prove properties about programs in a language such as C++... :) Any pointers?

That is not what they are for. Axiom is probably not a good choice of terminology. Axioms let a concept enforce certain statements about functions inside the concept. E.g., in a concept that describes addition, one could use an axiom statement to enforce commutativity of that addition operation. There seems to be no way to do this in Haskell, hence my question.

...

Why does Haskell not have a similar functionality in its type classes? Was there not time, desire, etc.? Or are there technical limitations?

If you want to exploit algebraic identities like, say,

   map f . map g = map (f . g)

for program optimization, you can use the RULE pragma in GHC.

If you want to use the axioms to prove your program correct, you are beginning to leave the scope of Haskell. Have a look at dependently typed languages and proof assistants like  Agda  and  Coq . For instance, the latter can extract Haskell programs from proofs.

That being said, enforcing invariants in the types, using quickcheck and good old pen & paper calculations can carry you a long way towards program correctness in Haskell.

Certainly. My question was as to why there isn't something like this right in the syntax for type classes. Seems like it would go a long way, esp. for things like enforcing the monad laws.

Regards, Heinrich Apfelmus

-- http://apfelmus.nfshost.com

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

On Sun, Jul 4, 2010 at 3:15 AM, Heinrich Apfelmus wrote:

Jorden M wrote:

...

Heinrich Apfelmus wrote:

...

Jorden M wrote:

...

C++ `Concepts', which almost made it into the C++0x standard, are roughly similar to Haskell type classes. The proposal for concepts in C++ had a feature called axioms, which allow the programmer to specify semantics on the functions the concept contains. This allows for enforcing things such as the Monad Laws, as well as letting the compiler make certain optimizations it may not have been able to make without axiomatic guarantees.

I have a hard time imagining that axioms are being used to prove properties about programs in a language such as C++... :) Any pointers?

That is not what they are for. Axiom is probably not a good choice of terminology. Axioms let a concept enforce certain statements about functions inside the concept. E.g., in a concept that describes addition, one could use an axiom statement to enforce commutativity of that addition operation. There seems to be no way to do this in Haskell, hence my question.

Now that I've had a really short look at Axioms, I think the Haskell equivalent would be QuickCheck properties. After all, Axioms are not enforced by the compiler, their only effect is documentation. Granted, they

Really? I thought they were.

are part of the source code, but frankly, I don't see how this has more effect than stating invariants as QuickCheck properties or writing them down in a comment.

Would it make sense to try to formalize things like the monad laws using QuickCheck?

Regards, Heinrich Apfelmus

-- http://apfelmus.nfshost.com

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

On Sun, Jul 4, 2010 at 11:16 AM, Daniel Fischer wrote:

On Sunday 04 July 2010 16:05:48, Jorden M wrote:

...

...

Now that I've had a really short look at Axioms, I think the Haskell equivalent would be QuickCheck properties. After all, Axioms are not enforced by the compiler, their only effect is documentation. Granted, they

Really? I thought they were.

I think that's not even possible in general.

It would equate to solving the Halting Problem, I suppose. The point of axioms for compiler use must then have been to say, `All right, assume this is true and make optimizations if possible.' A bit fast and loose in the presence of careless programmers, no? At least calling them axioms makes more sense.

Generally, you can't decide the equality of functions [okay, we're dealing with finite domains in a computer, so in principle one could check all possible inputs, but even for a small type like uint64_t, that's impractical].

...

...

are part of the source code, but frankly, I don't see how this has more effect than stating invariants as QuickCheck properties or writing them down in a comment.

Would it make sense to try to formalize things like the monad laws using QuickCheck?.

To a certain extent. You'd have a good chance to catch gross violations of the monad laws with QuickCheck. But for subtle violations, the odds are minuscule.

I wonder if the effort to do so would be useful.

On Mon, Jul 19, 2010 at 6:05 AM, Ozgur Akgun wrote:

On 4 July 2010 16:41, Jorden M wrote:

...

On Sun, Jul 4, 2010 at 11:16 AM, Daniel Fischer wrote:

...

On Sunday 04 July 2010 16:05:48, Jorden M wrote:

...

...

Now that I've had a really short look at Axioms, I think the Haskell equivalent would be QuickCheck properties. After all, Axioms are not enforced by the compiler, their only effect is documentation. Granted, they

Really? I thought they were.

I think that's not even possible in general.

It would equate to solving the Halting Problem, I suppose.

Nope, it would just take long (ok, very long) to compute. Halting problem is undecidable in general.

No, I think Daniel is right -- it is not possible in general. It's essentially verifying the behavior of a program, which is how the Halting Problem is framed. Here we're looking at something more general than `is the behavior of this program such that it halts?'.