TH1: The Polymorphic Higher-order Form Syntax

Overview

• Extends TH0 with polymorphic features of TF1
• Five new polymorphic constants

Types and Type Signatures

• Types
  • The predefined types $i and $o
  • The arithmetic types $int for integers, $rat for rationals, $real for reals
  • User-defined n-ary type constructors applied to n type arguments
  • (τ₁ > ... > τ_n > τ^~) for n > 0

• Type Signatures
  • Individual types τ

New Polymorphic Constants

• !! for Π (universal quantification), ?? for Σ (existential quantification)
  (as polymorphic constants, rather than binders)
• @@+ for ι (indefinite description, aka choice), @@- for ε (definite description)
  (as polymorphic constants, rather than binders)
• @= for equality (as a polymorphic constant, rather than a connective)

Notes

• Connectives can be used as terms
• Application can be partial
• Use of functions and predicates must respect the type signature
• Polymorphic symbols must have some type arguments and term arguments

TH1 Example