Пустой тип

• Определение и использование пустого типа

  • Пустой тип (0) — это тип без терминов. 
  • Может быть определен как нулевой побочный продукт или полиморфный тип. 
  • Для любого типа P тип ¬P определяется как P → 0. 

• Соответствие Карри-Говарда

  • Термин типа 0 соответствует ложному утверждению. 
  • Термин типа ¬P соответствует опровержению утверждения P. 

• Необязательность пустого типа

  • Теория типов может не содержать пустой тип. 
  • Если пустой тип присутствует, он обычно не уникален. 

• Взаимосвязь с нижним типом

  • Если система типов содержит пустой тип, нижний тип также должен быть необитаем. 
  • Оба типа (0 и нижний тип) могут обозначаться как ⊥. 

• Призыв к действию

  • Статья является теоретической и требует расширения для Википедии.