[Agda] Agda Digest, Vol 98, Issue 3

[Dominique Devriese]

All,

2013/10/4 Matthieu Sozeau <matthieu.sozeau at gmail.com>:
> 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.

Agreed, considering everything in scope for instance resolution seems
unrealistic in the presence of a recursive search.  The approach of
Coq's type classes to separate type classes from other types indeed
strongly restricts the set of candidates, but it has downsides as
well.  An alternative would be to use something like Scala's
"implicit" annotations, which mark a value as eligible for use in
instance resolution.  In such an approach, an annotation like
  instance listEq : forall {t} ->  {{eqT : Eq t}} -> Eq (List t)
                 listEq = ...
could play a role similar to a Haskell parametric instance
  instance Eq t => Eq (List t) where ...

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

True.  However, canonical structure resolution is still less
principled/more powerful than for example Haskell's parametric
instance resolution.  The computational model for canonical structures
is essentially like "Prolog with backtracking", as has been
demonstrated and exploited by Gonthier et al.:
http://dl.acm.org/citation.cfm?id=2034798.  As a side note, canonical
structures being not very well documented, Gonthier et al. had to
reverse engineer the precise working of the resolution and have
described the results in a technical appendix:
  http://www.mpi-sws.org/~beta/lessadhoc/appendix.pdf

Regards,
Dominique