[Agda] Agda Digest, Vol 98, Issue 3

[Matthieu Sozeau]

Hi all,

  Let me add to the discussion that trying to restrict the current Coq's type classes
to be more principled has been on my mind for quite some time as well, but it is 
frustratingly difficult to find a sweet spot that satisfies all reasonable use cases. 
Something like a prolog/twelf-like system could do the trick, with static analyses 
ensuring the termination and determinism/unicity of solutions of logic programs, and a
good notion of unification/matching but scaling this to the very computational setting 
of type theory does not look easy, typically dealing with instances built by recursion 
on some datatype or requiring unfoldings of constants. And indeed, this complicates 
the system by adding another computational paradigm, but I think that's unavoidable 
given the desired openness of classes and quite powerful unification strategy needed. 

Coq's system has only the restriction that classes are declared and only instances of 
classes are considered during resolution, allowing for a relatively efficient retrieval of 
instances based on discrimination nets and avoiding as much as possible trying to convert
with everything in the context. There is an admittedly ugly backdoor using arbitrary Ltac
tactics to infer instances, but it is not necessary to use it when doing simple, 
Haskell-style classes.

The canonical structures provide with a more principled approach, restricting to a
well delimited set of unification problems.

Best,
-- Matthieu

On 2 oct. 2013, at 23:21, David Darais <darais at seas.harvard.edu> wrote:

> 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
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda