The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Vadim,

 

I need to decide for a larger library development if I am going to use type classes or canonical instances. I would like to learn how bad instance resolution can get. I have quite some experience with getting normal eauto (not for instance but for goal resolution) behave well. If you could share an example, I might be able to help you getting it more well behaved and at the same time learn about the issues one might have.

 

Best regards,

 

Michael

 

From: vadim.zaliva AT west.cmu.edu [mailto:vadim.zaliva AT west.cmu.edu] On Behalf Of Vadim Zaliva
Sent: Saturday, June 11, 2016 10:07 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Typeclasses vs canonical instances

 

 

On Mon, Apr 25, 2016 at 2:41 PM, Gregory Malecha <gmalecha AT gmail.com> wrote:

1/ They do not have as predictable of a resolution mechanism (it is essentially [eauto with typeclass_instances]), and it is invoked later. My understanding is that (morally) the entire term is constructed with holes and then type class resolution tries to solve each hole that exists and has a type that is declared as a class (either using 'Class xxx := ...' or 'Existing Class xxx.'). In addition typeclass resolution has a tendency to loop infinitely when things go wrong which can be very annoying.

For what it worth, I would like to share my personal frustration with type classes. They worked for me just fine until my project grew big enough. Now, each my type class resolution stucks, I start painful sequence of steps trying to split goal into simpler ones trying to find where it stucks. Sometimes limiting the depth of the search helps, but you need to find just the right depth, below which it fails and above which resolution runs forever. Even more frustrating is when I split the goal and debug type class problems for parts of it, but combining things together makes it stuck again.  I am planning to look at canonical structures as alternative, but meanwhile there are few things I wish to know/exist:

 

1. Analysing type class resolution debug logs is not easy. I wish somebody explain clearly how resolution works, and what different log messages means (backtracking, exact, etc.) I have some intuitions but I feel that there are certain patterns like, loops, or branches where search get stuck could be derived from logs with simple scripting.

 

2. I want better control of type class resolution. Oftentimes, looking at the _expression_ I can sketch sequence of steps which will get all type class dependencies resolved. Unfortunately I could not control if resolver goes other way. It is painful to see it trying search in wrong direction. The only mechanism to control this I know about is class instance priorities, but they are static and I could not re-assign them. Some kind of hint mechanism for type class resolution would be great.

 

It would be great to hear some tips and tricks from people who spent more time dealing with problems like.

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928