Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] multiple typeclass instance question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] multiple typeclass instance question


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] multiple typeclass instance question
  • Date: Wed, 9 Mar 2016 22:37:30 -0500
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f47.google.com
  • Ironport-phdr: 9a23:pafGdxQZqXbTAIFbqA0Uu+8FEdpsv+yvbD5Q0YIujvd0So/mwa64Zx2N2/xhgRfzUJnB7Loc0qyN4/+mCTNLv8vJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuDPE4W2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzA0lRxBHwjM6lneU5bvvy3m/r5/3y+bPsDyQL0cVjGr7qMtQxjt3nRUfwUl+X3a35QjxJlQpwis8kRy



On 03/09/2016 10:11 PM, Jason Gross wrote:
Axiom A : Type.
Existing Class A.
Axioms a a' : A.
Existing Instances a a'.

Class MultiA (n : nat) {x : A} := dummy : list A.

Hint Extern 0 (@MultiA 0 ?x) => (exact nil) : typeclass_instances.
Hint Extern 0 (@MultiA (S ?n) ?x) => (let prev := constr:(_ : @MultiA n _)
in
match eval cbv beta in prev with
| context[cons x _] => fail 1
| ?prev' => exact (cons x prev')
end) : typeclass_instances.
Goal True.
pose (_ : MultiA 2). (* m := ((a :: a' :: nil)%list : MultiA 2) : MultiA
2 *)

There's probably a way to do this without giving the length of the list
ahead of time, but I hope this gives a bit of insight into the model I'm
using of typeclass resolution hackery.

OK - I think I get it. So, the backtracking must occur entirely within the extern hints? The list is then needed to accumulate the results seen during backtracking. It's unfortunate that the context search is needed each time. This must get really slow when the number of A's gets large.

I think the length of the list could be eliminated by having a dedicated first (or highest cost) instance of A that the second hint uses to know to stop looking for more.

Thanks, Jason! Now I have to see if I can repackage this to use...

-- Jonathan





Archive powered by MHonArc 2.6.18.

Top of Page