[Agda] stdlib for practical programming

[Sergei Meshveliani]

On Thu, 2013-09-26 at 22:44 +0300, Dmytro Starosud wrote:
> OK, I see I should have been more precise.
> Yes, Standard library is "some library" but it doesn't allow enough
> level of overloading.
> What I need? A lot of stuff.
> In particular I need map (fmap, _<$>_ whatever) function which will
> work for any functor (Maybe, List, Vector, Product, mapable; IMapable
> whatever).

In  Haskell  this is achieved by the  
                     language feature of constructor classes.

For example,  Functor  is a constructor class defined in the Haskell's
library:

  class Functor c where fmap :: (a → b) → c a → c b              
                        -- fmap f (c a) --> c (f a)           

-- if I recall correctly! 
Here  c  ranges over unary type constructors.
For example,  c  may be  List, Maybe, ...  
 
I think that Agda does not need any additional language feature for
this. This notion of Functor  
(let us call it  FMap,  because I am not sure that Haskell's `Functor'
means something close to Functor of the category theory)

is easily expressed via dependent types and records:

  record FMap (Cons : Set → Set) :  Set (suc 0ℓ)
         where
         field  fmap : {A B : Set} → (f : A → B) → Cons A → Cons B

(I skip the Level arguments, so far).
Here  Cons  correponds to  `c'  in Functor of the Haskell library.

This c FMap  an be set into Standard library.

But I suspect that Standard library already has something for this, 
may be something better.

Who knows, please, has it?

Anyway here is an example of using overloading for  fmap  via the above
FMap  `class':

---------------------------------------------------------------------
module FMap where
open import Level        using (suc) renaming (zero to 0ℓ)
open import Data.Bool    using (Bool; true; false)
open import Data.Nat     using (ℕ)
open import Data.Product using (_×_; _,_)
open import Data.List    using (List; []; _∷_)
open import Data.Maybe   using (Maybe; just; nothing)           

-- First, define various instances for FMap.
-- Such instances can be easily defined and set into the library:
 
listFMap : FMap List                  -- here Cons == List
listFMap = record{ fmap = fmap-l }
           where
           fmap-l : {A B : Set} → (f : A → B) → List A → List B
           fmap-l _ []       =  []
           fmap-l f (x ∷ xs) =  (f x) ∷ (fmap-l f xs)

maybeFMap : FMap Maybe                -- here Cons == Maybe
maybeFMap = record{ fmap = fmap-mb }
            where
            fmap-mb : {A B : Set} → (f : A → B) → Maybe A → Maybe B
            fmap-mb f nothing  = nothing
            fmap-mb f (just a) = just (f a)
---------------------------------------------------------------------------

Example of usage:

  g : Maybe Bool → Maybe ℕ → Maybe ℕ × Maybe Bool  
  g mbBoo mbN =  (fmap f mbBoo , fmap h mbN)
    where
    open FMap maybeFMap

    f : Bool → ℕ
    f true  = 1
    f false = 0

    h : ℕ → Bool
    h 1 = true
    h _ = false

We see that  fmap  is used as overloaded.


> I don't want import renaming ten modules just to do some simple things.
> I was asking for library, which simplifies all this work.
> e.g. I would like following:
> 
> open import Prelude -- Prelude is this wanted "some library"
> {- many useful stuff here -}
> 
> instead of:
> 
> open import Level renaming (zero to zeroL; suc to sucL; \lub to \lubL)
> open import Data.Nat renaming (zero to zeroN; suc to sucN; \lub to \lubN; ...)
> open import Data.List renaming (map to mapL; foldr to foldrL; ...)
> open import Data.Vector renaming (map to mapV; foldr to foldrV; ...)
> open import Data.Product renaming (map to mapP; ...)
> etc. ...
> etc. ...
> etc. ...
> 
> {- many useful stuff here -}
> 

This `sugar' can (probably) be done by 
    
     importing `classes' (done as records) and instances 
     instead of separate functions.

If Haskell and its library is considered as all right in this import
matters, what is wrong with the Agda library in this point? 

For example, instead of  zero  and  suc,  one can import  
DistributiveLattice  and its several instances
(NatProp.distributiveLattice, Foo.distributiveLattice, ...)

(a contrived example)
and then to use overloading by  open DistributiveLattice {{...}}
and such. 
This will give importing items by _groups_. 

For example,  0#, 1# _+_; _*_   do not need to be renamed, because one
can import the `classs' RingWithOne and several its instances.

Introducing more `classes' and instances will support this style
further.

If I needed a single      module Prelude  

which exports "everything I may needed", I could try to write
  
  module MyPrelude where
  open import Foo1 using (...) renaming (...)
  open import Foo2 using (...) renaming (...)
  ...
  somewhat use  "open ... public",

-- and do most of the import by `classes' and instances.
  
I hope,
this will join and re-export the needed things.

I used this approach in Haskell to create a union  DPrelude  of
MyProperPrelude  and  a large part of  Standard library. 

How people think, will a similar approach work in  Agda?

(And as to my personal taste, I (currently) prefer to specify explicitly
what is imported from each small module, because this way it is easier
to control, to debug, to maintain
).

Regards,

------
Sergei