Soft Type System

In type theory, when we write the type judgement \(\Gamma\vdash t:T\), this is a proposition in the metalanguage. But in ordinary mathematics, we often muddle metavariables and object variables (more generally, we muddle metalanguage constructs with object language constructs). We can approximate this muddling by building in the object language a typing judgement and a type system. This type system is called a Soft Type System.

More specifically, instead of writing something like G : Group, we have a unary predicate isGroup[-] and treat the judgement as isGroup[G].

Subtyping

for all x, isSubtype[x] implies isSupertype[x].

Dependent Types

A dependent type with \(n\) parameters is encoded as an \((n+1)\) -ary predicate.

• Freek Wiedijk,
  "Mizar's Soft Type System".
  In International Conference on Theorem Proving in Higher Order Logics (pp. 383-399). Springer, Berlin, Heidelberg. Eprint, 17 pages.
  • Wiedijk invented the notion of soft type systems to describe Mizar's typing system.
• Cezary Kaliszyk, Florian Rabe,
  "A Survey of Languages for Formalizing Mathematics". A CICM2020 paper, arXiv:2005.12876, 19 pages
  • This paper seems to invent the notion of a "semi-soft type system" and a "hard type system"
• Florian Rabe,
  "A Language with Type-Dependent Equality".
  Eprint, 16 pages
  • Notes how soft-type systems makes typing and equality both undecidable.