Skip to content

Commit

Permalink
Merge pull request #95 from JordanMartinez/development
Browse files Browse the repository at this point in the history
Make next major release: PS-0.12.x-v0.9.0
  • Loading branch information
JordanMartinez committed Oct 10, 2018
2 parents 95d853d + d083eeb commit 29f0d13
Show file tree
Hide file tree
Showing 102 changed files with 505 additions and 177 deletions.
1 change: 1 addition & 0 deletions 00-Getting-Started/ReadMe.md
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ TODO, but the general idea is:
- a linter is just a basic static type checker
- easier to write, read, and understand a 'safer language' that compiles to efficient Javascript
- alternatives: Typescript, Coffeescript, Elm, etc.
- [OO "design patterns" in FP languages](http://blog.ezyang.com/2010/05/design-patterns-in-haskel/)

### ...and write Purescript instead of alternatives

Expand Down
12 changes: 12 additions & 0 deletions 11-Syntax/01-Basic-Syntax/ReadMe.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# Basic Syntax

Read through these files in their order. To further grasp the concept, write your own version of the code and see if it still compiles by running:
```bash
pulp --psc-package build
```

To see what the documentation looks like, run this command:
```bash
pulp --psc-package docs
```
Then, open the file, `./generated-docs/Syntax/Documentation.md`, to see what it outputs.
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,3 @@ Anything between the bracket-dash syntax is regarded as a multi-line comment
-}

{- It can also be used to add a comment in-between stuff -}

-- | This is a single-line documentation

-- | This
-- | is
-- | a
-- | multi-line
-- | documentation block, not a comment.
Original file line number Diff line number Diff line change
Expand Up @@ -5,17 +5,10 @@ module Syntax.Record.Basic where
-- "# Type" stands for "Row". It is a special kind used to indicate that
-- there will be an N-sized number of types that are known at compile time.

-- closed rows
type Example_of_an_Empty_Row = ()
type Example_of_a_Single_Row = (fieldName :: ValueType)
type Example_of_a_Multiple_Rows = (first :: ValueType, second :: ValueType)

-- open rows
type Example_of_Open_Rows additionalRows =
(first :: ValueType, second :: ValueType | additionalRows)
type Example_of_Anything_and_Everything_Rows r = ( | r)


data Record_ -- # Type -> Type

-- Think of records as a unordered named TupleN
Expand Down Expand Up @@ -56,15 +49,17 @@ type NestedRecordType = { person :: { skills :: { name :: String } } }
nestedRecordUpdate :: String -> NestedRecordType -> NestedRecordType
nestedRecordUpdate name p = p { person { skills { name = "newName" } } }

{-
Syntax reminder:
syntaxReminder :: String
syntaxReminder = """
"field = value" - update the field
record { field = newValue }
Don't confuse the two operators that go in-between field and value!
"field : value" - create the record's field
{ field: initialValue }
-}
"field OPERATOR value" where OPERATOR is
"=" means "update the field of a record that already exists":
record { field = newValue }
":" means "create the field of a new record":
record { field: initialValue }
"""

-- needed to compile
type ValueType = String
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,34 @@ The following code...
...will output a compiler error since no other fields are allowed!
-}

{-
Rows can either be "closed" or "open." "Closed" rows means that we will
not be adding any other 'fields' to it at a later time. So far, we
have only shown examples of "closed" rows.
"Open" rows means that we might add more 'fields' to it at a later time.
We'll now show the syntax for that.
-}

-- open rows
type Example_of_Closed_Row = (first :: ValueType)
type Example_of_Open_Row additionalRows = (first :: ValueType | additionalRows)

type Closed_Record1 = Record (first :: ValueType)
type Open_Record1 r = Record (first :: ValueType | r)

type Closed_Record2 = { first :: ValueType }
type Open_Record2 r = { first :: ValueType | r}

-- There is a way to get rid of the compiler error using row polymorphism
type OpenRecord1 rowsAreDefinedLater = Record ( | rowsAreDefinedLater)
type OpenRecord2 rowsAreDefinedLater = { | rowsAreDefinedLater}

