[Agda] Bin._<_

[James Deikun]

On Sat, 2012-08-04 at 15:34 +0400, Serge D. Mechveliani wrote:
> 1. What does this mean `[later ..]'  in
> 
> >   [later ...] Bin._<_ a b
> ?

It means you write your Agda code, and somewhere later on in that code
you use the expressions to the right of [later ...]

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

'_<_' in Agda is not actually a comparison function, it is a type
representing the statement that its left operand is less than its right
operand.  It 'represents' this in the sense that values of this type
only exist in the case that the left operand is less than the right
operand.

Because of the use of 'on' (or rather '_on_', which i think is defined
in Function.agda in the stdlib) and toNat, a value of type b1 < b2 is
exponentially large.  Fortunately if you only intend a boolean
comparison, and if you use a lazy compiler backend like the default
MAlonzo, there is no need to actually construct a value of this type
(you will throw it away without pattern-matching on it, and the
non-normalized term that will be constructed during the comparison is
much smaller).

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

To perform your actual boolean comparison, you will want to use _<?_
from StrictTotalOrder (the internal module in Relation.Binary) and
\lfloor_\rfloor from Relation.Nullary.Decidable.  Here is an example:

   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 Relation.Binary using (module StrictTotalOrder)
   open import Relation.Nullary.Decidable

   open import Prelude hiding (IO; putStrLn)

   open StrictTotalOrder Bin.strictTotalOrder using (_<?_)

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

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

   b : Bool
   b = \lfloor n <? l \rfloor

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

> 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

Taking your questions out of order, so the explanation makes more sense:
the declaration above declares a type constructor _<_ parameterized on
two values of type 'Bin'.  The presence of the '_' in the name of the
type constructor means that the type '_<_ b1 b2' may alternately be
written as 'b1 < b2' with identical meaning.

'less' is a data constructor for any type constructed by the type
constructor '_<_'.  'less' takes an explicit argument of type '(Nat._<_
on toNat) b1 b2', which may also be written '_on_ Nat._<_ toNat b1 b2'.
'less' also takes two implicit arguments, b1 and b2, of type Bin which
are necessary to fully determine the type of its explicit argument and
its return value.  When applied to such arguments, 'less' returns a
value of type 'b1 < b2'.

An example of the use of '_<_' in ordinary programming:

   lookup : forall {A} (l : List A) i -> (i < binLength l) -> A
   lookup [] i () -- this case can't happen, checked at compile time
   lookup (x \:: xs) 0# _ = x
   -- this example is incomplete; the rest of the code goes here

Data.Bin contains several examples of the use of '_<_' in proofs.

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

As I said, Data.Bin already includes the 'cmp' function which quickly
compares Bins by their bitlists.  Exponential expense is only incurred
when expanding the proof terms it generates to their fully-evaluated
forms, which hopefully is usually only necessary in cases where you are
iterating on the Bin anyway.

> 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 cannot speak for the philosophy of Agda as I am not one of the Agda
developers, but in practice it seems that Agda has focused more on
providing good notation and foundations for verified programming than on
the nitty-gritty things like optimization, nice build systems, an
extensive library ecosystem, and so on.  Not that these things are not
planned; they just don't seem to have been the central focus yet.

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

Idris is a language perhaps more focused on providing a practical
programming language first and verifiability second, but it is also at a
very early stage of its development and in my opinion not usable for
medium-sized or large programs yet.

To be honest, I don't think there is any dependently-typed language that
is truly suitable for large-scale application programming at this time,
but if I had to pick one (if for example I had a contract or a grant) I
would pick Coq for high-level programs or ATS for low-level ones.

And if you do want to implement a computer algebra system in Agda, it
would be more practical to use the Fast library found at
http://github.com/xplat/potpourri/ along with a darcs version of Agda,
rather than using Data.Bin with released Agda.  The Fast library focuses
on taking full advantage of all features available in the Agda reference
implementation for the acceleration of natural number arithmetic in
order to provide types, functions and proofs that perform well at both
compile-time and runtime.  (Full disclosure: I am the author of the Fast
library.)