[Haskell-cafe] A question about algebra and dependent typing

[Jacques Carette]

Claus Reinke wrote:
> You might find this interesting:
>
> @inproceedings{ fokker95explaining,
> author = "Jeroen Fokker",
> title = "Explaining Algebraic Theory with Functional Programs",
> booktitle = "Functional Programming Languages in Education",
> pages = "139-158",
> year = "1995",
> url = "citeseer.ist.psu.edu/fokker95explaining.html" }

Extremely interesting, thank you. It also contains a very interesting 
remark (on p. 2), noting that one should have
class Eq a => Monoid a where
(<+>) :: a -> a -> a
zero ::a

And states "Because in the lawsŠ the notion of equality is used, we 
have made Monoid a subclass of Eq". In hindsight, this is obvious, but 
is naively tempting to define a monoid without this constraint. And, 
indeed, Data.Monoid defines a Monoid class without an Eq constraint!

So, what are monoids without equality in Haskell? There are rather 
interesting beasts: they are monoids for which we have a computable 0 
(mempty) and a computable addition (mappend), but for which we cannot 
*witness* equality of the underlying carrier 'set'. This, for example, 
is the only way one can legitimately get an instance such as
instance Monoid b => Monoid (a->b)

While Haskell is used quite a lot for doing computable (or 
'extensional') mathematics, intensionality sneaks in here and there -- 
and this is just one such example.

I must admit, I actually don't yet know whether I prefer classical 
monoids or these generalized monoids where the laws are _purely_ 
intensional. Opinions?

Jacques