[Agda] stdlib for practical programming

[Dmytro Starosud]

Great! Thank you Andreas
That's exactly what I was looking for.

Best regards,
Dmytro

2013/9/27 Andreas Abel <andreas.abel at ifi.lmu.de>:
> 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/