Introduction

In the post on the calculus of constructions, we implemented several Sorts (SProp, Prop, Set, Type). A Sort can be thought of as a “type of types.” For example, booleans and the natural numbers are types that live in Set.

In order to maintain consistency, we need to implement a Sort Hierarchy. This is roughly necessary due to possible contradictions that can arise due to self-reference (similar to Russell’s paradox).

This post describes a minimal sort hierarchy, based on Coq’s, and modifications to some of our earlier product formation rules. I don’t implement all of the rules (to keep the implementation simple), but if I discover I need them later, I will modify this post later.

This post is a sequel to several earlier posts about proofs and reasoning. I recommend reading those posts first.

Simplified Sort Levels

Here’s our simple type hierarchy:

def sort_level(sort: Sort) -> int:
    match sort:
        case SProp(): return 0
        case Prop(): return 1
        case Set(): return 2
        case Type(n): return 3 + n

def is_subsort(s1: Sort, s2: Sort) -> bool:
    if isinstance(s1, Type) and isinstance(s2, Type):
        return s1.n <= s2.n
    return sort_level(s1) <= sort_level(s2)

Basically, we assign a numerical level to each sort, then retrieve and compare the levels.

We will need to alter our product rules to include some special cases. The key idea is that we look at the sorts of the two inputs, then decide what the output sort should be. Usually, we take the maximum of the input sorts to produce the output sort. However, there can be special cases: for instance, if the second input is in Prop, then we should be able to construct that proposition by quantifying over terms in any sort like Set or Type (this is called small elimination). Similarly, if the second input is in Prop, then the result is in Prop (this is called impredicativity).

Let’s focus on small elimination. Why do we need this? The idea behind small elimination is that we want to be able to construct propositions (types in Prop) by quantifying over types in any sort. For example, given a type \(A\) in Set, we should be able to construct a proposition \(P(a)\) that depends on \(a:A\). The resulting type \(\forall(a:A).P(a)\) should be in Prop.

That being said, we need to restrict elimination in the opposite direction. We can’t construct computational types (Set or Type) by pattern matching on proofs in Prop. This restriction, preventing “large eliminations” from Prop, helps maintain “proof irrelevance”. That is: it shouldn’t matter how a term or type was constructed, only that we did construct it.

def sort_product_type(s1: Sort, s2: Sort) -> Sort:
    # No large eliminations from Prop
    if isinstance(s1, Prop):
        if not isinstance(s2, Prop):
            raise TypeError()
        return Prop()
        
    # Prop impredicativity 
    if isinstance(s2, Prop):
        return Prop()
        
    # Regular cases use max
    if isinstance(s1, Type) and isinstance(s2, Type):
        return Type(max(s1.n, s2.n))
    return s2 if sort_level(s2) > sort_level(s1) else s1

The above code implements the required logic.

Updated Product Rules

Here’s our original product formation rules:

def prod_set(environment: Environment, x: Variable, hyp_sort_type: Hypothesis, hyp_set_type: Hypothesis) -> Hypothesis:
    T1 = hyp_set_type.localContext.body()[x.name]
    assert terms_equal(environment, hyp_sort_type.term_, T1) 
    
    term_is_sprop = terms_equal(environment, hyp_sort_type.type_, SProp())
    term_is_prop = terms_equal(environment, hyp_sort_type.type_, Prop())
    term_is_set = terms_equal(environment, hyp_sort_type.type_, Set())
    assert term_is_set or term_is_prop or term_is_sprop 

    assert terms_equal(environment, hyp_set_type.type_, Set())

    assert x.name in hyp_set_type.localContext.body() 
    assert x.name not in hyp_sort_type.localContext.body()

    T2 = hyp_sort_type.term_
    assert terms_equal(environment, T1, T2)
    product = ProductType(x, T1, hyp_set_type.term_)

    return Hypothesis(environment, product, Set())

def prod_type(environment: Environment, x: Variable, hyp_sort_type: Hypothesis, hyp_type_type: Hypothesis) -> Hypothesis:
    T1 = hyp_type_type.localContext.body()[x.name]
    assert terms_equal(environment, hyp_sort_type.term_, T1)
    
    equals_sprop = terms_equal(environment, hyp_sort_type.type_, SProp())
    equals_type_i = terms_equal(environment, hyp_sort_type.type_, Type(hyp_type_type.type_.n))
    assert equals_sprop or equals_type_i

    assert terms_equal(environment, hyp_type_type.type_, Type(hyp_type_type.type_.n))

    assert x.name in hyp_type_type.localContext.body() 
    assert x.name not in hyp_sort_type.localContext.body()

    T2 = hyp_sort_type.term_
    assert terms_equal(environment, T1, T2)

    product = ProductType(x, T1, hyp_type_type.term_)
    return Hypothesis(environment, product, Type(hyp_type_type.type_.n))

Now let’s adjust these with our new sort_product_type function.

def prod_set(environment: Environment, x: Variable, hyp_sort_type: Hypothesis, hyp_set_type: Hypothesis) -> Hypothesis:
   T1 = hyp_set_type.localContext.body()[x.name]
   assert terms_equal(environment, hyp_sort_type.term_, T1) 
   
   s1 = hyp_sort_type.type_
   s2 = hyp_set_type.type_
   
   term_is_sprop = terms_equal(environment, s1, SProp())
   term_is_prop = terms_equal(environment, s1, Prop()) 
   term_is_set = terms_equal(environment, s1, Set())
   assert term_is_set or term_is_prop or term_is_sprop

   assert terms_equal(environment, s2, Set())

   assert x.name in hyp_set_type.localContext.body() 
   assert x.name not in hyp_sort_type.localContext.body()

   T2 = hyp_sort_type.term_
   assert terms_equal(environment, T1, T2)
   product = ProductType(x, T1, hyp_set_type.term_)

   result_sort = sort_product_type(s1, s2)
   return Hypothesis(environment, product, result_sort)

def prod_type(environment: Environment, x: Variable, hyp_sort_type: Hypothesis, hyp_type_type: Hypothesis) -> Hypothesis:
   T1 = hyp_type_type.localContext.body()[x.name]
   assert terms_equal(environment, hyp_sort_type.term_, T1)
   
   s1 = hyp_sort_type.type_
   s2 = hyp_type_type.type_

   equals_sprop = terms_equal(environment, s1, SProp())
   equals_type_i = terms_equal(environment, s1, Type(hyp_type_type.type_.n))
   assert equals_sprop or equals_type_i

   assert terms_equal(environment, s2, Type(hyp_type_type.type_.n))

   assert x.name in hyp_type_type.localContext.body() 
   assert x.name not in hyp_sort_type.localContext.body()

   T2 = hyp_sort_type.term_
   assert terms_equal(environment, T1, T2)

   product = ProductType(x, T1, hyp_type_type.term_)
   result_sort = sort_product_type(s1, s2)
   return Hypothesis(environment, product, result_sort)

We will need this rule for certain inductive proofs.

Next Steps

There are other special rules for various Sorts. As mentioned, we will implement them as we need them.

This is an interstitial post required for later posts, outside of our game plan. In the next posts we will either keep updating our type system, or continue implementing induction.