[Haskell-cafe] A question about algebra and dependent typing
nbloomf at gmail.com
Mon Jul 14 14:00:22 EDT 2008
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
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 . 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  and 3 :+: Ideal , for
example, and zero is ambiguous. This problem happems because Ideal  and
Ideal  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 ) 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
 - http://okmij.org/ftp/papers/number-parameterized-types.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe