Type

see type system, type inference, type-driven design

--- https://youtu.be/6hAeJmKXRfo

Top Type

--- https://en.wikipedia.org/wiki/Top_type

definition the top type is the type that is a super‹type of all other types

example Object is javascript's and java's top ‹type and interface{} is go's top ‹type

Bottom Type

definition the bottom type is the type that is a sub‹type of all other types

example ! is rust's bottom ‹type

Empty Type

--- https://en.wikipedia.org/wiki/Empty_type

equiv empty ‹set

definition an empty type is a type with no terms

all empty ‹types are isomorphic, and thus it is common to refer to one as the empty ‹type

the empty ‹type can be thought of as the sum ‹type of no types

example enum {} and ! are rust's empty ‹types

Unit Type

--- https://en.wikipedia.org/wiki/Unit_type

equiv singleton ‹set

definition a unit type is a type with exactly one term

all unit ‹types are isomorphic, and thus it is common to refer to one as the unit ‹type

the unit ‹type can be thought of as the product ‹type of no types

example () is rust's and Haskell's unit ‹type and void is c's unit ‹type

Subtype

Supertype

equiv sub‹set

equiv super‹set

definition a type A is a sub‹type of a type B if all terms of A are also terms of B

definition a type A is a super‹type of a type B if all terms of B are also terms of A

properties

the subtype relation is a partial order --- https://youtu.be/hy1wjkcIBCU?t=1926

Refinement Type

--- https://en.wikipedia.org/wiki/Refinement_type

definition a refinement type is a type equipped with a predicate that is assumed to hold for all terms of the refinement type

example

use non_zero_u8::*; //*
mod non_zero_u8 {
  pub struct NonZeroU8(u8);
  impl NonZeroU8 {
    pub fn new(n: u8) -> Option<Self> { (n != 0).then_some(Self(n)) }
    pub fn get(&self) -> u8 { self.0 }
  }
}

--- https://youtu.be/KWB-gDVuy_I?t=375

refinement types may be used to assert pre- and post-conditions at the type system level

Algebraic Data Type

algebraic data ‹types are one tool for making illegal states unrepresentable --- Yaron Minsky --- https://youtu.be/2JB1_e5wZmU?t=46m16s in type-driven design

Sum Type

aka "or" type, "choice" type, Rust enum

properties

the set› cardinality of a sum ‹type is the sum of the set› cardinalityes of its constituent types: \(|A + B| = |A| + |B|\)

Product Type

aka "and" type, pair, struct

properties

the set› cardinality of a product ‹type is the product of the set› cardinalityes of its constituent types: \(|A \times B| = |A| \cdot |B|\)

Exponential Type

aka function type

--- https://youtu.be/6hAeJmKXRfo?t=322

the set› cardinality of a exponential ‹type is the set› cardinality of its function › codomain to the power of the set› cardinality of its function › domain: \(|A \to B| = |B|^{|A|}\) aka \(|B^A| = |B|^{|A|}\)

note intuitively, to each of the \(|A|\) possible inputs we associate one of \(|B|\) possible outputs