Questions tagged [type-rule]
In type theory, a type rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well typed and what type expressions have. (from Wikipedia)
4
questions
10
votes
0
answers
177
views
Is there a proof assistant (or an embedding) for the (co)end calculus?
A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
- 3,490
9
votes
2
answers
251
views
What's the benefit of having pi and sigma types with an invariant parameter?
Ulf Norell wrote this in his PhD thesis (figure 1.6):
This contradicts my stereotype on pi & sigma types, where pi parameter should be contravariant and sigma parameter is covariant. Why is Agda ...
- 5,494
14
votes
2
answers
238
views
Tools for checking the consistency of a type theory
My question is twofold:
How do you define consistency (analogously to the concept in first-order logic) in the context of a type theory?
Are there any tools that can check consistency?
I have seen a ...
- 2,681
18
votes
2
answers
340
views
What is the difference between judgmental equality, definitional equality, and equality types?
This answer to this question about η-equivalence in Coq draws a distinction between judgmental equality and definitional equality.
In the simply typed lambda calculus (henceforth STLC), the following ...
- 2,681