[Agda] main, IO, agda -c, Nat and Float

[Alan Jeffrey]

On 10/16/2010 06:17 AM, Nils Anders Danielsson wrote:
> On 2010-10-16 11:24, Oscar Finnsson wrote:
>> Finally I got a question regarding Nat. Will
>>   >  value100000 : Nat
>>   >  value100000 = 100000
>> be stored as
>>   >  suc (suc (suc (suc (suc (suc (suc (suc (.... 100000 times ...)
>> or will the compiler realise that it can just store 100000?
>
> What does "just store 100000" mean? Unary numbers are represented in
> unary form also after compilation. One can probably do better: I've been
> told that Idris checks if a type is structurally isomorphic to the unary
> natural numbers, and if it is a different representation is used.

AFAICT, we can almost do this in out-of-the-box Agda: we could add a 
COMPILED_DATA pragma to bind Nat to an appropriate Haskell Natural type 
(e.g. an ADT wrapper round Integer).  Unfortunately there seems to be a 
deal-killer, in that Haskell allows (n+k) patterns, e.g.:

   f (x+1) = x
   f 0     = 0

but not (+k)n patterns, e.g.:

   g ((+1)x) = x
   g 0       = 0

The simplest language extension I can think of that would allow bindings 
of Agda datatypes to arbitrary Haskell types would be to support views 
in the FFI (e.g. http://hackage.haskell.org/trac/ghc/wiki/ViewPatterns). 
  Recall:

    class View a b where
       view :: a -> b

The pragma declaration would be something like:

   COMPILED_VIEW Nat Natural Zero Suc

where we translate zero to (view Zero), suc x to (view (Suc x)) and a 
case expression to:

   case view y of Zero -> ... ; Suc x -> ...

that is, the same translation only with the magic word "view" on the 
front.  The FFI writer then provides the appropriate view instances:

   data Natural' = Zero | Suc Natural

   instance View Natural Natural' where
     view 0 = Zero
     view (n + 1) = Suc n

   instance View Natural' Natural where
     view Zero = 0
     view (Suc n) = n + 1

This would allow other nice binders, e.g. making Bytestring look like a 
list type to Agda, binding Agda integers to Haskell Integer, binding 
Agda products to Haskell products, etc.

The more extreme version would be to include view types in Agda, which 
would require some syntax for declaring a new type X with carrier Z to 
be an initial F-algebra (for an existing datatype F : Set -> Set) after 
which X can be treated as if it were declared as a datatype.  This would 
be very tricky to get right though, e.g. there is an iso X -> Z to worry 
about: which eta/beta properties should hold for it?  Also, what about 
other functors, not just Set -> Set?  What about terminal F-coalgebras? 
  etc. etc. etc.

A.

>
>> (btw, the source code (Builtin.hs) mention a bunch of builtins. Is
>> there any documentation over what the different buildins stand for?
>
> There is some documentation in the following file:
>
>     http://code.haskell.org/Agda/examples/Introduction/Built-in.agda
>
> --
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda