### (Algebra)ic Data type - Một số khái niệm - Algebra trong ADT - Example - The Curry–Howard Isomorphism - Kết luận - Resource --- ### Khái niệm - Cardinality - Isomorphism --- ### Cardinality - *Cardinality* (size): số lượng phần tử của một tập hợp - Programming context: số lượng phần tử của kiểu (Type) không tính phần tử bottom. - `|A|` là cardinality(size) của type A ---- ### Cardinality  ---- ### Cardinality - `Nothing`: có 0 phần tử => `|Nothing| = 0` - `Unit`: có duy nhất 1 phần tử `()` => `|Unit| = 1` - `Boolean`: `True` và `False` => `|Boolean| = 2` - `Byte`: 8 bit => `|Byte|` = `256` --- ### Isomorphism - morph: to change - thay đổi - ism: system/theory - hệ thống, học thuyết - morphism: thing that changes something - sự thay đổi - iso: equal, similar, identical; isometric - tương đương - Isomorphism: sự biến đổi tương đương ---- ### Morphism Trong programming context - pure function - transformation from one type to another type. - morphism từ A sang B chính là một function từ type A sang type B, A với B có thể là một. ---- ### Isomorphism Type A và type B là isomophism (`A <=> B`) khi tồn tại 2 functions: - `from: A => B` - `to: B => A` thoả mãn: - ∀ a: A, `to(from(a)) == a` - ∀ b: B, `from(to(b)) == b` Cặp function (to, from) sẽ được gọi là một isomorphism của A và B ---- ### Isomorphism - `to.from = id` và `from.to = id` - trong đó `id` là identity function được định nghĩa: `id(a) = a` ``` val f: A => B val g: B => C f.g: A => C f.g(a) = f(g(a)) ``` --- ### Isomorphism và Cardinality Với 2 type bất kỳ, 2 type đó có cùng size khi vào chỉ khi có isomophism giữa 2 type đó `A <=> B` khi và chỉ khi `|A| = |B|` ---- ### Isomorphism và Cardinality example ```scala enum Direction: case Up case Down ``` Ta có cardinality: `|Direction| = |Boolean| = 2` và isomorphism: ``` val to = (d: Direction) => d match case Up => True case Down => False val from = (d: Boolean) => d match case True => Up case False => Down ``` ---- ### Isomorphism và Cardinality example ``` val to2 = (d: Direction) => d match case Up => False case Down => True val from2 = (d: Boolean) => d match case True => Down case False => Up ``` ---- ### Isomorphism và Cardinality Question ---- ### Isomorphism và Cardinality Khi A <=> B thì ta có thể đổi chỗ A, B cho nhau, mà không làm thay đổi tính chính xác của chương trình. --- ### Algebraic Data Type - ADT - ADT is a kind of composite type - Cách kết hợp các type lại với nhau  ---- ### ADT - Sum ```scala enum Either[A, B]: case Left(value: A) case Right(value: B) type sum = A | B ``` - Product ```scala case class Product[A, B](val a: A, val b: B) type Product[A, B] = (A, B) ``` --- ### Sum Type Vậy về mặt cardinalities mà nói thì Sum type sẽ tương đương với phép cộng. ```scala enum Either[A, B]: case Left(value: A) case Right(value: B) ``` Ta thấy: `|Either[A, B]| = |A| + |B|` ---- ### Sum Type ```scala= enum Deal[A, B]: case This(value: A) case Thas(value: B) case TheOther(value: Boolean) ``` - `|Deal[A, B]| = |A| + |B| + |Boolean|` - `|Deal[A, B]| = |A| + |B| + 2` ---- ### Sum Type ```Scala enum Option[A]: case Just(value: A) case None ``` - `|Option[A]| = |A| + 1` - `|Option[Boolean]| = |Boolean| + 1` - `|Option[Boolean]| = 3` --- ### Product Type ```Scala type Product[A, B] = (A, B) ``` `|(A, B)| = |A| * |B|` ---- ### Product Type ```Scala type Mix = (Byte, Boolean) ``` - `|Mix| = |Byte| * |Boolean|` - `|Mix| = 256 * 2` - `|Mix| = 512` --- ### Algebra properties An interesting consequence of all of this cardinality stuff is that we find ourselves able to express *mathematical truths in terms of types*. ---- ### One Trong ADT thì Unit (()) được coi là 1. - `a * 1 = 1 * a = a` - `|(A, Unit)| = |(Unit, A)| = |A|` ---- ### Chứng minh Như ta thấy 2 function `to`, `from` tạo thành một isomorphism giữa A và (A, Unit). => `|A| = |(A, Unit)| = |A| * 1` ```scala val to = (a) => (a, ()) val from = ((a, ())) => a ``` ---- ### Zero Trong ADT thì bottom type (Nothing) được coi là phần tử Zero - `a + 0 = 0 + a = a` - `|Either[A, Nothing]| = |Either[Nothing, A| = |A|` ---- ### Chứng minh ```scala val to = (e: Either[A, Nothing]) => e match case Left(a) => a case Right => throw RuntimeException() val from = (a: A) => Left(a) ``` Vì `Nothing` không có bất kỳ một phần tử nào, nên chúng ta không thể khởi tạo nhánh bên phải cho `Either[A, Nothing]`. ---- ### Một số algebra property khác: - Giao hoán: `a + b = b + a`, `a * b = b * a` - Kết hợp: `a* ( b + c) = a * b + b * c` --- ### Phép trừ và phép chia - [Example in typescript](https://www.typescriptlang.org/docs/handbook/utility-types.html) --- ### Exponentialization (sự luỹ thừa) Question ---- ### Exponentialization Để biểu diễn tính luỹ thừa thì chúng ta sẽ sử dụng function Ví dụ function `val f = Boolean => Boolean` Có bao nhiêu phân biệt implementaion của f? Coi `f = g <=> f(a) = g(a) ∀ a` ---- ### Exponentialization Sẽ có chính xác 4 phân biệt implementation của f: - id - not - const(True) - always return True - const(False) - always return False ``` val const = (a, b) => a ``` ---- ### Exponentialization Tổng quát hoá lên ta có: `|A => B| = |B| ^ |A|`  ---- ### Exponentialization với 0 ``` 0 ^ a = 0 <=> val impossible: A => Nothing a ^ 0 = 1 <=> val zero: Nothing => A = throw RuntimeException() ``` ---- ### Exponentialization với 1 ``` 1 ^ a = 1 <=> val oneToA: A => Unit = const(()) a ^ 1 = a <=> val aToOne: Unit => A ``` ---- ### Exponentialization Question --- ### Tic Tac Toe  ---- ### Tic Tac Toe First naive implemntation ``` case class TicTacToe[A]( topLeft: A, topCenter: A, topRight: A, midLef: A, midCenter: A, midRight: A, botLeft: A, botCenter: A, notRight: A ) ``` ---- ### Tic Tac Toe - empty board ``` val emptyBoard: TicTacToe[Option[Boolean]] = TicTacToe( None, None, None, None, None, None, None, None, None, ) ``` ---- ### Cardinality analysis on TicTacToe ``` |TicTacTole[A]| = |A| * |A| * ... * |A| // 9 times = |A| ^ 9 = |A| ^ (3 * 3) = (|A| ^ 3) ^ 3 ``` ---- ### Cardinality analysis on TicTacToe `3 => 3 => |A|` ---- ### New TicTacToe implementation ```scala enum Three: case One case Two case Three type TicTacToe[A] = Three => Three => A val emptyBoard = (_, _) => None ``` --- ### The Curry–Howard Isomorphism  ---- ### The Curry–Howard Isomorphism Question --- ### Kết luận - Toán, logic và lập trình có mối quan hệ chặt chẽ với nhau - Sử dụng các mệnh đề có sẵn trong toán để chứng minh chương trình được viết ra là chính xác. - Có thể refactor types mà không thay đổi tính chính xác của program --- ### Resource - Book: [Thinkging with types](https://leanpub.com/thinking-with-types) - Talk: [Domain Modeling Made Functional](https://www.youtube.com/watch?v=2JB1_e5wZmU) - Talk: [Propositions as Types](https://www.youtube.com/watch?v=IOiZatlZtGU) ---- ### Philip Wadler  ---- ### Philip Wadler  ---