professional-programming.hs

-- This is some boilerplate code, don't worry about it.
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
main = return ()


-- ** Start here for Interlude 1. **

-- I. Types

-- Types are very much like sets:
--   * we define new types from existing types (just as with sets)
--   * we use types as the domains and codomains of our functions.
--
-- Some built-in types are:
--   * `String`, the type consisting of all snippets of text,
--      e.g. `"Hello, World!"`
--   * `Integer`, the type consisting of all integers.
--   * `Rational`, the type consisting of all rational numbers.
--   * `Bool`, the type consisting of just two values, `False` and `True`.
--   * Given types `a` and `b`, the type `(a, b)` consists of
--     all ordered pairs of values of `a` and `b`, respectively.
--     Given `a_1`, ..., `a_n`, we have `(a_1, ..., a_n)` similarly.
--   * Given types `a` and `b`, the type `a -> b` consists of all
--     functions with domain `a` and codomain `b`.
--
-- The keyword `data` is used to define types.
--
--     data {{ type name }} {{ type parameters (if any) }} =
--         {{ data constructor 1 }} {{ arguments (if any) }}
--       | {{ data constructor 2 (if any) }} {{ arguments (if any) }}
--       ...
--       | {{ data constructor n (if any) }} {{ arguments (if any) }}
--
-- Everything after the equal sign forms a description of what the
-- values of the type can be, very similarly to how set-builder notation
-- describes what the elements of a set can be.
--
-- Using the above syntax, the type `Bool` would be defined as
--
--     data Bool = False | True
--

-- In set-builder notation, we'd write
-- Point2D = { Point2D(q1, q2) | q1, q2 ∈ Rational }.
data Point2D = Point2D(Rational, Rational)

data Point3D = Point3D(Rational, Rational, Rational)

makePoint2D :: (Rational, Rational) -> Point2D
makePoint2D(q1, q2) =
  Point2D(q1, q2) -- data construction

printPoint2D :: Point2D -> String
printPoint2D(p) =
  case (p) of
    Point2D(x, y) -> -- destructuring (a.k.a. pattern matching)
      "x = " <> show(x) <> ", y = " <> show(y)

yayOrNay :: Bool -> String
yayOrNay(p) =
  case (p) of
    False -> -- We can pattern match built-in types as well
      "Nay"
    True ->  -- When a type has multiple data constructors, we must write a case for each one.
      "Yay"

-- In set-builder notation, we'd write
-- LabelledPoint2D = { LabelledPoint2D(s, p) | s ∈ String, p ∈ Point2D }.
data LabelledPoint2D = LabelledPoint2D(String, Point2D)

printLabelledPoint2D :: LabelledPoint2D -> String
printLabelledPoint2D(x) =
  case (x) of
    LabelledPoint2D(lbl, p2D) ->
      lbl <> ": " <> printPoint2D(p2D)


-- data LabelledPoint3D = LabelledPoint3D(String, Point3D)
-- printLabelledPoint3D :: printLabelledPoint3D -> String
-- printLabelledPoint3D = ...

-- data LabelledRational = LabelledRational(String, Rational)
-- printLabelledRational :: LabelledRational -> String
-- printLabelledRational = ...

-- data LabelledBool = LabelledBool(String, Bool)
-- printLabelledBool :: LabelledBool -> String
-- printLabelledBool = ...

-- ...

-- This is getting very tedious.
-- Fortunately, there's a better way.

-- This type has a type parameter, `a`.
-- Different types can be substituted in place of `a`.
-- In set-builder notation, we'd write
-- Labelled(a) = { Labelled(s, x) | s ∈ String, x ∈ a }.
data Labelled(a) = Labelled(String, a)


-- This function works no matter what type `a` ends up being.
-- We take two arguments, the second is a function from `a` to `String`
-- which tells us how to print values of type `a`.
printWithLabel :: forall a. (Labelled(a), a -> String) -> String
printWithLabel(x, f) =
  case (x) of
    Labelled(lbl, y) -> lbl <> ": " <> f(y)

