[Agda] stdlib for practical programming

[Andreas Abel]

Hej Dmytro,

I would be happy if someone would take over the Agda Prelude and develop 
it further.  It was the Master project of Frederic Kettelhoit, but it 
seems he is no longer maintaining it.

The latest version is on github:

   https://github.com/fkettelhoit/agda-prelude

Maybe you can get into contact with Frederic about contributing, or you 
fork it and develop it further...

Cheers,
Andreas (from ICFP)

On 27.09.2013 14:34, Dmytro Starosud wrote:
> 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
>>
>>
>>
>>
>>
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/