[Agda] class inheritance

Nils Anders Danielsson nad at chalmers.se
Fri Aug 10 23:11:19 CEST 2012


On 2012-08-10 21:06, Serge D. Mechveliani wrote:
> this is on inheritance of `classes' (records), in Agda and in
> Standarad library (lib-0.6).

The approach used in the library (sharing by parametrisation, or
Pebble-style sharing) is documented in the README. There are other
approaches, see for instance Randy Pollack's "Dependently Typed Records
in Type Theory", which I have mentioned before on this list:

   Re: Avoiding implicit argument proliferation?
   http://thread.gmane.org/gmane.comp.lang.agda/2674/focus=2713

-- 
/NAD


More information about the Agda mailing list