-- Now it's easy to make as many similar functions as we want.
printLabelledPoint2D' :: Labelled(Point2D) -> String
printLabelledPoint2D'(l) =
  printWithLabel(l, printPoint2D)


-- Sometimes we might have zero or one of something.
-- The values of `Optional a` are the values of `a`
-- (tagged by the data constructor `NonemptyOptional`)
-- or the value `EmptyOptional`.
-- In set-builder notation, we'd write
-- Optional(a) = { EmptyOptional } ∪ { NonemptyOptional(x) | x ∈ a }
data Optional(a) = EmptyOptional | NonemptyOptional(a)


-- To get a `Rational` from an `Optional Rational`, we'll have to come up
-- with a "default value" for the `EmptyOptional` case.
defaultToZero :: Optional(Rational) -> Rational
defaultToZero(maybe_q) =
  case (maybe_q) of
    EmptyOptional -> 0
    NonemptyOptional(q) -> q


-- The "default value" is arbitrary, it doesn't have to be `0`.
-- We can pick whatever makes sense for our program.
defaultToTen :: Optional(Rational) -> Rational
defaultToTen(maybe_q) =
  case (maybe_q) of
    EmptyOptional -> 10
    NonemptyOptional(q) -> q


-- We can make a function that allows us to plug in a desired default value.
withDefault :: forall a. (a, Optional(a)) -> a
withDefault(x_0, maybe_x) =
  case (maybe_x) of
    EmptyOptional -> x_0
    NonemptyOptional(x) -> x


-- These functions become easier to write now that we have `withDefault`.
defaultToZero' :: Optional(Rational) -> Rational
defaultToZero'(maybe_q) =
  withDefault(0, maybe_q)

defaultToTen' :: Optional(Rational) -> Rational
defaultToTen'(maybe_q) =
  withDefault(10, maybe_q)


-- `Optional(a)` is zero `a`s or one `a`. Values of `List(a)` consist of
-- zero or more values of `a` in a particular sequence.
-- In set-builder notation, we'd write
-- List(a) = { EmptyList } ∪
--           { NonemptyList(x, xs) | x ∈ a, xs ∈ List(a) }
data List(a) = EmptyList | NonemptyList(a, List(a))

-- We deal with lists just like we deal with anything else.
-- We pattern match.
sumList :: List(Rational) -> Rational
sumList(l) =
  case (l) of
    EmptyList -> 0
    NonemptyList(x, xs) -> x + sumList(xs)


-- II. Product of Types

-- The pair type, `(a, b)`, is the product of the types `a` and `b`.
-- Construction: given `x :: a`, `y :: b`

-- Projection onto first coordinate.
pi_1 :: forall a b. (a, b) -> a
pi_1(x, y) =
  x

-- Projection onto second coordinate.
pi_2 :: forall a b. (a, b) -> b
pi_2(x, y) =
  y

-- To finish this, we still need to demonstrate that the universal property
-- of products holds for `(a, b)`.


-- III. Coproduct (Sum) of Types

-- The type `Sum a b` is the coproduct of the types `a` and `b`.
data Sum(a)(b) = Sum1(a) | Sum2(b)

-- Embedding of first summand into the sum.
iota_1 :: forall a b. a -> Sum(a)(b)
iota_1(x) =
  Sum1(x)

-- Embedding of second summand into the sum.
iota_2 :: forall a b. b -> Sum(a)(b)
iota_2(y) =
  Sum2(y)

-- To finish this, we still need to demonstrate that the universal property
-- of sums holds for `Sum(a)(b)`.


-- ** Interlude 1 Over. Head back to the Slideshow. **
-- ** Start here for Interlude 2. **


-- IV. Propositional Logic

-- There is a theorem that establishes a deep connection between logic and
-- programming called the "Curry-Howard Correspondence". The connection is not
-- simply that programming uses logic: it's that programming is logic, but
-- not in the way you're probably thinking. The correspondence is that types
-- are logical propositions, and functions are proofs of logical implications.
-- As a small example, we will prove two theorems from propositional logic
-- by writting functions from and to appropriate types. The obvious
-- hand-written proofs are exactly parallel to implementations of the
-- functions below, down to details of arbitrary depth.

