¿Por qué tipos de dato algebraicos?


Sum Type y búsqueda de patrones sobre ellos
Product Type y búsqueda de patrones
Exponential type

Pero...

¿Por qué son algebraicos?

¡Hay que dar una poquita vuelta a Matemática!

Cada ADT lleva su operador para realizar su álegebra


a | b = |a| + |b|


(a, b) = |a| * |b|


a -> b = |b| ^ |a|

Parte Uno

Los tipos y sus cardinalidades

						
							|Void|  = 0
							|()|    = 1
							|Bool|  = 2
							-- De aquí ya podemos realizar lo que siguiente
							type Product = |(Bool, Bool)|     = ???
							type Sum = |Either Bool Bool| = ???
							type Exponential = |(Bool -> Bool)|   = ???


La correspondencia unívoca tipos A y B con las mismas cardinalidades son isomorfismos TODO absurd :: Ex falso sequitur quodlibet

Parte Dos - dada la demostración

Isomorfismo entre entre Matemática y Tipos

							
							(a * b)^c = a^c * b^c
							a * ( b + c ) = a * b + a * c 
							-- not that easy
							(a^b)^c = a ^ (b * c)
							-- TODO show maxBound
							-- TODO show Data.Void
							-- curry/uncurry

La forma canónica de ADT

t = ∑ ∏ t m, n m n 
							
							-- canónicas ::

							Either a b
							
							a -> b 
							
							Either a (Either b, (c,d)) 
							
							-- no canónicas ::
							
							(a, Either b c)
							
							(a, Bool)

Las variantes del Tipos

“ A Profunctor is a Contravariant Functor on its first type parameter and a Functor on its second type parameter. ”

data Variance = Covariant | Contravariant | Invariant import Data.Functor
A Variance of type T a is fully specified by positive, negative (or mix of both) type variable position. 
						
							newtype F1 a = F1 ( Int -> a ) -- + => + Covariant
							newtype F2 a = F2 ( a -> a ) --  +/- => +/- Invariant
							newtype F3 a = F3 ((Int -> a) -> Int ) -- Contravariant - * + => - 
							newtype F4 a = F4 ((a -> Int) -> Int ) -- Covariant - * - => +

Scala -> (Haskell, Idris, Perl 6)

=> Pattern Matching - power of the types

=> Type classes vs. Interfaces

=> Kinds - as a labels for the types

=> GADTs - Generalized ADT

=> Partial Type Application/Type Level Programming

=> A better Scala REPL ammonite.io

=> Typelevel CATS library

=> Scalaz Scalaz-ZIO

¿Why?

Becasue writing like this we programming by giving proof.


¡Think about it!

¡¡EXTRA!! GADTs

								
									role Maybe[::A] { }
									sub just(::A $x --> Maybe[::A]) { class Just does Maybe[::A] { has $.V = $x; }.new }
									sub nothing(Any:U $t --> Maybe[$t]) { class Nothing does Maybe[$t] { }.new }
								
						
								 
								data MyMaybe a where
									MyJust    :: a -> MyMaybe a
									MyNothing :: MyMaybe a

¡Muchas Gracias!

Thanks!