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

[Nils Anders Danielsson]

On 2012-04-23 17:55, James Deikun wrote:
> 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.

As far as I've understood things you can avoid computing the equality
proofs and the Acc witness at run-time. I'm not sure how much benefit
you would get at compile-time.

> 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?

In Idris the module that does forcing, detagging and collapsing is less
than 150 lines long, and Idris has meta-variables. Perhaps irrelevance
would pose a problem.

-- 
/NAD