{-
We can get rid of the compiler error by using open rows and row polymorphism
The below function can be read as
"Given a record that has the field, 'name',
and zero or more other rows I don't care about,
I can give you a String value." -}
rowPolymorphism1 :: forall anyOtherFieldsThatMayExist
. { name :: String | anyOtherFieldsThatMayExist }
-> String
Expand All @@ -44,3 +70,7 @@ test2 =
-- such as this example:
--
-- getName4 { age: 4, stuff: "?" }


-- needed to compile
type ValueType = String
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,10 @@ data Box a = Box a
instance boxShow :: (Show a) => Show (Box a) where
show (Box a) = "Box(" <> show a <> ")"

-- We have names for specific parts of the instance
instance instancePartNames :: (InstanceContext a) => A_TypeClass (InstanceHead a) where
function2 _ = "body"

-- usage
test1 :: Boolean
test1 =
Expand All @@ -73,6 +77,15 @@ test2 =
class TypeClass1 a where
function1 :: a -> String

class InstanceContext a

instance ih :: InstanceContext a

data InstanceHead a = InstanceHead

class A_TypeClass a where
function2 :: a -> String

instance typeclass1 :: TypeClass1 String where
function1 a = a

Expand Down
58 changes: 58 additions & 0 deletions 11-Syntax/01-Basic-Syntax/src/04-Documentation.purs
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
-- | This is a single-line documentation.

-- | This
-- | is
-- | a
-- | multi-line
-- | documentation block, not a comment.
-- | Because it appears above the module declaration below,
-- | it will be combined with the next few documentation blocks.

-- | One can use markdown inside of documentation:
-- |
-- | Look an unordered list:
-- | - item 1
-- | - item 2
-- |
-- | An ordered list:
-- | 1. Item
-- | 2. Item
-- | 3. Item
-- |
-- | A table:
-- |
-- | | One | Two | Three |
-- | | - | - | - |
-- | | a | b | c
-- |
-- | Some code:
-- | ```purescript
-- | f :: Int
-- | f = 4
-- | ```

-- | Module-level documentation
module Syntax.Documentation where

-- | value documentation
value :: Int
value = 4

-- | function documentation
function :: Int -> String
function _ = "easy"

-- | data documentation
data SomeData = SomeData

-- | type documentation
type MyType = String

-- | newtype documentation
newtype SmallInt = SmallInt Int

-- | type class documentation
class MyClass a b | a -> b

-- | instance documentation
instance example :: MyClass String Int
Original file line number Diff line number Diff line change
Expand Up @@ -87,38 +87,56 @@ Let's review something first. In a type class definition and its instance, we ha
class Show a where
show :: a -> String
{- | 1 | | 2 | -}
instance s :: (Show a) -> Show (Box a) where
{- | 1 | | 2 | -}
instance s :: (Show a) => Show (Box a) where
show (Box a) = show a
```
1. Instance Context
2. Instance Head

The "Instance Context" and "Instance Head" terms are crucial to understanding the unification rules below.

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
1. Two concrete terms unify. A "term" for this explanation is either a `Type` or a `Kind`:
- Type
- `String` unifies with `String`
- `String` does not unify with `Int`
- Kind
- kind `BooleanK` unifies with kind `BooleanK`
- kind `BooleanK` does not unify with kind `IntK`
- a Kind term only unifies with other Kind terms, not Type terms.
- a Type term only unifies with other Type terms, not Kind terms.
2. A concrete term and a polymorphic/generic term (i.e. term variable) unify and the term variable is assigned to a concrete term:
- Similar to how a variable can be assigned a value, `let a = 5`, so one assigns a term to a term variable: `a = Int` (type variable assigned to a concrete type) or `a = IntK` (kind variable assigned to a concrete kind). By this analogy, every time one sees an `a` type/kind in a type/kind signature, they can replace it with `Int`/`IntK`.
3. Two term variables unify and their relationship is saved
- Ignoring the `forall .` syntax, given `f :: Add a b c => Add c d e => a -> b -> d -> e`, the `c` type/kind in both `Add` constraints are unified and their relationship is "saved". As soon as one of them is assigned to a concrete term, the other will be assigned that term, too.
4. Complex "term 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 terms in the type class is the same number of terms in the instance
- `class MyClass first second`
- `instance i :: MyClass String Int`
- instance types unify with the class' constraints
- `class (SuperClass constrained) => ThisClass constrained`
- `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
- the type of terms in the type class unify only with their corresponding term type in the instance:
- The type class' Kind terms are made to unify only with other Kind terms, not Type terms, in the instance
- The type class' Type terms are made to unify only with other Type terms, not Kind terms, in the instance.
- a term variable is only assigned once and is not assigned to two different concrete term 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)
- infinite unification: to unify some term, `a`, one must unify some term, `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/kind
- situations where one needs to do "backtracking".
- Normally, the compiler will commit to the instance head before it ever considers the instance context. Once it can figure out the instance head, it will then check whether the head adheres to the instance context. If the compiler cannot figure things out using the head alone, it will fail. If the compiler supported "backtracking," it would also consider the instance context, which would prevent failure in some cases.
- "Backtracking" could be implemented in the compiler by using instance guards, but this has not yet been done. For the current progress on this issue, as well as an example of what "backtrackign" code looks like, see [the related Purescript issue](https://github.com/purescript/purescript/issues/3120).

To understand unification at a deeper level, see these links:
- [Type Checking](https://www.youtube.com/watch?v=r030JkmMLMI). This video **quickly** explains some of the notation used in the paper below, but not all of it.
- [Introduction to Type Inference](https://www.youtube.com/watch?v=il3gD7XMdmA). This video will explain a few more pieces of the notation used in the paper below as well as the problems that arise in type inference. Unfortunately, the teacher goes through concepts quickly and runs out of time, so not everything is immediately understandable through the first viewing.
- [The original paper describing instance chains](http://web.cecs.pdx.edu/~mpj/pubs/instancechains.pdf).

## Functional Dependencies Reexamined

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -81,3 +81,5 @@ TODO: prove the above law using `Box` (a lot of work, so ignoring for now...)
- Do a computation...
- if some condition is true: `when`
- if some condition is false: `unless`

Note: `when`/`unless` is strict. For a lazy version, see [purescript-call-by-name](https://github.com/natefaubion/purescript-call-by-name)
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
# Mutable State: Global vs Local

**Note: This file will use the function, `traceM`. This function will be explained in the `Hello World/Debugging` folder. Please read through that entire folder before continuing here.**

There are two types of mutable state:

| | Global | Local |
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@ In short, the decision was made to drop `Eff`'s "extensible effects". Presumably

(You can read more about the decision making process [here](https://purescript-resources.readthedocs.io/en/latest/eff-to-effect.html). If one is curious about `Eff`, read through [the related section](https://leanpub.com/purescript/read#leanpub-auto-the-eff-monad-1) in the "Purescript by Example" book as it won't be covered here.)

## Aff

The `Aff` monad was introduced and in use before this decision was made. Thus, history explains the naming behind `Aff`: if `Eff` was for synchronous **eff**ects, then `Aff` is for **a**sychronous e**ff**ects.

`Aff` is more powerful than `Effect`, but why that is won't be explained now.
`Aff` is more powerful than `Effect`. For a good introduction to `Aff`, see [this video](https://www.youtube.com/watch?v=dbM72ap30TE).
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@

To use receive input from a user via the terminal, we need to use `Node.ReadLine`'s API. However, using the `Effect` monad for this will not work as expected. Thus, we will be forced to use `Aff`.

In this folder, we'll cover more of `Aff` in the context of `Node.ReadLine` but we will not cover both in all of their complexity. For a deeper explanation of `Aff`, see [this video](https://www.youtube.com/watch?v=dbM72ap30TE&index=20&t=0s&list=WL)
In this folder, we'll cover more of `Aff` in the context of `Node.ReadLine` but we will not cover both in all of their complexity. For a deeper explanation of `Aff`, see [this video](https://www.youtube.com/watch?v=dbM72ap30TE)
65 changes: 65 additions & 0 deletions 21-Hello-World/09-Games/src/02-Random-Number/12-Run/ReadMe.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,68 @@
The remaining two files solve the issues we raised earlier in the Free-based folder:
- `Change-Implementation.purs` uses the first version and changes the normal `MakeGuessF ~> API` "interpretation" to ask the user to confirm their guess before passing the `Guess` value to the Domain level
- `Add-Domain-Term.purs` uses the first version and adds another term, `TellJoke`, to the Domain level. When the user has only one guess left, the computer will tell a terrible joke to ease the player's stress levels.

## Translating Between Languages

To "translate" or "interpret" one language to the next, we follow this pattern:
```purescript
{-
data SourceLanguage
= Term1
| Term2 -}
data Term1F a = Term1F a
type TERM_1 r = (term1 :: FProxy Term1F)
-- smart constructor for `term1F`
data Term2F a = Term2F a
type TERM_2 r = (term2 :: FProxy Term2F) {-
-- smart constructor for `term2F`
data TargetLanguage
= TermA
| TermB -}
data TermAF a = TermAF a
type TERM_A r = (termA :: FProxy TermAF)
-- smart constructor for `termAF`
data TermBF a = TermBF a
type TERM_B r = (termB :: FProxy TermBF)
-- smart constructor for `termBF`
-- Define an algebra that maps one of the source language's terms
-- to one or more of the target language's terms:
term1_to_TargetLanguage :: forall r
. Term1F
-- Note: we can exclude TERM_B
-- if we don't need it.
~> Run (TERM_A + TERM_B + r)
term1_to_TargetLanguage (Term1F next) = do
-- translation goes here...
pure next
-- Define the translation from one language's terms
-- to the next language's terms.
translate :: forall r
-- Define the first run, so that it includes
-- both languages' terms and `r`
. Run (TERM_1 + TERM_2
TERM_A + TERM_B + r)
-- Define the second run, so that it
-- only includes the target language's terms
~> Run (TERM_A + TERM_B + r)
translate = interpret (
send
-- translate each term to the target language's terms
# on _term1 term1_to_TargetLanguage
# on _term2 term2_to_TargetLanguage {-
...
# on _termX termX_to_TargetLanguage -}
)
```
Following this pattern above, we can eventually translate/interpret a `Run` monad into one of two things:
- an effect monad via `Effect` or `Aff`
- a purely computed value via `extract`

0 comments on commit 29f0d13

Please sign in to comment.