Álgebra de Tipos

Daniel Yokomizo / @dyokomizo

Álgebra

a = (b × c) + d
					

• Símbolos: a, b, c, d
• Operações: ×, +
• Propriedades: comutatividade, associatividade
• Estruturas: Monóides, Grupos, Anéis

Tipos

data Either a b = Left  a
                | Right b

data Pair a b   = Pair (a, b)
					

• Variáveis: a, b
• Construtores: Left, Right, Pair

Álgebra de Tipos

Faz sentido? Sim.

Como?

• Definição de álgebra: estudo de estruturas algébricas
• Estruturas algébricas: conjunto com uma ou mais operações e propriedades

Álgebra de Tipos

• Conjunto: tipos possíveis
• Operações: +, ×
• Propriedades: ??
• Estruturas: ??

Álgebra de Tipos — Primitivos

• 1: tipo com um único habitante

  data () = () -- aka Unit

• 0: tipo com nenhum habitante

  data Void -- requer EmptyDataDecls

Álgebra de Tipos — Operações

• +: União

  |

• ×: Tupla

  (,)

• ^: Função

  →

Álgebra de Tipos — Operações

+

data Either a b = Left  a
                | Right b
					

c = a + b
					

Álgebra de Tipos — Operações

×

data Pair a b   = Pair (a, b)
					

c = a × b
					

Álgebra de Tipos — Operações

^

data Fun a b   = Fun (a → b)
					

c = ba

Álgebra de Tipos — Exemplos

data Maybe a = Just a
             | Nothing -- () impĺícito
					

c = a + 1
						

Álgebra de Tipos — Exemplos

data Bool = True
          | False
					

a = 1 + 1
						

Álgebra de Tipos — Propriedades

Elemento neutro

a ≅ (a × 1) ≅ (1 × a)
					

String ≅ (String, ()) ≅ ((), String)
					

a ≅ (a + 0) ≅ (0 + a)
					

String ≅ (Either String Void) ≅ (Either Void String)
					

Álgebra de Tipos — Propriedades

Associatividade

a × (b × c) ≅ (a × b) × c
					

(String,(Int,Bool)) ≅ ((String,Int),Bool)
					

a + (b + c) ≅ (a + b) + c
					

Either String (Either Int Bool) ≅ Either (Either String Int) Bool
					

Álgebra de Tipos — Propriedades

Elemento neutro

a ≅ (a × 1) ≅ (1 × a)
					

a ≅ (a + 0) ≅ (0 + a)
					

Associatividade

a × (b × c) ≅ (a × b) × c
					

a + (b + c) ≅ (a + b) + c
					

Álgebra de Tipos — Estruturas

Monóide

• Definição: conjunto com uma operação associativa e com elemento neutro
• × com 1
• + com 0

Álgebra de Tipos — Propriedades

Distributividade

a × (b + c) ≅ (a × b) + (a × c)
					

(String, Either Int Bool) ≅ Either (String, Int) (String, Bool)
					

Álgebra de Tipos — Exemplos

data A a b = A1 a b
           | A2 b
					

type A a b = Either (a, b) b
					

c = (a × b) + b
  ≅ (a × b) + (1 × b) -- Elemento neutro
  ≅ (a + 1) × b       -- Distributividade
					

type A a b = (Maybe a, b)
					

Álgebra de Tipos — Funções

a → b   ≍   ba

Bool → Int   ≍   IntBool

Álgebra de Tipos — Funções

Bool → a   ≍   aBool

Bool   ≍   1 + 1
					

aBool≅ a‌1 + 1        ≅ a‌1× a‌1
        ≅ a × a
					

Bool → a   ≅   (a,a)
					

Álgebra de Tipos — Funções

meaningOfLife :: Boolean -> Int
meaningOfLife True  = 42
meaningOfLife False = 37

Bool -> a ≅ (a, a)

meaningOfLife' :: (Int, Int)
meaningOfLife = (42,37)
					

Referências

• The Algebra of Data, and the Calculus of Mutation
• Abusing the algebra of algebraic data types — why does this work?
• The Derivative of a Regular Type is its Type of One-Hole Contexts
• Differentiating Types in Haskell
• Differentiating Datastructures — The Algebra of Datatypes (for Non-Functional Programmers)
• Theseus and the Zipper
• The Algebra of Algebraic Data Types
• github.com/dyokomizo/type-algebra-slides