[Haskell-cafe] A question about algebra and dependent typing
Jacques Carette
carette at mcmaster.ca
Mon Jul 14 21:03:10 EDT 2008
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
More information about the Haskell-Cafe
mailing list