# Recursion and Dependence

1. BOOL
2. TRUE
3. FALSE
4. OPTION
5. UNIT

1. NAT
2. LIST
3. IO
4. IOI

1. EQ
2. EXISTS

1. VECTOR

1. PROD
2. PURE
3. FUNCTOR
4. APPLICATIVE

1. STREAM
2. PROCESS
3. EFFECT
5. EFF.HANDLER

1. SIGMA
2. SETOID
3. PROPER
4. RESPECT

### RD *

1. CAT
2. GROUPOID
• 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) ```

```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) ```

## 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)) ```

```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) ```