4 ms·
I still don't understand how one can express a concept such as monoid or group in, say, Haskell. One option is typeclasses, but they don't actually let you expr
by js8 11y ago
I still don't understand how one can express a concept such as monoid or group in, say, Haskell. One option is typeclasses, but they don't actually let you express the laws.. Furthermore, sometimes the laws require more than one different objects, or objects which satisfy some other laws and so on recursively.
I can see how one can start from types, but I don't see how one can start from abstract algebra (or categories or something). That is, possibly not to have fully specified objects that you work with.
- theseoafs 11y agoYou can't, not with Haskell. (Maybe you can, I don't know, with some really insane extensions and type-level programming. It wouldn't be nice.) Haskell's approach is: write out the typeclass and the implementations, and you can probably safely assume that the "natural" implementation of the typeclass will satisfy the laws. Dependently typed languages are what you use for this kind of thing.
- js8 11y agoI agree that you can probably do that with dependent-types, I am just wondering if there is a way to do stuff like that in more simpler formalism, similar to untyped lambda calculus. I mean, in untyped lambda calculus you start with simple objects that are fully specified and you compose them to get more complex objects. I think one should be able to do the "opposite" thing, i.e. start with potentially complicated objects and restrict those down by adding relational conditions on them. So I am looking for some (minimalistic) formalism to do that, something like "lambda calculus in reverse". In classic Lisp, there were operators CAR, CDR and EQ which let you introspect any lambda expression. So maybe there should exist a formalism having these decompositional operators as primitives..
- theseoafs 11y agoYou already know it: the way you do this is with a homoiconic language. I don't know of any "formalisms" of homoiconic languages, but there's always Scheme. I don't know why this idea is relevant though. If where you're going with this is "you can write code to take in a monad instance as an input syntax tree and verify it satisfies the laws", then I assure you that's impossible in the general case.
- tel 11y agoYou should read up on Agda. Its standard library [0] does all this. [0] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.S...
- dllthomas 11y ago"I still don't understand how one can express a concept such as monoid or group in, say, Haskell." Roughly the same way one can express the concept in mathematics. You say "this set forms a monoid under that operation, with such-and-such identity element", and optionally include some argument (or, ideally, proof) that this is the case. In (traditional/most) math, that is only checked by humans. In Haskell, it is checked by humans and hopefully tests (laws often make great QuickCheck properties!).
- js8 11y agoThanks for both replies to my questions, I have asked additional question above.