coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Typeclass instance derivation, Merlin Göttlinger, 01/11/2018
- Re: [Coq-Club] Typeclass instance derivation, Matthieu Sozeau, 01/11/2018
Archive powered by MHonArc 2.6.18.