[Agda] stdlib for practical programming

[Dmytro Starosud]

Ok, thank you.
I've understood, will implement my own Prelude.

P.S. Just want to note, that I wasn't saying Agda cannot something or
isn't powerful enough, the same for Standard Library. I just asked if
someone had already written "Prelude" library for practical
programming. For me it would be more convenient to use uniform way
instead of reinvented one. But now I see everyone does it :-)

Best regards,
Dmytro

2013/9/27 Sergei Meshveliani <mechvel at botik.ru>:
> 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
>
>
>
>
>
>