CSC 208: Introduction to Purescript

Main.purs

module Main where

import Prelude

import Control.Monad.Eff.Console (logShow)
import Data.Map (Map, lookup, singleton)
import TryPureScript (render, withConsole)

----- Introduction --------------------------------------------------------

{--
Welcome to Purescript!  Purescript is a pure, statically typed functional
programming language for the web.  In this course, we'll use Purescript as
a vehicle to talk about program verification which is our domain for
exploring how mathematical logic is applicable to computer science.

As software developers, we are interested in writing correct programs.  To
do this, we specify the intended behavior of our programs and then verify
that our programs meet these specifications.  We accomplish this in a 
variety of ways, for example:

* We write pre- and post-conditions on our functions and then manually
  inspect our code to determine if the post-condition holds given the
  pre-condition.
* We write tests which codify the behavior of our functions on particular
  inputs.  We then run those tests to verify that these functions behave
  as expected.

In this course, we'll introduce a third way to verify our programs: formal
proof.  When we inspect our programs for correctness, we have an informal
idea about how the program should execute.  To create formal proofs of
program correctness we must:

* Specify the behavior of our program using formal, mathematical logic.
* Prove those logical propositions correct using a combination of the
  rules of deductive reasoning and a program logic which models precisely
  how our programs execute.

To begin, we'll start with a whirlwind introduction of the salient
features of Purescript for our purposes:

(1) Function definitions, static types, and expressions
(2) Algebraic datatypes

From this, we'll define a formal model of how Purescript programs execute,
a substitutive model of computation.  This model applies to any language
that includes expressions (which is virtually every programming language
under the sun).  And then finally, we'll prove properties of Purescript
programs within this model.

--}

----- Installing Purescript -----------------------------------------------

{--

There are two ways that you can use Purescript in this course:

(1) https://try.purescript.org offers an in-browser editor, compiler, and
interpreter for the language.  The editor is live---your code is
constantly compiled and interpreted in the background so you can see the
results of your program at all times.  This requires no setup although
you'll need to be careful about saving your work as there is no save
feature in this browser-based system.

(2) The Purescript Github has instructions to install Purescript locally
on your own machine via the command-line:

https://github.com/purescript/documentation/blob/master/guides/Getting-Started.md

This takes more effort to get working but is a more stable, traditional
alternative to the IDE-based model.

Either approach is fine for this course since we won't be doing too much
work in Purescript.  I recommend (1) and getting in the habit of saving
your work often.  If you are interested in learning Purescript in more
depth, you can go with (2) and pursue alternative resources such as the
Purescript Book:

https://leanpub.com/purescript/read

for more details.

--}

----- Functions, Types, and Expressions ----------------------------------


{--
Like Racket, Purescript is made up of a collection of top-level bindings
which define datatypes and values such as functions.  Unlike Racket,
Purescript is a statically-typed language.  This means that Purescript
checks the consistency of our programs to make sure that they respect
the language's type system.  Recall the following basic constructs of
programming languages:

- An expression is a program construct that evaluates to a value.
- A value is an expression that takes no further steps of evaluation.
- A type classifies an expression by the sorts of values that it
  produces.
  
Examples of expressions include expressions over numbers, booleans, and
strings:
--}

exampleExpressions = do
  logShow true
  logShow (3 * 5)
  logShow (1 + 2 * 3 >= 4 || 1 - 2 / 3 < 4)
  logShow ("Hello " <> "world!")
  -- logShow ("Hello " <> 5)
  
{--
(The `logShow` function is the equivalent of printing to the console
within the Try Purescript sandboxed environment.)

Every one of these expressions has a type which classifies the value
that the expression evaluates to, for example:

+ `true` is a value and has type Boolean
+ `3 * 5` is an expression that evaluates to 15 has type Int
+ `1 + 2 * 3 >= 4 || 1 - 2 / 3 < 4` is an expression that evaluates to
  `true` and has type Boolean
+ `"Hello " <> "world!"` is an expression that evaluates to "Hello world!"
  and has type String

((<>) is the string concat operator.  More generally (<>) is the
semigroup operator of which String is a member.)
  
Purescript's type system ensures we don't intermix expressions in
inappropriate ways.  For example, the following expression:

+ `"Hello " <> 5`

Produces the following error message.  Uncomment out the relevant line
above to see it:

  Could not match type

    Int

  with type

    String


while checking that type Int
  is at least as general as type String
while checking that expression 5
  has type String
in value declaration exampleExpressions

These type errors are caught during compilation, before the program is
run, and thus save the programmer time and effort in debugging their
programs.

--}

