A question about algebra and dependent typing

[Nathan Bloomfield]

There's something I want to do with Haskell, and after tinkering for a while I think it's not possible. Before giving up entirely, I thought I'd try this mailing list.

 

I'm working on an abstract algebra library, using the "types are sets" strategy. For the algebraists out there, I'm trying to implement as much as I can of "Abstract Algebra" by Dummit & Foote in Haskell. I've got a Ring class definition that looks approximately like

 

> class Ring t where

>   (<+>) :: t -> t -> t

>  (<*>) :: t -> t -> t

>  neg :: t -> t

>  zero :: t

 

So, for example, we can say

 

>instance Ring Integer where

>  (<+>) = (+)

>  (<*>) = (*)

>  neg = negate

>  zero = 0

 

From here I can subclass to domains, PIDs, EDs, UFDs, fields, et cetera, and write some useful algorithms in great generality. The ring R[x] can be modeled by the type [r], direct products are tuples, and fractions in the domain r have type Fraction r. I can even model the set (i.e. type) of nxn matrices over a ring using type-level integers as demonstrated in the paper "Number-Parameterized Types" by Oleg Kiselyov [1]. All good stuff.

 

However, I'm running into problems modeling some other useful and computationally interesting things, in particular adjoining an algebraic element and taking a quotient by an ideal. For example, I've tried the following (using GHC extensions):

 

>class (Ring r) => Ideal i r | i -> r

>

>data (Ring r) => FinGenIdeal r = Ideal [r]

>

>instance (Ring r) => Ideal (FinGenIdeal r) r

>

>data (Ring r, Ideal i r) => Coset r i = r :+: i

 

But of course I can't say

 

>instance (Ring r, Ideal i r) => Ring (Coset r i) where

>  (r :+: i) <+> (s :+: j) = (r <+> s) :+: i

>  zero = zero :+: ?

>  ...

 

It shouldn't make sense to add 2 :+: Ideal [3] and 3 :+: Ideal [5], for example, and zero is ambiguous. This problem happems because Ideal [3] and Ideal [5] have the same type, namely FinGenIdeal Integer.

 

I am pretty new to Haskell and type theory, but I think what I'm wanting is dependent types. So, for instance, the type of Coset r i is parameterized by an particular value in FinGenIdeal r. Is there another way around this? I'm sure there is some sophisticated type-fu one could perform (similar to the examples in [1]) to construct ideals of integers, tuples of integers, et cetera, but this would quickly get unwieldy and sacrifices some generality. I have heard lots of praise of GADT as an approximation to dependent types, but I don't yet see how they could apply in this situation.

 

Has anyone else encountered a similar problem, and if so, how did you get around it? Would I be better off working in a dependently-typed language like Agda?

 

[1] - http://okmij.org/ftp/papers/number-parameterized-types.pdf

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Henning Thielemann]

On Mon, 14 Jul 2008, Nathan Bloomfield wrote:

> There's something I want to do with Haskell, and after tinkering for a while
> I think it's not possible. Before giving up entirely, I thought I'd try this
> mailing list.
>
> I'm working on an abstract algebra library, using the "types are sets"
> strategy. For the algebraists out there, I'm trying to implement as much as
> I can of "Abstract Algebra" by Dummit & Foote in Haskell. I've got a Ring
> class definition that looks approximately like

It follows my usual pointer to NumericPrelude where some
algebraic structures are implemented including residue classes.
However a quotient by a general ideal is missing.
   http://darcs.haskell.org/numericprelude/src/Number/ResidueClass/Func.hs
   http://hackage.haskell.org/cgi-bin/hackage-scripts/package/numeric-prelude

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Claus Reinke]

> I'm working on an abstract algebra library, using the "types are sets"
> strategy. For the algebraists out there, I'm trying to implement as much as
> I can of "Abstract Algebra" by Dummit & Foote in Haskell. I've got a Ring
> class definition that looks approximately like

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" }

Claus
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Derek Elkins]

On Mon, 2008-07-14 at 13:00 -0500, Nathan Bloomfield wrote:
> There's something I want to do with Haskell, and after tinkering for a
> while I think it's not possible. Before giving up entirely, I thought
> I'd try this mailing list.
>  
> I'm working on an abstract algebra library, using the "types are sets" strategy. For the algebraists out there, I'm trying to implement as much as I can of "Abstract Algebra" by Dummit & Foote in Haskell. I've got a Ring class definition that looks approximately like
>  

I haven't read most of the rest of this email, but you might want to
look at Serge Mechveliani's DoCon library if you haven't already:
http://www.haskell.org/docon/
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe