Specifying polarity in a module type

3
votes

The following inductive definition of U is accepted by Coq because it can see that the occurrences of U in M.T U -> U are strictly positive.

Module M.

Definition T (A : Type) : Type := unit -> A.

End M.

Module N.

Inductive U : Type :=
| c : M.T U -> U.

End N.

On the other hand, the following inductive definition of U is not accepted by Coq because, depending on the definition of M.T, it might have non-strictly positive occurrences.

Module Type S.

Parameter T : Type -> Type.

End S.

Module N (M : S).

Fail Inductive U : Type :=
| c : M.T U -> U.

End N.

How can I specify in the signature S that the parameter of T should only have strictly negative occurrences? Thus preventing any non-strictly positive occurrences of U in its definition.

1
coq

1 Answers

0
votes

This U type can be seen as the least fixed point of M.T. Another common encoding is

Definition Mu (T : Type -> Type) := forall A, (T A -> A) -> A.
Definition U := Mu M.T.

Provided that T is a functor (which strict positivity would imply, maybe?):

Parameter map : forall A B, (A -> B) -> T A -> T B. (* in module M *)

we have a constructor and destructor:

Definition c : M.T U -> U := fun x A f =>
   f (M.map _ _ (fun y => y _ f) x).

Definition d : U -> M.T U := fun y => y _ (fun x => M.map _ _ c x).

Showing they are inverses requires parametricity, so there is no direct way to prove it. If you don't want to axiomatize it, you can probably enrich T and U to carry evidence of parametricity.

Essentially, the requirement above that T be a functor is a semantic replacement/approximation of the strict positivity condition, which is syntactic.

It is also possible to switch off positivity checking with this new plugin:

https://github.com/SimonBoulier/TypingFlags