@@ -0,0 +1,235 @@
1+## Type System
2+
3+The type system defines the following types:
4+
5+- Primitive Types
6+ - Number
7+ - String
8+ - Boolean
9+- Arrays
10+ - E.g. `[String]`, `[[Number]]`
11+- Records
12+ - E.g. `{ foo :: String, bar :: Number }`
13+- Tagged Unions
14+ - E.g. `data Foo a = Foo | Bar String`
15+- Functions
16+ - E.g. `Number -> String`
17+ - E.g. `(Number, Number) -> Number`
18+ - Functions can have zero or more arguments
19+- Polymorphic types
20+ - E.g. `forall a. a -> a`
21+
22+## Primitive Types
23+
24+The three primitive types `String`, `Number` and `Boolean` correspond to their Javascript equivalents at runtime.
25+
26+PureScript supports the same binary and unary operations on primitive types as Javascript, with the following exceptions:
27+
28+- String concatenation is denoted `++` to differentiate it from numeric addition, `+`
29+- PureScript's `==` and `!=` correspond to Javascript's strong equality tests `===` and `!==`
30+
31+Examples:
32+
33+```haskell
34+num = 1 + 2 * 3
35+str = "Hello, " ++ "World!"
36+bool = 1 > 2 || true
37+```
38+
39+## Arrays
40+
41+PureScript arrays correspond to Javascript arrays at runtime, but all elements must have the same type.
42+
43+Array literals look like Javascript array literals: `[1, 2, 3]`
44+
45+Array elements can be read using array index notation `arr !! index`
46+
47+## Records
48+
49+PureScript records correspond to Javascript objects.
50+
51+Record literals look like Javascript object literals: `{ foo: "Foo" }`
52+
53+Properties can be read by using dot notation: `o.foo`
54+
55+## Tagged Unions
56+
57+Tagged unions consist of one or more constructors, each of which takes zero or one arguments.
58+
59+Tagged unions can only be created using their constructors, and deconstructed through pattern matching (see later).
60+
61+For example:
62+
63+```haskell
64+data Foo a = Foo | Bar String
65+
66+runFoo Foo = "It's a Foo"
67+runFoo (Bar s) = "It's a Bar. The string is " ++ s
68+
69+test = runFoo Foo ++ runFoo (Bar "Test")
70+```
71+
72+In the example, Foo is a tagged union type which has two constructors. It's first constructor `Foo` takes no argument, and it's second `Bar` takes one, which must be a String.
73+
74+`runFoo` is an example of pattern matching on a tagged union type to discover its constructor, and the last line shows how `Foo`s are constructed.
75+
76+## Functions
77+
78+Functions in PureScript can have zero or more arguments in general, just like in Javascript.
79+
80+Functions are introduced by using a backslash followed by a list of argument names:
81+
82+```haskell
83+test1 = \a b -> a + b
84+```
85+
86+which would correspond to the Javascript
87+
88+```javascript
89+function test1(a) {
90+ return function (b) {
91+ return a + b;
92+ }
93+}
94+```
95+
96+Multiple argument functions can be introduced by wrapping the arguments in parentheses, and separating them with commas:
97+
98+```haskell
99+test1 = \(a, b) -> a + b
100+```
101+
102+which generates
103+
104+```javascript
105+function test1(a, b) {
106+ return a + b;
107+}
108+```
109+
110+In the case of a function with no arguments, the parentheses may be omitted, as follows:
111+
112+```haskell
113+test2 = \ -> 100
114+```
115+
116+which would correspond to the Javascript `function test2() { return 100; }`
117+
118+Multiple-argument and single-argument syntax can be mixed, as follows:
119+
120+```haskell
121+test3 = \a (b, c) d -> a + b + c + d
122+```
123+
124+which generates
125+
126+```javascript
127+function test3(a) {
128+ return function (b, c) {
129+ return function (d) {
130+ return a + b + c + d;
131+ }
132+ }
133+}
134+```
135+
136+Functions are applied by providing their arguments inside parentheses:
137+
138+```haskell
139+test1(1, 2, 3)
140+test2()
141+```
142+
143+A special case is made in the case of functions with one argument. These functions can be applied without parentheses, and function application associates to the left:
144+
145+```haskell
146+-- has type Number -> Number -> Number -> Number
147+addThree = \a b c -> a + b + c
148+
149+-- has type Number -> Number -> Number
150+addThree 1
151+
152+-- has type Number -> Number
153+addThree 1 2
154+
155+-- has type Number
156+addThree 1 2 3
157+```
158+
159+## Polymorphic Types
160+
161+Expressions defined at the top level may have polymorphic types.
162+
163+Here is an example:
164+
165+```haskell
166+identity x = x
167+```
168+
169+`identity` is inferred to have (polymorphic) type `forall t0. t0 -> t0`. This means that for any type `t0`, `identity` can be given a value of type `t0` and will give back a value of the same type.
170+
171+A type annotation can also be provided:
172+
173+```haskell
174+identity :: forall a. a -> a
175+identity x = x
176+```
177+
178+Functions may also be polymorphic in row types or type variables with other kinds (see "Kind System"):
179+
180+```haskell
181+addProps o = o.foo + o.bar
182+```
183+
184+Here, `addProps` is inferred to have type `forall r. { foo :: Number, bar :: Number | r } -> Number`. That is, it can take any type which has properties `Foo` and `Bar`, and *any other record properties*.
185+
186+So, the following compiles:
187+
188+```haskell
189+addProps { foo: 1, bar: 2, baz: 3 }
190+```
191+
192+but the following does not:
193+
194+```haskell
195+addProps { foo: 1 }
196+```
197+
198+since the `bar` property is missing.
199+
200+Again, a type annotation can be provided if necessary.
201+
202+## Rank N Types
203+
204+It is also possible for the `forall` quantifier to appear on the left of a function arrow, inside types record fields and data constructors, and in type synonyms.
205+
206+In most cases, a type annotation is necessary when using this feature.
207+
208+As an example, we can pass a polymorphic function as an argument to another function:
209+
210+```haskell
211+poly :: (forall a. a -> a) -> Boolean
212+poly f = (f 0 < 1) == f true
213+```
214+
215+Notice that the polymorphic function's type argument is instantiated to both `Number` and `Boolean`.
216+
217+An argument to `poly` must indeed be polymorphic. For example, the following fails:
218+
219+```haskell
220+test = poly (\n -> n + 1)
221+```
222+
223+since the skolemized type variable `a` does not unify with `Number`.
224+
225+## Type Inference
226+
227+All types can be inferred, but annotations can optionally be provided.
228+
229+## Kind System
230+
231+There are two primitive kinds, the kind `*` of types and the kind `!` of effects.
232+
233+For each kind `k` there is also a kind `# k` of rows, with types of kind `k`. For example `# *` is the kind of rows of types, as used to define records, and `# !` is the kind of rows of effects, used to define the monad `Eff` of extensible effects.
234+
235+Higher kinded types are also supported. That is, a type variable can refer to not only a type or a row, but a type constructor, or row constructor etc.