[Agda] Re: Agda Digest, Vol 98, Issue 3

[David Darais]

I want to echo Edward's statement, and support the argument that the lack of type classes is an enormous limitation in Agda.

It turns out that type classes are also extremely useful for proof developments (as opposed to "just" programs) in dependently typed languages, and Coq users have already seen lots of the benefits of this.  Although Coq's type class mechanism is much less principled than Haskell's, in that it is extremely easy to get it to diverge and difficult to reason about.  This is because they plugged all of type class resolution into an eauto hint database.  One can hope to do much better.

I don't see how you could hope to "generalize" the type class mechanism by writing type-level functions inside the logic of Agda.  Type class resolution is about *static* recursive term construction, and as your static universe of types grows, so must your instance resolution be open to new mappings.  Sure, there is some hope that we could get a closed, recursive construction of, say, Eq instances, as an agda-level function using universes and generic programming.  But there will be classes for which one doesn't want to define all instances for in one go.

Type classes give you added expressivity (recursive term construction), and this expressiveness comes necessarily from the fact that resolution happens statically, and outside the logic.  Yes, adding type classes to your languages makes it a little more complicated, but it never touches the core type theory, and the simple version (basic recursive search) is really not *that* crazy.  At least not any crazier than instance arguments, which are much less principled than type classes (find an arbitrary term in scope with the right type), and doomed to forever be inefficient with their current semantics.

So I restate the question: what is the real barrier to adding type classes to Agda?  Do you believe that in the end we don't need them, or that they can be generalized by Agda functions?  Then us advocates of type classes should provide more compelling examples of their expressive power.  Do you believe it adds too much complexity to the language?  Then us advocates should propose a non-obtrusive resolution system that cleanly elaborates to core, similar in spirit to the design of instance arguments.  If not these… what is the barrier?

Best,
David

On Oct 2, 2013, at 3:28 PM, Edward Kmett <ekmett at gmail.com> wrote:

> I just want to mention as a data point the lack of recursive instance search is one of the things that prevents me from actively writing more Agda code today. Almost nothing I want to say is first-order enough that it can infer any arguments I actually want to use, and libraries like lens can't usefully be ported to Agda without it.
> 
> I would love to have a more principled story though, so I understand the current motivations, they just keep me stuck waiting in the wings. ;)
> 
> -Edward

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131002/368fd674/attachment.html