Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Typeclass instance derivation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Typeclass instance derivation


Chronological Thread 
  • From: Merlin Göttlinger <megoettlinger AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] Typeclass instance derivation
  • Date: Thu, 11 Jan 2018 11:41:34 +0000
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f42.google.com
  • Ironport-phdr: 9a23:x1IvZBFIrA/jA72Ey+R++p1GYnF86YWxBRYc798ds5kLTJ78o82wAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6yaJUAD/AFPeZZqYnyv1oAtR2iBQmwAOPvyzlIhnDo0q0gzu8sFgTG0xIvH9IJrnvUsMn1NKMTUeCzw6nH0y/DYuhZ2Tf48ofIcxQhreuQUrJ3dMrc0E8iHB7GgFWIsYHpIS+Z2+AXv2WY7+dsT/yjh3Mopg1rrTWj2MEhgZTTiI0P0FDL7yB5zZ41JdKmTE57ZsapEJ5KuCGbM4t6W8IiQ310tCojxL0LtoC3cDIFyJQgwB7fZPiHfJaS7h3/U+aRJC90hHNjeL2hmxa/6VasxvH4W8Wu01tHrjBJnsfRun0CzRDe5daLRuN4/ki72DaP0w7T6vtDIUAxjafbLoAuwrE3lpUNrUTDAiv2mETwjK+ZaEok4POl6+viYrr8p5+cM5V4hR35MqQrgsC/G/g3MhASX2iH/uSxzKHs/UrgQLlTkvI2lrTZv4vBKMQApq+5BhdV3Zw55xa+CTemytUYkmMdIFJLYhLUx7TubhvFJ+m9BvOiiXytli1qzrbIJPepVp7KNz3IlKrrVbd78U9VjgQpm4Nx/ZVRX5QMOvbyXHjeKsDECh4/PAGui7LiBdp6258CXWOJDaKDGKzXuF6MoOkoJr/fN8cupD/hJq19tLbVhngjlApFJPj77d4scHm9W89eDQCcaHvojM0GFD5T7AU7Re3uzlaFVGwKPirgb+cH/jg+TbmeI8LbXIn02e6O2S66GttdYWUUUgnRQ0etTJ2NXrI3UAzXIsJllWZZB72oSotk1A328QGmkfxoKe3b/iBevpXmhoB4

Hi,

I'm trying to "derive" typeclass instances from existing tpeclass instances by functoriality of the typeclasses.
So given a instance (ta : TC A) that is covariant in A and a function (f : A -> B) I would like to write something like (fmap f ta : TC B).
Depending on the shape of the typeclass it might also be contravariant or more likely invariant requiring two functions (ab : A -> B) (ba : B ->A).
To generalise this I wrote a typeclass Invariant (encoded with the CPS trick discussed recently). Implementing the instances of this has one issue however:

Class BPL m := { 
  verum : m;
  falsum : m;
  prop : atom -> m;
  nomi : nom -> m;
  conj : m -> m -> m;
  disj : m -> m -> m;
}.

Global Instance bpl_invar : Invariant (F := BPL) := fun r f => f {| imap__ A B := fun ab ba fa =>
        {| verum := ab verum;                                                           falsum := ab falsum;
           prop p := ab (prop p);
           nomi n := ab (nomi n);
           conj a b := ab (conj (ba a) (ba b));
           disj a b := ab (disj (ba a) (ba b))
         |}
|}.

This leaves me with a wrong type for fa resulting in a missing Instance.

A : Type
B : Type
ab : A -> B
ba : B -> A
fa : (fun B : Type => BPL B) A

?BPL : "BPL A"

if you wrap the inner record creation in let _ : BPL A := fa in ... it works as expected.

Why isn't the type of fa reduced without this wrapper? 
Is there a better way to do what I want to do?

Cheers,
Merlin



Archive powered by MHonArc 2.6.18.

Top of Page