# Algebra in algebaric data type (ADT) ## Cardinality Cardinality: the number of elements in a set or other grouping, as a property of that grouping. programming context: the number of inhabitants it has, ignoring bottoms  `Nothing` là bottom type có 0 phần tử hay `|Nothing|` = 0 `Unit` thì có duy nhất 1 phần tử hay `|Unit|` = 1 `Boolean` thì có 2 phần tử: `True` và `False`, `|Boolean|` = 2 ## Morphism - morph: to change - ism: system/theory - morphism: thing that changes something với programming context: morphism transformation from one type to another type => a function from type A to type B (A, B can be the same). - Endomorphism: a morphism from a type to itself (A => A function). `Endo` means the same - isomophism: iso bidirectional, a morphism that is reversable, A => B <=> B => A - homomorphism: homo means same, higher order morphism. A morphism that keep the sturcture of type. structure reserving transformation. Any two types that have the same cardinality will always be isomorphic to one another. An isomorphism between types s and t is defined as a pair of functions to and from: ``` val from : T => Q val to : Q => T ∀ t: T => to(from(t)) == t ∀ q: Q => from(to(q)) == q ``` We sometimes write an isomorphism between types s and t as s t. ```scala enum Direction: case Up case Down ``` |Direction| = |Boolean| = 2 ``` val to1 = (d: Direction) => d match case Up => True case Down => False val to2 = (d: Direction) => d match case Up => Fasle case Down => True val from1 = (d: Boolean) => d match case True => Up case False => Down val from2 = (d: Boolean) => d match case True => Down case False => Up ``` Which of the two isomorphisms should we prefer? Does it matter? Ingeneral,foranytwotypeswithcardinalityn,thereare n! unique isomorphisms between them. As far as the math goes, any of these is just as good as any other—and for most purposes, knowing that an isomorphism exists is enough. An isomorphism between types s and t is a proof that for all intents and purposes, s and t are the same thing. ## ADT ### Sum type Sum type <=> phép cộng, tương đương như thế nào? ``` enum Either[A, B] case Left(value: A) case Right(value: B) ``` => `|Either[A, B]| === |A| + |B|` ``` enum Deal[A, B] case This(value: A) case Thas(value: B) case TheOther(value: Boolean) ``` `|Deal[A, B]| = |A| + |B| + |Boolean| = |A| + |B| + 2` ``` enum Option[A] Just(value: A) None ``` `|Option[A]| = |A| + 1` ### Production type Dual to sum types are the so-called product types. Again, we will look at the canonical example first—the pair type (a, b). Analogously, the cardinality of a product type is the product of their cardinalities. `|(A, B)| = |A| * |B|` https://www.youtube.com/watch?v=IOiZatlZtGU ### notes on subtraction & division Subtraction corresponds to types with particular values removed, while division of a type makes some of its values equal (in the sense of being defined equally—rather than having an Eq instance which equates them.) https://www.typescriptlang.org/docs/handbook/utility-types.html#omittype-keys I just checked https://www.typescriptlang.org/docs/handbook/utility-types.html, it seems Omit can mimic division and Exclude can mimic subtraction Ngoài ra đạo hàm tích phân cũng có những ứng dụng trong programming, nhưng nó lại đi qua xa chủ đề của chúng ta ngày hôm nay. To illustrate, consider the theorem a1 = a. When viewed through Curry–Howard, it describes an isomorphism between () -> a and a. Said another way, this theorem shows that there is no distinction between having a value and having a (pure) program that computes that value.