Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]

James Deikun james at
Mon Apr 23 17:55:37 CEST 2012

On Mon, 2012-04-23 at 16:34 +0200, Nils Anders Danielsson wrote:
> On 2012-04-23 15:37, James Deikun wrote:
> > The current stdlib implementation is clever, but thanks to depending
> > on optimizations Agda still doesn't implement, it can take about 25
> > seconds to reduce the product of two rationals (involving no more than
> > 2-digit arithmetic).
> I think you refer to the following comment:
>    -- Note that Induction.Nat.<-rec is used to establish termination of
>    -- division. The run-time complexity of this implementation of integer
>    -- division should be linear in the size of the dividend, assuming
>    -- that well-founded recursion and the equality type are optimised
>    -- properly (see "Inductive Families Need Not Store Their Indices"
>    -- (Brady, McBride, McKinna, TYPES 2003)).
> Note that at least one of these optimisations (collapsing) is a
> /run-time/ optimisation.

I knew full collapsing was only available at runtime, but I wasn't aware
that division was depending on it for its time bound; that certainly
strengthens my point.

The typechecking-time optimizations from that paper could already make
asymptotic improvements on a lot of uses of Fin and the comparator
types, as well as Vecs and so forth; are there known bad interactions
with things like metavariable inference that exclude them, or does it
seem more like the proverbial Small Matter of Programming?

More information about the Agda mailing list