[Haskell-cafe] 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080714/206f449f/attachment.htm