TF1: The Polymorphic Typed First-order Form

Overview

• Extends TF0 with type constructors, type variables, and polymorphic symbols
• One new binder is added

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
  • Type variables, which must be quantified by !>
• About type constructors
  • Declared to be of the kind ($tType * ... * $tType) > $tType
  • If arity is 0 then they are type constants

• Type Signatures
  • Individual types τ
  • (τ₁ * ... * τ_n) > τ^~ for n > 0
  • !>[α₁: $tType, ... α_n: $tType] : σ for n > 0
    where α₁ ... α_n are distinct type variables and σ is a type signature

Notes

• Use of functions and predicates must respect the type signature
• Polymorphic symbols must have all type arguments and term arguments

TF1 Example