mirror of
https://github.com/sdiehl/write-you-a-haskell.git
synced 2024-09-19 07:29:00 +03:00
Merge pull request #13 from bmjames/apostrophes
Apostrophe pedantry (fixes #9 and other similar occurrences)
This commit is contained in:
commit
5dd521c926
@ -116,7 +116,7 @@ data Maybe a = Nothing | Just a
|
||||
Values
|
||||
------
|
||||
|
||||
A list is an homogeneously inductively defined sum type of linked cells parameterized over the type of it's
|
||||
A list is an homogeneously inductively defined sum type of linked cells parameterized over the type of its
|
||||
values.
|
||||
|
||||
```haskell
|
||||
@ -139,7 +139,7 @@ List have special value-level syntax
|
||||
(1 : (2 : (3 : []))) = [1,2,3]
|
||||
```
|
||||
|
||||
A tuple is a heterogeneous product type parameterized over both the type of it's two values.
|
||||
A tuple is a heterogeneous product type parameterized over both the type of its two values.
|
||||
|
||||
Tuples also have special value-level syntax.
|
||||
|
||||
@ -333,7 +333,7 @@ the instance search always converges to a single type to make the process of res
|
||||
globally unambiguous.
|
||||
|
||||
For instance the Functor typeclass allows us to "map" a function generically over any type of kind (``* ->
|
||||
*``) applying it on it's internal structure.
|
||||
*``) applying it on its internal structure.
|
||||
|
||||
```haskell
|
||||
class Functor f where
|
||||
@ -522,7 +522,7 @@ IO
|
||||
A value of type IO a is a computation which, when performed, does some I/O
|
||||
before returning a value of type ``a``. The notable feature of Haskell is that
|
||||
IO is still pure, a ``IO a`` is simply a value which stands for a computation
|
||||
which when performed would perform IO and there is no way to peek into it's
|
||||
which when performed would perform IO and there is no way to peek into its
|
||||
contents without running it.
|
||||
|
||||
For instance the following function does not print the numbers 1 to 5 to the screen, it instead builds a list
|
||||
|
@ -537,7 +537,7 @@ returnIO a = VEffect $ return a
|
||||
```
|
||||
|
||||
Effectively we're just recreating the same conceptual relationship that Haskell
|
||||
IO has with it's runtime, but instead our host language uses Haskell as the
|
||||
IO has with its runtime, but instead our host language uses Haskell as the
|
||||
runtime!
|
||||
|
||||
Full Source
|
||||
|
@ -43,8 +43,8 @@ $$
|
||||
|
||||
Milner's observation was that since the typing rules map uniquely onto syntax,
|
||||
we can in effect run the typing rules "backwards" and whenever we don't have a
|
||||
known type for an subexpression, we "guess" by putting a fresh variable in it's
|
||||
place, collecting constraints about it's usage induced by subsequent typing
|
||||
known type for an subexpression, we "guess" by putting a fresh variable in its
|
||||
place, collecting constraints about its usage induced by subsequent typing
|
||||
judgements. This is the essence of *type inference* in the ML family of
|
||||
languages, that by generation and solving of a class of *unification problems*
|
||||
we can reconstruct the types uniquely from the syntax. The algorithm itself is
|
||||
@ -688,7 +688,7 @@ Constraint Solver
|
||||
The Writer layer for the Infer monad contains the generated set of constraints
|
||||
emitted from inference pass. Once inference has completed we are left with a
|
||||
resulting type signature full of meaningless unique fresh variables and a set of
|
||||
constraints that we must solve to refine the type down to it's principle type.
|
||||
constraints that we must solve to refine the type down to its principle type.
|
||||
|
||||
The constraints are pulled out solved by a separate ``Solve`` monad which holds
|
||||
the Unifier ( most general unifier ) solution that when applied to generated
|
||||
@ -704,7 +704,7 @@ type Solve a = StateT Unifier (ExceptT TypeError Identity) a
|
||||
```
|
||||
|
||||
The unification logic is also identical to before, except it is now written
|
||||
independent of inference and stores it's partial state inside of the Solve
|
||||
independent of inference and stores its partial state inside of the Solve
|
||||
monad's state layer.
|
||||
|
||||
```haskell
|
||||
@ -837,7 +837,7 @@ data Value
|
||||
```
|
||||
|
||||
The interpreter is set up an Identity monad. Later it will become a more
|
||||
complicated monad, but for now it's quite simple. The value environment will
|
||||
complicated monad, but for now its quite simple. The value environment will
|
||||
explicitly threaded around, and whenever a closure is created we simply store a
|
||||
copy of the local environment in the closure.
|
||||
|
||||
|
@ -121,7 +121,7 @@ the world in any *observable* way.
|
||||
|
||||
The implementation may perform effects, but central to this definition is the
|
||||
unobservability of such effects. A function is said to *referentially
|
||||
transparent* if replacing a function with it's computed value output yields the
|
||||
transparent* if replacing a function with its computed value output yields the
|
||||
same observable behavior.
|
||||
|
||||
By contrast impure functions are ones which allow unrestricted and observable
|
||||
@ -143,7 +143,7 @@ function f() {
|
||||
```
|
||||
|
||||
The behavior of a pure function is independent of where and when it is
|
||||
evaluated, whereas the sequence a impure function is intrinsically tied to it's
|
||||
evaluated, whereas the sequence a impure function is intrinsically tied to its
|
||||
behavior.
|
||||
|
||||
Functional programming is defined simply as programming strictly with pure
|
||||
|
@ -47,7 +47,7 @@ StandardML, etc. The variation we will discuss first is known as **untyped
|
||||
lambda calculus**, by contrast later we will discuss the **typed lambda
|
||||
calculus** which is an extension thereof.
|
||||
|
||||
A lambda expression is said to bind it's enclosing variable. So the lambda here
|
||||
A lambda expression is said to bind its enclosing variable. So the lambda here
|
||||
binds the name $x$.
|
||||
|
||||
$$
|
||||
@ -239,7 +239,7 @@ $$
|
||||
By convention we will always use a *capture-avoiding* substitution.
|
||||
Substitution will only proceed if the variable is not in the set of free
|
||||
variables of the expression, and if it does then a fresh variable will be
|
||||
created in it's place.
|
||||
created in its place.
|
||||
|
||||
$$
|
||||
(\lambda a. e) x \to [x / a] e \quad \text{if}\ x \notin \FV{e}
|
||||
@ -487,7 +487,7 @@ class Pretty p where
|
||||
```
|
||||
|
||||
The ``p`` variable will indicate our depth within the current structure we're
|
||||
printing and allow us to print out differently to disambiguate it from it's
|
||||
printing and allow us to print out differently to disambiguate it from its
|
||||
surroundings if necessary.
|
||||
|
||||
```haskell
|
||||
|
@ -190,7 +190,7 @@ newtype Parser s a = Parser { parse :: s -> [(a,s)] }
|
||||
```
|
||||
|
||||
For the first couple of simple parsers we will use the String type for
|
||||
simplicities sake, but later will generalize our parsers to use the ``Text``
|
||||
simplicity's sake, but later will generalize our parsers to use the ``Text``
|
||||
type. The combinators and parsing logic will not change, only the lexer and
|
||||
language definitions types will change slightly to a generalized form.
|
||||
|
||||
@ -210,7 +210,7 @@ we defined in our toy library.
|
||||
``<|>`` The choice operator tries to parse the first argument before proceeding to the second. Can be chained sequentially to a generate a sequence of options.
|
||||
``many`` Consumes an arbitrary number of patterns matching the given pattern and returns them as a list.
|
||||
``many1`` Like many but requires at least one match.
|
||||
``optional`` Optionally parses a given pattern returning it's value as a Maybe.
|
||||
``optional`` Optionally parses a given pattern returning its value as a Maybe.
|
||||
``try`` Backtracking operator will let us parse ambiguous matching expressions and restart with a different pattern.
|
||||
``parens`` Parsers the given pattern surrounded by parentheses.
|
||||
|
||||
|
12
path.md
12
path.md
@ -42,7 +42,7 @@ compiler pipeline.*
|
||||
Haskell: A Rich Language
|
||||
-----------------------
|
||||
|
||||
Haskell itself is a beautifully simple language at it's core, although the
|
||||
Haskell itself is a beautifully simple language at its core, although the
|
||||
implementation of GHC is arguably anything but simple! The more one digs into
|
||||
the implementation the more it becomes apparent that a lot of care and
|
||||
forethought was given to making the frontend language as expressive as it is.
|
||||
@ -81,7 +81,7 @@ Scope
|
||||
-----
|
||||
|
||||
Considering our project is intended to be a simple toy language, we are not
|
||||
going to implement all of Haskell 2010. Doing so in it's entirety would actually
|
||||
going to implement all of Haskell 2010. Doing so in its entirety would actually
|
||||
be a fairly involved effort. However we will implement a sizable chunk of the
|
||||
functionality, certainly enough to write non-trivial programs and implement most
|
||||
of the standard Prelude.
|
||||
@ -126,7 +126,7 @@ the [Haskell 98](https://www.haskell.org/onlinereport/) or [Haskell
|
||||
specifications. However in terms of the colloquial usage of the term Haskell,
|
||||
there does seem to be some growing feeling that the "Haskell language family"
|
||||
does exist as a definable subset of the functional programming design space,
|
||||
although many people disagree what it's defining features are. In this sense we
|
||||
although many people disagree what its defining features are. In this sense we
|
||||
will most certainly be writing a language in the Haskell family.
|
||||
|
||||
Intermediate Forms
|
||||
@ -385,7 +385,7 @@ conflict with later passes.
|
||||
|
||||
Ensuring that all names are unique in the syntax tree will allow us more safety
|
||||
later on during program transformation, to know that names cannot implicitly
|
||||
capture and the program can be transformed without changing it's meaning.
|
||||
capture and the program can be transformed without changing its meaning.
|
||||
|
||||
Datatypes
|
||||
---------
|
||||
@ -532,7 +532,7 @@ although unlike GHC we will effectively just be using vanilla System-F without
|
||||
all of the extensions ( equality witness, casts, roles, etc ) that GHC uses to
|
||||
implement more complicated features like GADTs and type families.
|
||||
|
||||
This is one of the most defining feature of GHC Haskell, is it's compilation
|
||||
This is one of the most defining feature of GHC Haskell, is its compilation
|
||||
into a statically typed intermediate Core language. It is a well-engineers
|
||||
detail of GHC's design that has informed much of how Haskell the language has
|
||||
evolved as a language with a exceedingly large frontend language that all melts
|
||||
@ -978,7 +978,7 @@ Fixity Declarations
|
||||
-------------------
|
||||
|
||||
Fixity declarations are exceedingly simple, the store either arity of the
|
||||
declaration along with it's associativity (Left, Right, Non-Associative) and the
|
||||
declaration along with its associativity (Left, Right, Non-Associative) and the
|
||||
infix symbol.
|
||||
|
||||
```haskell
|
||||
|
@ -24,7 +24,7 @@ area of research with many degrees of freedom in the design space.
|
||||
|
||||
*As stated in the introduction, this is a very large topic and we are only going
|
||||
to cover enough of it to get through writing the type checker for our language,
|
||||
not the subject in it's full generality.* The classic text that everyone reads
|
||||
not the subject in its full generality.* The classic text that everyone reads
|
||||
is *Types and Programming Languages* or ( TAPL ) and discusses the topic more in
|
||||
depth. In fact we will follow TAPL very closely with a bit of a Haskell flavor.
|
||||
|
||||
@ -442,7 +442,7 @@ Simply Typed Lambda Calculus
|
||||
The *simply typed lambda calculus* ( STLC ) of Church and Curry is an extension
|
||||
of the lambda calculus that annotates each lambda binder with a type term, The
|
||||
STLC is *explictly typed*, all types are present directly on the binders and to
|
||||
determine the type of any variable in scope we need only traverse to it's
|
||||
determine the type of any variable in scope we need only traverse to its
|
||||
enclosing scope.
|
||||
|
||||
$$
|
||||
|
Loading…
Reference in New Issue
Block a user