[Agda] Raw natural numbers

[Alan Jeffrey]

I'm afraid there's still a coercion left, for example (# 2) ends up as:

   (MAlonzo.Data.Natural.d2
     (Unsafe.Coerce.unsafeCoerce
       (MAlonzo.Data.Nat.mazIntegerToNat
         ((2) :: Integer))))

so can't be optimized.

The fix for this particular instance is to add an FFI binding to 
Data,Nat, but boy it would be nice to have a coerce function that played 
well with RULES.

A.

On 10/21/2010 01:44 PM, Jeffrey, Alan S A (Alan) wrote:
> I'm building the new compiler now...  Fingers crossed!
>
> A more general solution to the problem of unsafeCoerce getting in the
> way would be for Agda to use its own coerce function, defined something
> like:
>
>     {-# INLINE [1] coerce #-}
>     coerce = Unsafe.Coerce.unsafeCoerce
>
>     {-# RULES "coerce-id" forall (x :: a) . coerce x = x #-}
>
> This would at least remove all the identity coercions, and would allow
> other FFI bindings to define their own RULES.
>
> A.
>
> On 10/21/2010 04:48 AM, Ulf Norell wrote:
>>
>> On Thu, Oct 21, 2010 at 12:22 AM, Alan Jeffrey<ajeffrey at bell-labs.com
>> <mailto:ajeffrey at bell-labs.com>>  wrote:
>>
>>      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.
>>
>>
>> I removed the unnecessary coercion of integer literals, so now you get
>>
>>     Unsafe.Coerce.unsafeCoerce (mazIntegerToNat ((10) :: Integer))
>>
>> instead of
>>
>>     Unsafe.Coerce.unsafeCoerce (mazIntegerToNat
>> (Unsafe.Coerce.unsafeCoerce ((10) :: Integer)))
>>
>> when using natural number literals. I also changed the implementation of
>> mazNatToInteger/IntegerToNat to
>>
>> mazNatToInteger
>>     = \ x ->  case x of { C2 ->  0 :: Integer; C3 x ->  1 + (mazNatToInteger
>> (Unsafe.Coerce.unsafeCoerce x)) }
>> mazIntegerToNat
>>     = \ x ->  if x<= (0 :: Integer) then C2 else C3
>> (Unsafe.Coerce.unsafeCoerce (mazIntegerToNat (x - 1)))
>>
>> (where C2 and C3 are the constructor names for zero and suc). Hopefully
>> this will help a little.
>>
>> / Ulf
>