[Agda] Raw natural numbers
Alan Jeffrey
ajeffrey at bell-labs.com
Thu Oct 21 00:22:34 CEST 2010
Hi everyone,
I did some simple bindings for raw natural numbers:
http://github.com/agda/agda-system-io/tree/master/src/Data/Natural
The interesting thing is that we can almost optimize away many of the
uses of unary numbers -- in particular to get constants such as #1000000
to be represented in native form rather than unary.
The idea would be to add a rule to Haskell's rewrite engine:
{-# RULES "int2nat2int" forall x .
MAlonzo.Data.Nat.mazNatToInteger (MAlonzo.Data.Nat.mazIntegerToNat x)
= x #-}
This almost works. The two things stopping it are:
a) There isn't an FFI binding for Nat (grr) which means the compiler
inserts some unsafeCoerce operations which then stop rewrites from firing.
b) The definitions of mazNatToInteger and mazIntegerToNat define a local
variable, which isn't in scope for rewriting.
Fixes:
a.1) Give FFI bindings for Nat. It would be nice to have these anyway.
a.2) Have the compiler emit its own coerce operation, which inlines to
unsafeCoerce in a later phase of rewriting, so earlier phases can
rewrite it. This would be useful for other optimizations, e.g. stream
fusion.
b) Clean up the emitted code to be:
mazNatToInteger C0 = 0 :: Integer
mazNatToInteger (C1 x) = 1 + mazNatToInteger (coerce x)
mazIntegerToNat x | x <= (0 :: Integer) = C0
mazIntegerToNat x | True = C1 (coerce (mazIntegerToNat (x - 1)))
These minimal changes would allow Agda access to native natural numbers.
A slight improvement on unary arithmetic!
A.
More information about the Agda
mailing list