[Agda] Simple Agda Libraries

[Shin-Cheng Mu]

On Mon Jan 12 12:32:31 CET 2009, Lennart Augustsson wrote:
 > Actually, I find mixfix operators much more complex to parse when  
reading code.
 > But as with all custom syntax, when used correctly they can also make
 > it much easier to read.
 > > On Mon, Jan 12, 2009 at 11:26 AM, Nils Anders Danielsson wrote:
 > > Is it the use of non-ASCII characters which is problematic, or  
the use
 > > of mixfix operators?

Personally, I like the use of both unicode and mixfix operators
in the Standard Library very much --- I think they are very concise,
and look nice too, at least for the parts I use often.

I did find the learning curve using the Standard Library
a bit steep when I began to try it, however, for other reasons.
Firstly, the Haskell Prelude contains most of what I need and
I can start coding immediately, except for when I need functions
like inits, tails, etc, for which I would  "import List." And
usually that would be enough. For Agda, however, I would often
need to import a longer list of modules:

    open import Data.Empty    -- if you do some first-order logic
    open import Data.Unit     -- you'd perhaps need all of the
    open import Data.Product  -- first four modules.
    open import Data.Sum
    open import Data.Bool
    open import Data.Nat   -- if you import Vec usually you'd
    open import Data.Fin   -- need to import both Nat and Fin.
    open import Data.Vec
    open import Data.List
    open import Relation.Binary.PropositionalEquality
                -- Almost needed all the time.

One has got to be quite familiar with the Standard Lib
to know where to find what one needs. (On the other hand it's
needless to say that it's an overkill importing Evertyhing.agda.)

Secondly, I found it quite hard to dig through, for example,
    ≤-trans = IsPreorder.trans (IsPartialOrder.isPreorder
                                  (Poset.isPartialOrder poset))
to extract transitivity of some datatype. Perhaps there is
an easier way?

sincerely,
Shin