2
$\begingroup$

In Coq, is it possible to write a predicate (list Type -> Prop) that is only provable if all entries of the list are of the form Type@{U}?

The predicate should accept Types from different universes within the same list. For example, [Type@{U1}; Type@{U2}] should be accepted, where U1 < U2. Other types, such as nat, should not be accepted in the list.

The closest I was able to get is to have the predicate verify that each entry of the list is a universe-like type that has some of the properties of Type@{U}:

  • The universe-like types form a chain, where the previous one is embedded within the next.
  • Set is at the start of the chain.
  • Each universe-like type has an export function that can convert an inhabitant of the universe-like type, T: UT, into an inhabitant of T@{max}. That is, export: UT -> Type@{max}.

However, that predicate also accepts types which are not of the form Type%{U}, such as (Type * nat)%type.

Require Import List.

Import ListNotations.

Inductive TypeChain: forall (carrier: Type), (carrier -> Type) -> Type :=
| TypeChainSet: TypeChain Set (fun s: Set => s)
| TypeChainNext:
  forall prev_carrier prev_export,
  TypeChain prev_carrier prev_export ->
  forall carrier (export: carrier -> Type) (import: prev_carrier -> carrier),
  (forall p: prev_carrier, export (import p) = prev_export p) ->
  forall prev_embed,
  (export (prev_embed) = prev_carrier) ->
  TypeChain carrier export.

Inductive InTypeChain (T: Type):
    forall {carrier export}, TypeChain carrier export -> Prop :=
| InTypeChainTop: forall export (chain: TypeChain T export),
  InTypeChain T chain
| InTypeChainPrev:
  forall prev_carrier prev_export prev_chain,
  InTypeChain T prev_chain ->
  forall carrier export import export_imported prev_embed prev_embed_matches,
  InTypeChain T (TypeChainNext prev_carrier prev_export prev_chain carrier
                 export import export_imported prev_embed prev_embed_matches).

Definition ListContainsOnlyTypes (l: list Type) :=
exists carrier export (c: TypeChain carrier export),
  Forall (fun T => InTypeChain T c) l.
Module GoodExample.

Universe U1 U2.
Constraint U1 < U2.

Definition ChainU2: TypeChain Type@{U2} (fun T => T).
Proof.
  unshelve eapply (TypeChainNext Type@{U1}); auto.
  unshelve eapply (TypeChainNext Type@{Set}); auto.
  unshelve apply TypeChainSet.
Defined.

Example GoodListAccepted: ListContainsOnlyTypes [Type@{U1}; Set; Type@{U2}].
Proof.
  eexists.
  eexists.
  exists ChainU2.
  eauto 7 using InTypeChain.
Qed.

End GoodExample.
Module BadExample.

Definition BadChain: TypeChain (Type * nat) (fun T => fst T).
Proof.
  unshelve eapply (TypeChainNext Set); auto.
  - exact (fun s:Set => (s:Type, 0)).
  - exact (Set, 0).
  - apply TypeChainSet.
  - reflexivity.
  - reflexivity.
Defined.

Example BadListAccepted: ListContainsOnlyTypes [(Type * nat)%type; Set].
Proof.
  eexists.
  eexists.
  exists BadChain.
  eauto using InTypeChain.
Qed.

End BadExample.
$\endgroup$
9
  • $\begingroup$ Can you prove that nat is not equal to nat * nat in Coq? $\endgroup$
    – Trebor
    May 25 at 2:42
  • $\begingroup$ I'm not an expert on these things, but I think you can only prove that two types are not equal in Coq if their cardinality is different. nat and nat * nat are both countably infinite types. So without adding axioms, you can't prove that they are equal or not equal. $\endgroup$ May 25 at 3:04
  • $\begingroup$ Since you can't disprove that, if you add nat = (nat*nat) as an axiom there will be no inconsistency. Similarly adding the axiom about universes Type = Type*nat does not result in inconsistencies. $\endgroup$
    – Trebor
    May 25 at 3:19
  • $\begingroup$ Now if you add that axiom, you can now rewrite using that. So you can never distinguish these two things with any definition whatsoever. Due to its consistency, even without that axiom you can't disprove the possibility. $\endgroup$
    – Trebor
    May 25 at 3:20
  • 1
    $\begingroup$ @KyleStemen: here's a proof that (Set -> bool) = Set -> False, so your claim above is incorrect. $\endgroup$ May 25 at 22:10

1 Answer 1

1
$\begingroup$

As pointed out in the comments, universes are very underspecified in CIC, so that the kind of things you want to do is not easily feasible.

If you want to do "intensional" analysis of types, a good solution is often to consider codes rather than types. Here is a very naïve example:

Require Import List.
Import ListNotations.

Inductive code : Type :=
  | ty : code
  | ar : code -> code -> code
  | n : code.

Fixpoint El (c : code) : Type :=
  match c with
  | ty => Type
  | ar c1 c2 => El c1 -> El c2
  | n => nat
  end.

Inductive CodeChain : list code -> Prop :=
  | cnil : CodeChain []
  | ccons l : CodeChain l -> CodeChain (ty :: l).

Definition TypeChain (l : list Type) : Prop :=
  exists l', l = map El l' /\ CodeChain l'.

There are multiple difficulties here, however.

First, while CodeChain encodes the predicate you are looking for, TypeChain is somewhat too lose again, because eg we cannot derive falsity from TypeChain [nat*Type], while we can derive it from eg CodeChain [n]. Basically, applying El loses the intensional content you are looking for. So you should as much as possible reason on the codes rather than the types.

Second, because Coq cannot reason about universe levels is a first class way, you cannot specify in your codes that the ty constructor should be at a given level.

Third, and maybe the biggest limitation, this inductive presentation of codes does not scale to dependent types. Indeed, in such a setting you would want to write a constructor for dependent function type as ar : forall A : code, (El A -> code) -> code, but this means El and code need to be defined mutually. This is called an inductive-recursive definition, and is not available in Coq (but it is in Agda for instance).

$\endgroup$
9
  • $\begingroup$ Does this solve the dependent types problem with codes in Coq? Inductive codeable : Type -> Type := | ty : codeable Type | ar : forall input, codeable input -> forall (output: input -> Type), (forall i, codeable (output i)) -> codeable (forall i, output i) | n : codeable nat. Record code := { El: Type; witness: codeable El; }. $\endgroup$ May 26 at 7:29
  • $\begingroup$ Your TypeChain predicate basically says that all of the types in the list can be expressed as codes instead. It allows types like nat -> nat, because they can be expressed as codes. However in my example, ListContainsOnlyTypes rejects nat -> nat, because it is too different from Type. I think the point you are trying to make is that I should avoid using Type in the rest of my program and use codes instead. In this case, the second difficulty you listed (cannot reason about universe levels) is a bigger deal. That limits the kinds of higher order functions that are accepted. $\endgroup$ May 26 at 7:39
  • $\begingroup$ As to your first comment: indeed, yes, this is a way to go around the issue, by replacing induction-recursion with indices. Basically, you replace the El function by a predicate describing its graph. You lose computation, but you gain the ability to define it in Coq. $\endgroup$ May 26 at 8:58
  • $\begingroup$ As for the second comment, this is not the case: the CodeChain predicate says that all elements in the list are ty, the code for Type. So applying map El to such a list must result in a list where all elements are Type. The issue being that l = map El l' hits the issue of equality between types again. $\endgroup$ May 26 at 9:08
  • $\begingroup$ I am not sure what you mean by "limiting the kinds of higher order functions that are accepted", though? $\endgroup$ May 26 at 9:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.