I was trying to make a form of list
restricted to just nat
and bool
.
So I did:
Inductive type : Type :=
 Int
 Bool.
Definition typeDenote (t:type) : Type :=
match t with
 Int => nat
 Bool => bool
end.
Inductive listmod (A:type) : Type :=
 mnil : listmod A
 mcons : (typeDenote A) > listmod A > listmod A.
Arguments mnil {A}.
Arguments mcons {A}.
It works okay if I try this without the implicit arguments of mcons
:
Check @mcons Int 3 mnil.
(*
mcons 3 mnil
: listmod Int
*)
Check mnil.
(*
mnil
: listmod ?A
where
?A : [  type]
*)
but gives error upon actually having the type
argument implicitly:
Check mcons 3 mnil.
(*
The term "3" has type "nat" while it is expected to have type
"typeDenote ?A".
*)
Why is this happening? And how can we get around this?
Presumably, you need bidirectional typing. Adding something like Arguments mcons {A} & h t
should help.
That said, this might not even be sufficient, since Coq still needs to invert typeDenote
, which bidirectional typing does not help with.
I don't think that this will help. Imagine what would happen if type
would have Int1
and Int2
and typeDenote
would map both to nat

But I find the error message rather strange. I would expect to get an error that Coq can't derive the implicit argument of mcons
and mnil
. What seems to be happening is that Coq silently denies to make the argument implicit  probably because there is no chance to derive it even if all other arguments are given.
You would get a message about the inability to derive the implicit argument only once no unification problems remain. Here, there is one single remaining failure: nat == typeDenote A
.
Anyway, while bidirectional typing does not solve the issue, it still helps a bit, as Coq will therefore accept mcons 3 mnil : listmod Int
.
Sorry, please forget my note about the error message  I just didn't read it properly. It is perfectly clear.
you can do some stuff with canonical structures
Inductive type : Type :=
 Int
 Bool.
Definition typeDenote0 (t:type) : Type :=
match t with
 Int => nat
 Bool => bool
end.
Record denotedType := {
reified :> type;
typeDenote :> Type;
typeDenote_ok : typeDenote = typeDenote0 reified;
}.
Inductive listmod (A:denotedType) : Type :=
 mnil : listmod A
 mcons : (typeDenote A) > listmod A > listmod A.
Arguments mnil {A}.
Arguments mcons {A}.
Canonical Structure denotedInt :=
{
reified := Int;
typeDenote := nat;
typeDenote_ok := eq_refl;
}.
Check mcons 3 mnil.
This makes Check @mcons Int 3 mnil.
fail but https://github.com/coq/coq/pull/15693 makes it work again.
Okay, we can achieve almost the same result using additional features.
Could there be some simpler way to achieve this? Am I approaching this from a wrong perspective?
I just needed a version of list
which can be used to make just boolean or nat lists (lists of other types disallowed using the new list type).
tbh listmod is useless here, you can just use list (typeDenote bla)
Can we place the 'type restriction' while constructing list objects as well?
Like cons 2 nil
being okay, but cons "hi"%string nil
being not okay.
what's the point?
you can do Definition listmod (A:denotedType) := list (typeDenote A).
and similar for mnil and mcons (that way you can still enjoy all the lemmas on list)
You mean something like this:
Definition listmod (A:type) := list (typeDenote A).
Definition mnil (A:type) : list (typeDenote A) := nil.
Definition mcons (A:type) (a:(typeDenote A))
(l:list (typeDenote A))
: list (typeDenote A) := cons a l.
Arguments mnil {A}.
Arguments mcons {A} a l.
with the canonical structure way to have implicit args?
Oh wait, I missed the denotedType
.
This worked:
Definition listmod (A:denotedType) := list (typeDenote A).
Definition mnil (A:denotedType) : list (typeDenote A) := nil.
Definition mcons (A:denotedType) (a:(typeDenote A))
(l:list (typeDenote A))
: list (typeDenote A) := cons a l.
Arguments mnil {A}.
Arguments mcons {A} a l.
Compute mnil.
Compute mcons 2 mnil.
(*
= (2 :: nil)%list
: list denotedInt
*)
Compute mcons "h"%string mnil.
(*
The term ""h"%string" has type "string" while it is expected to have type
"typeDenote ?A".
*)
I need to read up about canonical structures.
Thanks!
Last updated: Oct 04 2023 at 23:01 UTC