ADTS

WellTyped :: (Scala, Haskell)



Dawid Furman

Motivation

The common mistake is to choose too powerfull type.

Effect => Such a type can represent anything

Consequences => Tends to corrupt, illegal state, wrong buisness model representation, "strange" runtime errors, lost time, ...

Action point => ???

Algebraic data types to the rescue

In computer programming, more so functional programming and type theory, an algebraic data type is a kind of composite type, i.e., a type formed by combining other types.

Source Wikipedia

ADT :: Sum Type -> "is a relationship - logical or"
a Day is Mo | Tu | We | Th | Fr | Sa | Su
ADT :: Product Type -> "has a relationship - logical and"
a Pair has a value a and b
ADT :: Exponential type -> "it`s a transformation"

But...

algebraic - what stands for?

¡Let`s return to Math for a while!

Each ADT has his operator for the algebra realization


a | b = |a| + |b|


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


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

Part I

Types and their cardinalities

						
							|Void|  = 0
							|()|    = 1
							|Bool|  = 2
							-- Let`s check the cardinalities for ::
							type Product = |(Bool, Bool)|     = ???
							type Sum = |Either Bool Bool| = ???
							type Exponential = |(Bool -> Bool)|   = ???
Two different types A and B with the same cardinalities are isomorphisms between each other.

and suddenly ...

We are able to express mathematical theorems in terms of types! 

						
							(a * b)^c = a^c * b^c
							a * ( b + c ) = a * b + a * c 
							-- not that easy
							(a^b)^c = a ^ (b * c)

TODO ::
1. prove that
a * 1 = a | a ^ 1 = a
by Curry-Howard
2. import Data.Void - discussion about absurd

The canonical form of ADT

aType = ∑ ∏ aType m, n

So the canonical form is represent as a
Sum of products 

						
						-- correct canonical from ::
						
						Either a b
						a -> b 
						Either a (Either b, (c,d)) 
						
						-- not correct ::
						
						(a, Either b c)
						(a, Bool)

Part II

Types variants

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

Source TypeLevel::Cats API

data Variance = Covariant | Contravariant | Invariant

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, PureScript)

=> 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 proofs.


¡Think about it!

Takeaways I

  • ADTs are simple yet powerful.
  • So go for it! Model your data as ADTs...
  • ...and be dumb! Think in is-a and has-a relationships.

Takeaways II




STOP String data modeling


Well type data ~ More free time for all!




No State -> No Classes

¡Muchas Gracias!

Find us

					
						sealed trait SocialMedia
						case object Telegram extends SocialMedia
						case object Meetup   extends SocialMedia 
						case object Twitter  extends SocialMedia 
						aMalagaScalaSocial match {
						case Twitter  => https://twitter.com/MalagaScala 
						case Telegram => https://t.me/malaga_scala
						case Meetup   => https://meetup.com/Malaga-Scala
						case _ 		=> ???
						}