The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 26 août 2014, at 19:08, Kevin Sullivan 
<sullivan.kevinj AT gmail.com>
 wrote:

> I'm trying to use typeclass inheritance (using :>) to model a 
> specialization hierarchy in which subclasses provide values for certain 
> fields that are declared but left abstract in a superclass. This seems not 
> possible. Can someone (a) confirm, and (b) suggest an alternative design 
> pattern. 
> 
> The problem: it appears that a super-typeclass has to be fully instantiated 
> before one can instantiate a subclass, but values defined in a subclass are 
> unavailable until the subclass is instantiated -- catch 22. 
> 
> In a little more detail, I want to provide an implementation, in a 
> subclass, of a function that is declared but not defined in a type 
> superclass. The implementation is defined in terms of other functions 
> introduced in the subclass.

Hi Kevin,

  I don’t think I’ve seen this pattern yet and indeed it seems it can’t work 
in the current system the way
you describe it. I can only think of using propositional equalities to do 
that:

Class SubClass A := { sup : SuperClass A; …; spec : fn sup = bar }

Best,
— Matthieu