4 ms·
This is really toy example, and there's nothing special about it. Languages like Agda, Coq, Idris support this for quite a long time. And unlike what the author
by solomatov 12y ago
This is really toy example, and there's nothing special about it. Languages like Agda, Coq, Idris support this for quite a long time. And unlike what the author wrote, all the reasoning is checked formally.
In Agda it looks like this: https://github.com/solomatov/AgdaSandbox/blob/master/Monoid.agda https://github.com/solomatov/AgdaSandbox/blob/master/Monoid.... Here we prove that in a monoid if a inverse element exists, then it's unique.
- Gabriel439 12y agoI'm actually not aware of a proof in the wild equivalent to the one in Appendix B. If you know of a machine checked proof that Applicatives lift Monoids then I would be happy to link to it.
- solomatov 12y agoI think, implementing such a proof in Agda would be a great way to learn it.
- Gabriel439 12y agoThis is an excellent suggestion. I will take a stab at this, but probably in Idris first if you don't mind. If I succeed then I will write about what I learned.
- solomatov 12y agoIf you need any help with agda, just ask.
- Gabriel439 12y agoHow do I contact you? Can I find you on the #agda channel on IRC?
- solomatov 12y agoYou can contact me via konstantin dot solomatov at google mail. I visit #agda channel from time to time.
- samstokes 12y agoGabriel, I've noticed your posts often attract this criticism - "you can do X in any language, it's not unique to Haskell". The funny thing is I don't think you ever claim that X is unique to Haskell. IMHO this (excellent) post advocates equational reasoning a lot more strongly than it advocates Haskell. Assuming your aim is to spread awareness of the advantages of pure functional programming, rather than of Haskell specifically, I wonder if your Haskell-specific domain name is muddling your message?
- Gabriel439 12y agoYeah, the domain name is misleading. It really should be called "Equational reasoning for all". I'm reluctant to change it at this point, but I think I should make more of an effort to clarify that the posts are advocacy for purely functional programming languages, including Idris in particular since it is maturing quite rapidly. Tonight I will revise this post to be less Haskell-centric by mentioning that most of what it describes applies to other purely functional languages and also mention how dependently typed languages can improve and mechanically check the proof process.