Infinity Types

Inductive Base Library

Recursion and Dependence

  • N: Not a
  • R: Recursive
  • D: Dependent
  • +: Inductive
  • *: Coinductive

Inductive

Inductive types are the dependent version of generalized algebraic data types used in ML. With inductive and coinductive types you can model polynomial higher order functors that define generic trees and their constructors. Two very basic and known inductions are over natural numbers and lists, we show them the more detailed description.

Nat

Pointed Unary System is a category nat with the terminal object and a carrier nat having morphism [zero: 1nat → nat, succ: nat → nat]. The initial object of nat is called Natural Number Object and models Peano axiom set.

data nat: Type := (zero: () → nat) (succ: nat → nat)

List

The data type of list over a given set A can be represented as the initial algebra (μ LA, in) of the functor LA(X) = 1 + (A × X). Denote μ LA = List(A). The constructor functions nil: 1 → List(A) and cons: A × List(A) → List(A) are defined by nil = in ◦ inl and cons = in ◦ inr, so in = [nil,cons].

data list: (A: Type) → Type := (nil: () → list A) (cons: A → list A → list A) record lists (A,B: Type): Type := (len: list A → integer) ('++': list A → list A → list A) (map: (A → B) → (list A → list B)) (filter: (A → bool) → (list A → list A)))

Sum

sum is a meta-representation form of data inductive Inf syntax construction. For the internal form see Data AST construction.

data sum (A,B: Type): Type := (left: A → sum) (right: B → sum)

Empty

empty is a bottom type used as zero or terminal for sum inductive type. This type nas no constructors or with empty body.

data empty: Type := ()

Bool

bool is run-time version of the boolean logic you may use in your general purpose applications. It has only two unit constructors [true,false] and functions: [and,or].

data bool: Type := (true: () → bool) (false: () → bool)

Vector

vector is the inductive defintion of limited length list. Through it depends on term nat it can be used on reasoning about single discrete dimention of the space, bringing very basic inductive logic. It can be used for reasoning about sqrt, as latter for any fractional exponent has correspondent number of roots inscribed in a circle on a complex surface. When vector is not dependent on nat its encoding should match with regular list.

data vector (A: Type) (N: nat): Type := (nil: vector A nat.zero) (cons: A → vector A n → vector A (nat.succ n))

Coinductive

When you need to inspect the addendums of inductive tree defintions you can name the agruments of the constructor, these arguments called elements of the tuple or fields of the record. In this chapter we will use record Inf syntax, we only show how record and data are equal in example of unit and prod which are primitive forms of coinductive constructions.

Product

data prod (A,B: Type): Type := (cons: A → B → prod) record prod (A,B: Type): := (pr1: A) (pr2: B)

Unit

data unit: Type := (star: () → unit) record unit: Type := (star: ())

Stream

stream is a record form of the list's cons constructor. It models the infinity list that has no terminal element.

record stream (A: Type): Type := (head: A) (tail: stream A)

Pure

record pure (P: Type → Type) (A: Type): Type := (return: P A)

Functor

record functor (F: Type → Type) (A B: Type): Type := (fmap: (A → B) → F A → F B)

Functor carried with theorem fields.

record Functor (F: Type → Type): Type := (fmap: ∀ (A,B: Type) → (A → B) → F A → F B) (id: ∀ (A: Type) (x: F A) → Equ (fmap id x) x) (comp: ∀ (A,B,C: Type) (f: B → C) (g: A → B) (x: F A) → Equ (fmap (f ◦ g) x) ((fmap f ◦ fmap g) x))

Applicative

record applicative (F: Type → Type) (A,B: Type): Type extend pure F A, functor F A B := (ap: F (A → B) → F A → F B)

Monad

record monad: (F: Type → Type) → (A B: Type) → Type extend pure F A, functor F A B) := (join: F (F A) → F B)

Sigma

record sigma (A: Type) (B: A → Type): Type := (pr1: A) (pr2: B pr1)

I/O Monads

Recursive and Corecursive Monads.

IO

Finite I/O

data IO (A: Type): Type := (getLine: (String → IO) → IO) (putLine: String → IO → IO) (pure: A → IO)

Example:

(main: IO.replicateM 100 (IO.>>= IO.data () IO.getLine IO.putLine))

IOI

Infinity I/O

data IOI.F (A,State: Type): Type := (getLine: (String → State) → IO) (putLine: String → State → IO) (pure: A → IO) data IOI (A,State: Type) := (intro: State -> (State -> IOI.F A State) -> IOI)

Example:

record Main: Type := (main: λ (r: Type) -> IOI.MkIO r (Maybe IOI.data) (Maybe.Nothing IOI.data) ( λ (m: Maybe IOI.data) -> Maybe.maybe IOI.data m (IOI.F r (Maybe IOI.data)) ( λ (str: IOI.data) -> IOI.putLine r (Maybe IOI.data) str (Maybe.Nothing IOI.data)) (IOI.getLine r (Maybe IOI.data) (Maybe.Just IOI.data))))

Effects

Programming effect system with single Monad and Effect Handlers.