increment :: Int -> Int
increment n = n + 1

incrementExamples = do
  logShow (increment 0)
  logShow (increment 10)

{--

Functions in Purescript are similar in intent to Racket although they
are syntactically very different.  Consider the example of the function
`increment` above that increments an integer and returns the incremented
amount:

* A function definition in Purescript has two parts: a signature (the
  first line) and a definition (the second line)
* The function signature contains the name of the function (increment)
  and its type, separated by two colons (::).
* The function definition contains the name of the function (increment),
  the names of its arguments (n), and the definition of the function
  (n+1) separated by an equals sign (=).
* The definition of a function is always a single expression that is the
  result of calling the function.

Note that if you elide the type signature, Purescript (usually) can
figure out the type of the function anyways.  This process is called type
inference and is a hallmark feature of typed functional languages like
Haskell.  It is useful to avoid writing complicated types such as the
type of incrementExamples (which has the complicated type:

+ forall eff. Eff (console :: CONSOLE | eff) Unit

Function types in Purescript capture the expected type of the arguments
of the function as well as the function's intended output type.  In
the example above, the type Int -> Int says that the function takes an
integer as input and produces an integer as output.  In contrast,
consider the simple functions below:

--}

isEven :: Int -> Boolean
isEven n = n `mod` 2 == 0

celebrateBirthday :: String -> Int -> String
celebrateBirthday name age =
  "Enjoy " <> show age <> ", " <> name <> ".  Happy birthday!"

moreFunctionsExamples = do
  logShow (isEven 5)
  logShow (isEven 10)
  logShow (celebrateBirthday "Mary" 21)
  
{--
In the first example, the function isEven of type Int -> Boolean returns
an integer and produces a boolean.  The second example is a function of
two arguments.  The way that we read the type String -> Int -> String
is similar to how we read implications: because (->) is
right-associative, all of the types to the left of the right-most arrow
(here, String and Int) are arguments to the function; the type to the
right is the return type (String).
--}

{--
In addition to basic arithmetic expressions, Purescript provides a
conditional expression form:

  if <expr> then <expr> else <expr>

If the guard of the conditional is true, then the expression evaluates
to the expression following "then" (the if-branch), otherwise, it 
evaluates to the expression following "else" (the else-branch).

--}

printWinner :: Int -> Int -> String
printWinner p1 p2 = if p1 > p2 then "player 1" else "player 2"

printWinnerExamples = do
  logShow (printWinner 0 10)
  logShow (printWinner 10 0)
  logShow (printWinner 0 0)
  
{--
Exercise:

Write a function that simulates the movement of a robot on a
one-dimensional plane, returning the new position of the robot.  The
function takes as input:
  init: the initial position of the robot, 0 <= init < 99
  dir:  the direction the robot moves, either "forward" or "backwards"
  num:  the number of steps the robot takes in the given direction
The one-dimensional plane has 100 spaces that the robot can occupy
(starting at space 0 and ending on space 99).  The robot cannot move
beyond these spaces.
--}

moveRobot :: Int -> String -> Int -> Int
moveRobot init dir num = 0 -- TODO: fill me in

moveRobotTests = do
  logShow (moveRobot 5 "forward" 10)    -- 15
  logShow (moveRobot 3 "backwards" 8)   -- 0
  -- TODO: fill in other tests

main = render =<< withConsole do
  logShow "===== exampleExpressions ====="
  exampleExpressions
  logShow "===== incrementExamples ====="
  incrementExamples
  logShow "===== moreFunctionsExamples ====="
  moreFunctionsExamples
  logShow "===== printWinnerExamples ====="
  printWinnerExamples
  logShow "===== moveRobotTests ====="
  moveRobotTests