3 ms·

What I find weird about Haskell and its touted equational reasoning and all, is that there doesn't seem to be any program for aiding in and/or checking these pr

by Dewie 12y ago

What I find weird about Haskell and its touted equational reasoning and all, is that there doesn't seem to be any program for aiding in and/or checking these proofs. (All examples of it I've seen are 'with pen and paper'. And while that might be a great/good enough way for beginners, I would expect that bigger/more serious applications of it would welcome the chance of having a program verify the proof steps for them.) It doesn't seem that hard, at least when it comes to these algebraic proofs; let the programmer build up proofs and lemmas by applying legal equational substitutions. Then let him reuse them in new proofs. The only responsibility of the program might be that it checks that all transitions are legal. Then you just have a verifier/checker, not even an automatic prover or anything. Does anything like this exist?

MaxGabriel 12y ago
There's a good screencast of this being done with Idris, which has tools like you mentioned for interactively solving proofs. In it, the author proves that an instance of Monoid upholds its 'laws': properties like associativity that are only upheld by convention in Haskell. https://www.youtube.com/watch?v=P82dqVrS8ik https://www.youtube.com/watch?v=P82dqVrS8ik
lomnakkus 12y ago
It's a continuum of how much checking/proving you want to do. Assuming that all Monoid instances obey the monoid laws is a pretty reasonable thing to do even if you haven't proven every single instance yourself. It's the same as assuming that a Set<T> in e.g. Java actually obeys the set abstraction: has no duplicates, ordering is not guaranteed, etc. In practice the laws associated with type classes are a bit better specified in Haskell via either terse (algebraic) documentation or default implementations of associated functions. It would perhaps be nice if libraries which export type classes came with test functions that could be used to test your instances using some sort of QuickCheck-like approach. Though I've personally found that Haskell is sufficient at least my purposes, Idris currently seems the most "practical" of the dependently typed languages, but it's quite young and doesn't really have any ecosystem to speak of AFAICT.

by Dewie 12y ago

MaxGabriel 12y ago

There's a good screencast of this being done with Idris, which has tools like you mentioned for interactively solving proofs. In it, the author proves that an instance of Monoid upholds its 'laws': properties like associativity that are only upheld by convention in Haskell. https://www.youtube.com/watch?v=P82dqVrS8ik https://www.youtube.com/watch?v=P82dqVrS8ik

lomnakkus 12y ago

It's a continuum of how much checking/proving you want to do. Assuming that all Monoid instances obey the monoid laws is a pretty reasonable thing to do even if you haven't proven every single instance yourself. It's the same as assuming that a Set<T> in e.g. Java actually obeys the set abstraction: has no duplicates, ordering is not guaranteed, etc. In practice the laws associated with type classes are a bit better specified in Haskell via either terse (algebraic) documentation or default implementations of associated functions. It would perhaps be nice if libraries which export type classes came with test functions that could be used to test your instances using some sort of QuickCheck-like approach. Though I've personally found that Haskell is sufficient at least my purposes, Idris currently seems the most "practical" of the dependently typed languages, but it's quite young and doesn't really have any ecosystem to speak of AFAICT.