Merge pull request #94 from JordanMartinez/development

Make minor release: PS-0.12.x-v0.8.3

11-Syntax/01-Basic-Syntax/src/03-TypeClasses-and-Newtypes/06-Functional-Dependencies.purs

@@ -2,33 +2,51 @@ module Syntax.Typeclass.MultiParameters.FunctionalDependencies where
 
 {-
 Sometimes in multi-parameter type classes, there is a relationship
-between the types. In such cases, we call them 'functional dependencies'.
+between the types. In such cases, we call them 'functional dependencies' (FDs).
 
-This paper (section 2.1.2) quickly explains why we need functional dependencies:
-http://homepages.inf.ed.ac.uk/jmorri14/pubs/morris-icfp2010-instances.pdf
-In short, it prevents nonsensical code that is otherwise type-safe.
+The next block summarizes these links:
+- https://stackoverflow.com/questions/20040224/functional-dependencies-in-haskell/20040427#20040427
+- https://stackoverflow.com/questions/20040224/functional-dependencies-in-haskell/20040343#20040343
+- Section 2.1.2 shows an example where it needs FDs to work correctly
+    http://homepages.inf.ed.ac.uk/jmorri14/pubs/morris-icfp2010-instances.pdf
 
 Syntax:
   Read
-    "type1 -> type2"
-  as either
-    "There is a function from type1 to type2 (e.g function :: type1 -> type2)."
-  or
-    "'type1' determines what 'type2' will be"
+    class SomeClass type1 type2 | type1 -> type2
+  as
+    "Once you tell the type inferencer what the types on the left-hand side
+    of the arrow are (e.g. `type1`), then the type inferencer will stop
+    trying to infer what the types on the right-hand side of the arrow are
+    (e.g. `type2`).
+
+    Rather, the compiler will look for an instance where
+    the left-hand side types are defined and use that instance
+    to determine what the right-hand side types are. If the compiler finds
+    multiple instances where the left-hand side types are the same types
+    between instances but the right-hand side types are different,
+    it will throw a compiler error.
 -}
 class TypeClassWithFunctionalDependency type1 type2 | type1 -> type2  where
   functionName1 :: type1 -> type2
 
--- example (not sure whether this works...)
+-- Example
 
 data Box a = Box a
 
 class Unwrap a b where
   unwrap :: a -> b
 
--- Here, the type of "a" (Box a) determines what "b" will be:
-instance unwrapBox :: Unwrap (Box a) a where
-  unwrap (Box a) = a
+-- Here, the type of "a" (i.e. Box String) determines what "b" will be:
+instance unwrapBox :: Unwrap (Box String) String where
+  unwrap (Box s) = s
+
+{-
+If we defined another instance of `Unwrap` where
+"a" is the same type (e.g. `Box String`) but `b` is different,
+the compiler will throw an error:
+
+instance unwrapBox2 :: Unwrap (Box String) Int where
+  unwrap (Box s) = length s                                                 -}
 
 ------------------------
 
@@ -39,6 +57,27 @@ class ManyTypesDetermineAnotherType a b c | a b {- n -} -> c  where
 class OneTypeDeterminesManyTypes a b c | a -> b c where
   functionName3 :: a -> b c
 
--- If multiple FDs exist, use this syntax:
-class ManyFDRelationships a b c | a -> b, b -> c where
+------------------------
+
+{-
+In some situations, there might be multiple ways to determine
+a type. In such cases, we can use multiple FDs to tell the compiler
+how to infer a given type in the type class.
+
+The following two FDs can be read as,
+  "Make the type checker try to find an instance of ManyFDRelationships where
+  the `a` type and `b` type are known and then use
+  the instance to infer what the `c` type is.
+
+  However, if the type checker can't ultimately find such an instance,
+  then try to find an instance where the `c` type is known and
+  use that instance to infer what the `a` type and `b` type are."
+-}
+class ManyFDRelationships a b c | a b -> c, c -> a b where
   functionName4 :: a -> b -> c
+
+{-
+In short, the type checker will use the FDs to determine how it should "unify"
+the types together. If one FD fails, it'll go to the next one. If all of them
+fail, it'll assume that there is no such type class instance.
+-}

