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?