If we remove subtyping (https://coq.inria.fr/distrib/current/refman/language/cic.html#subtyping-rules) from CIC we will lose some expressive power. But is that power necessary for a programming language?

If we demand programmer to write e.g. Type(1) and Type(2) to mean respectively type and kind, that won't be anything novel in software engineering.

Can we get something in exchange? For example relaxed requirement on strict positivity of inductive types (without creating inconsistency in the language)?

We should get at least simpler term equivalence check where problem of η-reduction (https://coq.inria.fr/distrib/current/refman/language/cic.html#expansion) doesn't exist.

Is there some research on this topic? How does it compare to e.g. inductive types from NuPrl (https://ecommons.cornell.edu/handle/1813/6710)?


Your Answer

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

Browse other questions tagged or ask your own question.