[Agda] stdlib for practical programming

[Sergei Meshveliani]

On Fri, 2013-09-27 at 21:34 +0300, Dmytro Starosud wrote:
> [..]
> P.S. Just want to note, that I wasn't saying Agda cannot something or
> isn't powerful enough, the same for Standard Library. 
> [..]

Concerning `classes', I have the two notes.

1. I recall now of  "recursive instance search".
People say that Agda has not such.
And may be, the Haskell classes have such.

Can people give a simple illustration for  recursive instance search?
(to understand its meaning).

Seeing examples for recursive instance search, we could think of how to
program these examples in Agda.

2. Instance import.

When an Haskell class Foo is imported from a module M into M2, all its
instances defined in M are also imported automatically. Instances apply
as implicit: they are not named in the application place, neither they
are explicitly `open'. They work silently, in each place where an
operation  foo  from  Foo  is applied, the compiler chooses them
according to the _type of the argument_ of  foo.

In Agda, an instance for Foo is a record _value_, it needs to be
imported explicitly as a value, then, `open' individually or by {{...}}.

As a result, an Haskell programmer has less to write, but in an Agda
program it is easier to avoid ambiguity. 

Regards,

------
Sergei