-- The type `Sum(a)(b)` is the proposition `a ∨ b`.
-- The type `a -> b` is the proposition `a ⇒ b`.
-- The type `(a, b)` is the proposition `a ∧ b`.
-- Introduction rules for logical connective are exactly the rules of
-- data construction.
-- Elimination rules for logical connective are exactly the rules of
-- pattern matching.
-- Function definition is implication-introduction.
-- Function application is Modus Ponens.

-- IV.A. Proposition 1: (a ∨ b ⇒ c) ⇔ (a ⇒ c) ∧ (b ⇒ c)

-- Here, we prove (a ∨ b ⇒ c) ⇒ (a ⇒ c) ∧ (b ⇒ c) by
-- writing a function from `Sum(a)(b) -> c` to `(a -> c, b -> c)`.
prop1_fwd :: forall a b c. (Sum(a)(b) -> c) -> (a -> c, b -> c)
prop1_fwd(c_from_a_or_b) = -- ⇒-introduction
  let
    c_from_a :: a -> c
    c_from_a(x) = -- ⇒-introduction
      c_from_a_or_b(iota_1(x)) -- 2 × Modul Ponens

    c_from_b :: b -> c
    c_from_b(y) = -- ⇒-introduction
      c_from_a_or_b(iota_2(y)) -- 2 × Modul Ponens
  in
    (c_from_a, c_from_b) -- ∧-introduction

-- Here, we prove (a ⇒ c) ∧ (b ⇒ c) ⇒ (a ∨ b ⇒ c) by
-- writing a function from `(a -> c, b -> c)` to `Sum(a)(b) -> c`
prop1_rev :: forall a b c. (a -> c, b -> c) -> (Sum(a)(b) -> c)
prop1_rev(c_from_a, c_from_b) = -- ⇒-introduction
  let
    c_from_a_or_b :: Sum a b -> c
    c_from_a_or_b(s) = -- ⇒-introduction
      case (s) of -- ∨-elimination
        Sum1(x) -> c_from_a(x) -- Modus Ponens
        Sum2(y) -> c_from_b(y) -- Modus Ponens
  in
    c_from_a_or_b

-- IV.B. Proposition 2: (a ⇒ b) ∧ (a ⇒ c) ⇔ (a ⇒ b ∧ c)

-- Here, we prove (a ⇒ b) ∧ (a ⇒ c) ⇒ (a ⇒ b ∧ c) by
-- writing a function from `(a -> b, a -> c)` to `a -> (b, c)`
prop2_fwd :: forall a b c. (a -> b, a -> c) -> (a -> (b, c))
prop2_fwd(b_from_a, c_from_a) = -- ⇒-introduction
  let
    b_and_c_from_a :: a -> (b, c)
    b_and_c_from_a(x) = -- ⇒-introduction
      (b_from_a(x), c_from_a(x)) -- 2 × Modul Ponens, ∧-introduction
  in
    b_and_c_from_a

-- Here, we prove (a ⇒ b ∧ c) ⇒ (a ⇒ b) ∧ (a ⇒ c) by
-- writing a function from `a -> (b, c)` to `(a -> b, a -> c)`
prop2_rev :: forall a b c. (a -> (b, c)) -> (a -> b, a -> c)
prop2_rev(b_and_c_from_a) = -- ⇒-introduction
  let
    b_from_a :: a -> b
    b_from_a(x) = -- ⇒-introduction
      pi_1(b_and_c_from_a(x)) -- 2 × Modul Ponens

    c_from_a :: a -> c
    c_from_a(x) = -- ⇒-introduction
      pi_2(b_and_c_from_a(x)) -- 2 × Modul Ponens
  in
    (b_from_a, c_from_a) -- ∧-introduction

-- To come to a nice closure, consider that I chose the particular propositions
-- above for a very specific purpose. If you look at the signatures of the
-- above four functions, you will see that they are exactly the universal
-- properties of sum and product (respectively) that we needed to show from
-- before, so we are done.