Effect

record effect (v:Type) (r:Type): Type := (values: v) (resource: r) (computation: (v → r)) (handler: effect v r → monad effect v r) data RA: Type := (intro: effect nat (random nat)) data IO (t:Type): Type := (intro: effect t (file t)) data EX (t:Type): Type := (intro: effect () (exception t))

Eff.Monad

data Eff.Monad (eff: list effect) (m: Type → Type) (a: Type): Type := (intro: eff m a xs (\ (v: Type) → xs) → monad_eff xs m a)

Eff.Handler

record Eff.Handler (e: effect) (m: Type → Type): Type := (action: ∀ (r: res) (eff: e t res resk) (k: ∀ (x: t) → resk x → m a) → m a)

Logic

Basic Theories: Equality, Congruence, Categories, Setoid.

True

data True: Prop := (intro: () → True)

False

data False: Prop := ()

Inhabited

data Inhabited (A: Type): Prop := (intro: A -> Inhabited A)

Proper

record Proper (A: Type) (R: A → A → Prop) (m: A): Prop := (Proof: R m m)

Respect / Congruence

define Respect (A,B: Type) (C: A → Type) (D: B → Type) (R: A → B → Prop) (Ro: ∀ (x: A) (y: B) → C x → D y → Prop) : (∀ (x: A) → C x) → (∀ (x: B) → D x) → Prop := λ (f,g: Type → Type) → (∀ (x,y: Type) → R x y) → Ro x y (f x) (g y)

Eq

record Id (A: Type): Type := (Id: A → A → Type) (refl (a: A): Id a a) (Predicate: ∀ (x,y: A) → Id x y → Type) (Forall (C: Predicate): ∀ (x,y: A) → ∀ (p: Id x y) → C x y p) (∆ (C: Predicate): ∀ (x: A) → C x x (refl x)) (axiom-J (C: Predicate): ∆ C → Forall C) (computation-rule (C: Predicate) (t: ∆ C): ∀ (x: A) → (J C t x x (refl x)) '==>' (t x) ) data Eq (A:Type): A → A → Prop := (refl: ∀ (x:A) → Eq A x x)

Exists

data Exists (A:Type) (P: A → Type): Prop := (intro: ∀ (x:A) → P x → exists P x)

Cat

record Cat: Type := (Ob: Type) (Hom: ∀ (dom,cod: Ob) → Setoid) (Id: ∀ (x: Ob) → Hom x x) (Comp: ∀ (x,y,z: Ob) → Hom x y → Hom y z → Hom x z) (Dom₁ₒ: ∀ (x,y: Ob) (f: Hom x y) → (Hom.Equ x y (Comp x x y id f) f)) (Cod₁ₒ: ∀ (x,y: Ob) (f: Hom x y) → (Hom.Equ x y (Comp x y y f id) f)) (Subst₁: ∀ (x,y,z: Ob) → Proper (Respect Equ (Respect Equ Equ)) (Comp x y z)) (Substₒ: ∀ (x,y,z: Ob) (f₁,f₂: Hom x y) (g₁,g₂: Hom y z) → (Hom.Equ x y f₁ f₂) → (Hom.Equ y z g₁ g₂) → (Hom.Equ x z (Comp x y z f₁ g₁) (Comp x y z f₂ g₂))) (Assocₒ: ∀ (x,y,z,w: Ob) (f: Hom x y) (g: Hom y z) (h: Hom z w) → (Hom.Equ x w (Comp x y w f (Comp y z w g h)) (Comp x z w (Comp x y z f g) h)))

Setoid

Setoid in essence is a type with an equality. Type theory has its own equality type, which could be treated as the simplest non-trivial dependent type, however the behavior of this kind of equality is defined with additional axioms, that may be optional in minimal type theory. The neat thing about Setoid is that categorical constructions on setoids give us equality on all (Co)inductive types, which is not dependent on properties of underlying type theory.

record Setoid: Type := (Carrier: Type) (Equ: Carrier → Carrier → Prop) (Refl: ∀ (x: Carrier) → Equ x x) (Trans: ∀ (x₁,x₂,x₃: Carrier) → Equ x₁ x₂ → Equ x₂ x₃ → Equ x₁ x₃) (Sym: ∀ (x₁,x₂: Carrier) → Equ x₁ x₂ → Equ x₂ x₁)

Groupoid

Groupoid is a multidimensional generalization of Setoid type, which has equalities on equalities and operations between them. Gropoid was introduced in algebraїс topology for the purposes of homotopy theory and has the potential to replace the notion of topological space since groupoid covers all the properties of topological space from the homotopy perspective. The ultimate equality on universum of all types was shown in HoTT setting, thus type theory became successful for reasoning about homotopies. Iterating a Groupoid record over infinity number of universes that hold objects and homomorphisms gives us a concept of ∞-Groupoid.

record Groupoid: Type := (ob: Type) (hom: ∀ (a,b: ob) → (Hom a b) → Groupoid)

Resources

  1. Om archives.
  2. Inf archives.
  3. Git sources.
  4. Inf git sources.