[Agda] Bin._<_

[Serge D. Mechveliani]

On Fri, Aug 03, 2012 at 01:37:34PM -0400, James Deikun wrote:
> On Thu, 2012-08-02 at 17:04 +0400, Serge D. Mechveliani wrote:
> > People,
> > I have a beginner question. Probably, it is on usage of  lib-0.6.
> > 
> > Please, what stands for "<" for Bin  (binary naturals) ?
> > I need to test a binary variant for `length' and `lookup':
> 
> You really have about 5 options here:
> 
> 1) Use qualified prefix syntax:
> 
>    open import Data.Nat
>    open import Data.Bin as Bin
> 
>    [later ...] Bin._<_ a b
>
> [..]


So, I try it to compare two binary naturals obtained by applying
fromBits: 

----------------------------------------------------------------
module Lookup where
open import Data.Bool
open import Data.String
open import Data.Digit
open import Data.List
open import Data.Nat
open import Data.Bin as Bin
open import Foreign.Haskell
open import IO.Primitive

open import Prelude hiding (IO; putStrLn)

l : Bin
l = fromBits (0b :: 1b :: [])  

n : Bin
n = fromBits (0b :: 1b :: 1b :: [])

b : Set          -- ? what must be is its type?
b = Bin._<_ n l

main : IO Unit
main =  putStrLn (toCostring (show b))
----------------------------------------------------------- 

1. What does this mean `[later ..]'  in

>   [later ...] Bin._<_ a b
?

2. Data.Bin  of  lib-0.6  declares

--------------------
infix 4 _<_

-- Order relation. Wrapped so that the parameters can be inferred.

data _<_ (b1 b2 : Bin) : Set where
  less : (lt : (Nat._<_ on toNat) b1 b2) -> b1 < b2
--------------------

(I replaced math symbols). 

2.1. I am looking into the reference manual page of
 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Keywords

and do not find the keyword `on'. What does `on' mean?
Does it mean here that  less b1 b2  is evaluated via conversion to 
unary Natural, as 
                 (toNat b1) < (toNat b2) ?

If so, then I do not need it, because I intended a fast comparison, and
toNat  has an exponential cost.

2.2. Apart from the computation cost, what to set in my program instead 
     of   b = Bin._<_ n l   in order to obtain a Boolean value for 
comparison of these two binaries?

2.3. It is difficult for a newbie to understand these things.
     Can people comment the meaning of the declaration

     data _<_ (b1 b2 : Bin) : Set where
       less : (lt : (Nat._<_ on toNat) b1 b2) -> b1 < b2

in Data.Bin in lib-0.6 ?
What may be examples of its usage  a) in ordinary computation,  
b) may be, in a proof 
?
Does it imply that   _<_ : Bin -> Bin -> Set,
that _<_ takes two binaries and returns a  small abstract type with
operation `less' ?
Probably, the returnd type is non-empty  iff  (toNat b1) < (toNat b2) 
-- ?
What is the type of the argument of `less' ?
What does it denote the last occurence of `<'  (in `b1 < b2'),
is it the one from  `data _<_' ?


3. I hope one can program fast ordering comparison on Bin 
   (linear cost in the bit list length) by applying toDigits and by 
comparing the bit lists. But maybe lib-0.6 already has something for this?

A bit of philosophy:
generally, I have an impression that Agda cares more for proofs than 
for an ordinary computation support. Providing proofs via types is 
interesting, all right (needs investigation).
I and some other people need a language (and compiler) which _also_ 
gives possibility to formulate efficient algorithms for a real-world 
mathematics. Something like this:  Haskell + GHC + dependent types. 
For example, having an algorithm of  O(n^3),  it is not appropriate to 
replace it with a program of  O(2^n),  neither even of  O(n^4),  despite
even possible proof simplification for various algorithm properties.
The reason is evident.
Also the very algorithm formulation must be as simple as possible, for
readability. To what extent a program can be complicated in order to 
accomodize it for proofs -- this may be a question. 
Also I expect that on the real _today_ practice, 99% of proofs would 
appear by an human thinking and typing the hints to the system. Still 
this may be useful, due to the possibility of automatically checked 
certificates. Because a human often gives an erroneous proof, and such  
are stopped by the proof assistant.

Thank you in advance for explanation,

------
Sergei