Seeking comments on an implementation of quotients and rationals

[Cliff Harvey]

Rationals would be an important part of many things I'd eventually like to do with Idris. The implementation I've written is almost certainly not ideal, and I'm curious about any particular suggestions you may have about how to do it better.

First I made an extremely simple definition of a Quotient class, requiring only a canonical projection function (for rationals, this is fraction simplification of course):

class Quotient a where

  proj : a -> a

This definition isn't quite fully general, since it may not always be clear how to choose a canonical representative of a given equivalence class, however this approach is sufficient for all the examples I've considered implementing. And it has the advantage of making clear that the equivalence respects the reflective, symmetric and transitive properties, since equality of the equivalence class is just regular equality under the projection. A fully general implementation would need something like an equivalence test function (~~) : a -> a -> Bool, which wouldn't be as nice or easy to use I don't think. 

Now to the rationals. My definition of them is here. In particular I made a strictly positive variant Fraction along with the general rational number data type Rational. Both have all the requisite operations of the Num class. In both cases I wanted to ensure that only valid numbers could be represented, so I also made a data type representing strictly positive natural numbers to serve as the denominator for both. I called this type NNat and defined it as simply a wrapper around a Nat. I judged this to be the least-worst option, better than either A) using only a Nat but interpreting it as 'plus one' the nominal value, which would inevitably be confusing or B) requiring a proof that it's nonzero, which would probably make defining functions on it at least burdensome (unless we subvert the type checker).

My hope was that since both the numerator and denominator are represented as essentially Nat containers, they would inherit some of the special optimizations applied to Nats. This may be the case, but I still was able to run into trouble with it pretty quickly. I threw together a quick test program, and the compiled program cried uncle when asked to simplify 8328075 / 2436 ("Segmentation fault: 11") but it seems to work reasonably well with anything much smaller than that. I'm curious how unavoidable this kind of limit is.

It seems like this may hinge on what I've heard described as a more ambitious long-term goal of Idris, which is to somehow intelligently transform ADTs into more efficient representations. Am I correct that that's what would be required? Can anyone tell me, is there some easy-to-state conceptual reason this is difficult? Is it just an issue of being a large task? Or maybe its a genuinely difficult and subtle problem?

I realize for the time being that primitive-based types like Integer might dramatically outperform their ADT counterparts, but an ADT-based Rational type may still be good to have. Even if they're not yet very practical to use yet, maybe they're worth having around to allow other things to be defined, and perhaps they could be useful in some performance benchmarks or something. Or maybe one of you has a good idea for how to make them better. In any case, I'm interested in hearing thoughts.

[Jon Sterling]

Hello,

In case anyone is interested, I have a not-near-finished embedding of
Observational Type Theory in Idris, which allows proper quotients.
Here's the traditional encoding of the rationals as a quotient:
https://github.com/jonsterling/ETT-Playground/blob/master/examples.idr.
I haven't tried testing its performance of course; there are some
optimizations that can be made to the representation, probably.

As you note, a lot of quotients can be got in intensional type theory by
means of a canonical projection, though, so perhaps that's enough.

Kind regards,
Jon

P.S. If you were going to try and generalize your quotient signature to
arbitrary equivalence relations, you probably would not want to restrict
it to types which have decidable equality; so you'd want a -> a -> Type
instead of a -> a -> Bool, I think.

On Mon, Mar 9, 2015, at 10:46 AM, Cliff Harvey wrote:
> Rationals would be an important part of many things I'd eventually like
> to
> do with Idris. The implementation I've written is almost certainly not
> ideal, and I'm curious about any particular suggestions you may have
> about
> how to do it better.
>
> First I made an extremely simple definition

> <https://github.com/BlackBrane/quantum/blob/master/math%2FQuotient.idr>

> of
> a Quotient class, requiring only a canonical projection function (for
> rationals, this is fraction simplification of course):
>
> class Quotient a where
> proj : a -> a
>
> This definition isn't quite fully general, since it may not always be
> clear
> how to choose a canonical representative of a given equivalence class,
> however this approach is sufficient for all the examples I've considered
> implementing. And it has the advantage of making clear that the
> equivalence
> respects the reflective, symmetric and transitive properties, since
> equality of the equivalence class is just regular equality under the
> projection. A fully general implementation would need something like an
> equivalence test function (~~) : a -> a -> Bool, which wouldn't be as
> nice
> or easy to use I don't think.
>
> Now to the rationals. My definition of them is here.

> <https://github.com/BlackBrane/quantum/blob/master/math%2FRational.idr>

> In
> particular I made a strictly positive variant Fraction along with the
> general rational number data type Rational. Both have all the requisite
> operations of the Num class. In both cases I wanted to ensure that only
> valid numbers could be represented, so I also made a data type
> representing
> strictly positive natural numbers to serve as the denominator for both. I
> called this type NNat

> <https://github.com/BlackBrane/quantum/blob/master/math%2FNNat.idr> and

> defined it as simply a wrapper around a Nat. I judged this to be the
> least-worst option, better than either A) using only a Nat but
> interpreting
> it as 'plus one' the nominal value, which would inevitably be confusing
> or
> B) requiring a proof that it's nonzero, which would probably make
> defining
> functions on it at least burdensome (unless we subvert the type checker).
>
> My hope was that since both the numerator and denominator are represented
> as essentially Nat containers, they would inherit some of the special
> optimizations applied to Nats. This may be the case, but I still was able
> to run into trouble with it pretty quickly. I threw together a quick test

> program <https://gist.github.com/BlackBrane/476acd4bf53af96dfc62>, and

> the
> compiled program cried uncle when asked to simplify 8328075 /
> 2436 ("Segmentation fault: 11") but it seems to work reasonably well with
> anything much smaller than that. I'm curious how unavoidable this kind of
> limit is.
>
> It seems like this may hinge on what I've heard described as a more
> ambitious long-term goal of Idris, which is to somehow intelligently
> transform ADTs into more efficient representations. Am I correct that
> that's what would be required? Can anyone tell me, is there some
> easy-to-state conceptual reason this is difficult? Is it just an issue of
> being a large task? Or maybe its a genuinely difficult and subtle
> problem?
>
> I realize for the time being that primitive-based types like Integer
> might
> dramatically outperform their ADT counterparts, but an ADT-based Rational
> type may still
> be good to have. Even if they're not yet very practical to use yet, maybe
> they're worth having around to allow other things to be defined, and
> perhaps they could be useful in some performance benchmarks or something.
> Or maybe one of you has a good idea for how to make them better. In any
> case, I'm interested in hearing thoughts.
>

> --
> You received this message because you are subscribed to the Google Groups
> "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to idris-lang+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.