11-Syntax/03-Type-Level-Programming-Syntax/src/01-An-Overview-of-Terms-and-Concepts.md

@@ -116,3 +116,7 @@ Type-Level programming has 2-3 stages:
 - Terminal
     - Constrain types, so that an impossible state/code fails with a compiler error
     - **Reflection** - convert a type-level instance stored in a `Proxy` type into a value-level instance
+
+## Related Papers
+
+- [Fun with Functional Dependencies](http://www.cse.chalmers.se/~hallgren/Papers/hallgren.pdf)

11-Syntax/03-Type-Level-Programming-Syntax/src/02-Basic-Syntax/03-Defining-Functions/ReadMe.md

@@ -1,5 +1,7 @@
 # Defining Functions
 
+## Solve for X
+
 Normally, when we define a function for value-level programming, it looks like this:
 ```purescript
 function :: InputType -> OutputType
@@ -8,7 +10,7 @@ function InputInstance = OutputInstance
 
 In other words, when given `InputInstance`, return `OutputInstance`. The direction of this "relationship" is ALWAYS in one direction: to the right (i.e. `->`).
 
-When we define a function for type-level programming, we're not defining a function that takes some input and returns an output. Rather, we are defining a "relationship" between some input(s) and some output(s). Because we're doing this at compile-time, this "relationship" already knows (i.e. has fully evaluted) what all of the entities described in the relationship are. Thus, these "relationships" can be applied in multiple directions to create multiple functions. One could say that type-level functions work in **all directions**. To put it another way...:
+When we define a function for type-level programming, we're not defining a function that takes some input and returns an output. Rather, we are defining a "relationship" between some input(s) and some output(s). In other words, these "relationships" can be applied in multiple directions to create multiple functions. One could say that type-level functions work in **multiple directions**. To put it another way...:
 - `function InputInstance` outputs `OutputInstance`
 - `function OutputInstance` outputs `InputInstance`
 
@@ -38,31 +40,137 @@ Thus, we can take this "relationship"/equation and figure out one entity if we k
 This is the same idea used in type-level programming. So, how does this actually work in Purescript? Multi-parameter type classes and functional dependencies.
 
 | The Relationship/Equation | The Number of Functions & its type signature | The implementation of a function
-| - | - |
-| a type class | the number of functional dependencies | type class instances
+| - | - | - |
+| a multi-parameter type class | functional dependencies (the exact number depends) | type class instances
 
-For example, assuming we had a type-level number called `IntK`, we could write both an `add` and two `subtract` functions using just one relationship:
+For example, assuming we had 1) a type-level number called `IntK`, 2) its value-level Proxy type, `IProxy`, and 3) instances for the below type class, we could write an `add` and two `subtract` functions using just one relationship:
 ```purescript
--- the relationship itself, where each entity is already fully known...
-class AddOrSubtract (left :: IntK) (right :: IntK) (total :: IntK)
-  -- the normal "add" function: "total = left + right"
-  | left right -> total
-
-  -- the first 'subtract' function: "right = total - left"
-  , left total -> right
-  -- the second 'subtract' function: "left = total - right"
-  , right total -> left
+-- the relationship itself
+class AddOrSubtract (x :: IntK) (y :: IntK) (total :: IntK)
+  -- the normal "add" function: "total = x + y"
+  | x y -> total
+
+  -- the first 'subtract' function: "y = total - x"
+  , x total -> y
+  -- the second 'subtract' function: "x = total - y"
+  , y total -> x
 ```
 Then, we could use this one relationship as three different functions:
 ```purescript
 -- given two IntK values, I can add them together by returning
 -- `total`, which is "calculated" via the type class `AddOrSubtract`
-addTwoIntK :: AddOrSubtract left right total => left -> right -> total
+addTwoIntK :: forall x y total
+            . AddOrSubtract x y total
+           => IProxy x -> IProxy y -> IProxy total
+addTwoIntK _ _ = IProxyInstance
 
 -- given two IntK values, I can subtract one from another by
--- returning `left`/`right`, which is "calculated"
+-- returning `x`/`y`, which is "calculated"
 -- via the type class `AddOrSubtract`
-subtractIntK_1 :: AddOrSubtract left right total => left -> total -> right
+subtractIntK_1 :: forall x y total
+                . AddOrSubtract x y total
+               => IProxy x -> IProxy total -> IProxy y
+subtractIntK_1 _ _ = IProxyInstance
+
+subtractIntK_2 :: forall x y total
+                . AddOrSubtract x y total
+               => IProxy y -> IProxy total -> IProxy x
+subtractIntK_2 _ _ = IProxyInstance
+```
+
+## Unification
+
+Recall that the type checker / type constraint solver "computes" type-level expressions by figuring out what type something is. Thus, the above analogy is helpful for understanding type-level programming, but it is incomplete without an explanation on how types "unify". In short, **unification** is the way by which the compiler infers or figures out some type. For our context, it is how the type checker computes the "type-level output" of a type-level function. It does this by unifying the undefined types in a type class' definition with a concrete type's instance of that type class.
+
+Let's review something first. In a type class definition and its instance, we have terms to refer to specific parts of it:
+```purescript
+class Show a where
+  show :: a -> String
+
+{-            | 1    |    |    2     |                                -}
+instance s :: (Show a) -> Show (Box a) where
+  show (Box a) = show a
+```
+1. Instance Context
+2. Instance Head
+
+Unification is how logic programming works. A popular language which uses logic programming to compute is Prolog, which has a nice explanation on unification. (Curious readers can see the bottom of the file for links about Prolog). To see the rules for how this works in general, I've adapted the Prolog unification rules defined by Blackburn et al. below:
+1. Two concrete types unify
+    - `String` unifies with `String`
+    - `String` does not unify with `Int`
+2. A concrete type and a polymorphic/generic type (i.e. type variables) unify and the type variable is assigned to a concrete type
+    - Similar to how a variable can be assigned a value, `let a = 5`, so one assigns a type to a type variable:`a = Int`. By this analogy, every time one sees an `a` type in a type signature, they can replace it with `Int`.
+3. Two type variables unify and their relationship is saved
+    - Given `f :: Add a b c => Add c d e => a -> b -> d -> e`, the `c` type in both `Add` constraints are unified and their relationship is "saved". As soon as one of them is assigned to a concrete type, the other will be assigned that type, too.
+4. Complex "type chains" (e.g. a type class and a concrete type's instance of that type class) unify if and only if all of their corresponding arguments unify:
+    - the number of parameter types in the type class is the same number of types in the instance
+        - `class MyClass first second`
+        - `instance i :: MyClass String Int`
+    - instance types unify with the class' constraints
+        - `class (SuperClass constrained) => ThisClass constrained`
+        - `instance a :: SuperClass String`
+        - `instance i :: ThisClass String`
+    - types in the instance context unify with their corresponding class
+        - `instance a :: OtherConstraint a`
+        - `instance i :: (OtherConstraint a) => FastClass a`
+    - a type variable is only assigned once and is not assigned to two different concrete types during the unification process
+
+A type-level function can only "compute" a type-level expression when the types unify. This will fail in a few situations (this list may not be exhaustive):
+- infinite unification: to unify some type, `a`, one must unify some type, `b`, which can only be unified if `a` is unified. After making X many recursive steps, the type inferencer will eventually give up and throw an error. This is a hard-coded number in the Purescript compiler.
+- situations where the type inferencer cannot infer the correct type
+- situations where one needs to do "backtracking". (Either Google this for a better understanding of it or see the Prolog links below)
+
+## Functional Dependencies Reexamined
 
-subtractIntK_2 :: AddOrSubtract left right total => right -> total -> left
+At times, it can be difficult for the type checker to infer what a given type is. Thus, one uses functional dependencies (FDs) to help the compiler. As a reminder, FDs tell the compiler to find an instance whose known types are the types on the left-hand side of the arrow and use that instance to infer what the types on the right-hand side of the arrow are:
+```purescript
+class Add (x :: IntK) (y :: IntK) (total :: IntK)
+  | x y -> total
+  , y total -> x
+  , x total -> y
 ```
+However, sometimes the functional dependencies get a bit more complicated because there are two types on the right-hand side of the arrow. This is where our analogy of a "FDs are type-level functions" starts to break down since a value-level function can only return one value at a time. (Granted, one can use a `Tuple` or `Record` to return multiple values in a container, but the principle still applies.) **With our "relationships", a single FD can sometimes define multiple type-level functions depending on how we use them.**
+
+For example, look at the second FD of [`Prim.Row.Cons`](https://pursuit.purescript.org/builtins/docs/Prim.Row#t:Cons):
+```purescript
+class Cons (label :: Symbol) (a :: Type) (tail :: # Type) (row :: # type)
+  | label a tail -> row
+  , label row -> a tail                                                     {-
+
+The second FD can be read as
+ "If you provide a row and the name of a field in the row,
+  I can give you that field's type and a version of the row
+  without that field (i.e. the tail)"
+
+One can see how this single FD can be used to do two things
+if one uses one of the types and ignores the other:
+- get the type of a some field (use `a`, ignore `tail`)
+- remove a field from a row (use `tail`, ignore `a`)                          -}
+
+-- given this type
+type ExampleRow = (first :: String, second :: Int)
+-- the kinds in Cons would appear as:
+type ExampleCons = Cons
+  (first :: Symbol) (a :: String) (tail :: (second :: Int))
+  (first :: String, second :: Int)
+
+-- given this type
+type ExampleRow2 = (first :: String)
+-- the kinds in Cons would appear as:
+type ExampleCons2 = Cons
+  (first :: Symbol) (a :: String) (tail :: ())
+  (first :: String)
+```
+
+## Prolog Links
+
+Learning Prolog is not necessary to understand how to do type-level programming. However, one may want to learn more about it to understand the idea of unification better. If so, these links helped me understand Prolog:
+- the "Learn Prolog Now" book, [chapter 1 - 2](http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-html)
+- the ["Learn X in Y minutes where X = Prolog"](https://learnxinyminutes.com/docs/prolog/)
+- this [Intro to Prolog](https://www.doc.gold.ac.uk/~mas02gw/prolog_tutorial/prologpages/)
+
+## Works Cited
+
+(for lack of a better section header name...)
+
+Blackburn, Patrick, et al. "2.1: Unification." _Learn Prolog Now!_ vol. 7, College Publications, 2006, http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse5. Accessed 9 Oct. 2018

21-Hello-World/01-FP-Philosophical-Foundations/01-Pure-vs-Impure-Functions.md

@@ -6,6 +6,14 @@ Functional Programming utilizes functions to create programs and focuses on sepa
 
 ### Properties
 
+<hr>
+The following table that shows a comparison of pure and impure functions is licensed under CC BY-SA 4.0
+- Original Credit: Sam Halliday - ["Functional Programming for Mortals with Scalaz"](https://leanpub.com/fpmortals)
+- License: [legal code](https://creativecommons.org/licenses/by-sa/4.0/legalcode) & [legal deed](https://creativecommons.org/licenses/by-sa/4.0/)
+- Changes made
+    - Converted idea into a table that compares pure functions with impure functions
+    - Further expand on "does it iteract with the real world" idea with more examples from the original work
+
 Pure functions have 3 properties, but the third (marked with `*`) is expanded to show its full weight:
 
 |     | Pure | Pure Example | Impure | Impure Example |
@@ -16,6 +24,8 @@ Pure functions have 3 properties, but the third (marked with `*`) is expanded to
 | *Does it acces or modify program state | Never | `newList = oldList.removeElemAt(0)`<br>Original list is copied but never modified | Sometimes | `x++`<br>variable `x` is incremented by one.
 | *Does it throw exceptions? | Never | | Sometimes | `function (e) { throw Exception("error") }` |
 
+<hr>
+
 In many OO languages, pure and impure code are mixed everywhere, making it hard to understand what a function does without examining its body. In FP languages, pure and impure code are separated cleanly, making it easier to understand the code without looking at its implementation.
 
 Programs written in an FP language usually have just one entry point via the `main` function. `Main` is an impure function that calls pure code.

21-Hello-World/08-Type-Level-Programming/.purs-repl

@@ -0,0 +1 @@
+import Prelude