Code and Notes (Week 9 Tuesday)

Modules
-------

Instead of `foo`, we want an expression of this form instead:

  X ⇒ Bool

(Where Bool was the return type of the slide example `foo`)


Via Curry-Howard
----------------

Important laws for this derivation:

  A ⇒ B ⇒ C  ≡    A ∧ B ⇒ C

  ∀x. (P(x) ⇒ Q) ≡  (∃x. P(x)) ⇒ Q


The first law is a bit like uncurrying:

 uncurry :: (a -> b -> c) -> (a,b) -> c
 uncurry f (a,b) = f a b


Example of the second law:

 P(x)   it rains on day x
 Q      rain has happened

 ∀x. (P(x) ⇒ Q)   On every day, if it rains on that day,
                  rain has happened

 (∃x. P(x)) ⇒ Q   If there is a day when it rains,
                  rain has happened


A student asked via Zoom, why can't we have
(∀x. P(x)) ⇒ Q instead?

There would be two problems with this.

**First**, the equivalence with our original expression
∀x. (P(x) ⇒ Q) doesn't hold in propositional logic.
Thanks to the student who suggested this in the break,
if we assign P and Q to these propositions instead:

 P(x)   it does *not* rain on day x
 Q      it has never rained

Then we have

 ∀x. (P(x) ⇒ Q)   On every day, if it does not rain on
                  that day, then it has never rained.

 (∀x. P(x)) ⇒ Q   If we have that on every day it does
                  not rain, then it has never rained.

Clearly the latter is true but the former isn't, so
the equivalence doesn't hold.

**Second**, even if the equivalence did hold, the formula
gives us a type that does not fit our intended purpose.

Remember, we were seeking a type to give to `foo` to
represent a module that *restricts* access to its internal
implementation from its users behind *some* opaque type x.

This is what is captured by existential type ∃x. P(x):

 foo :: (∃x. (tuple of interface functions of x)) => Bool

Rather, as ∀x. P(x) has universal type, using it would
imply `foo` takes a module that somehow has to work for
*all* types x that its user is *free* to choose.

 foo :: (∀x. (tuple of interface functions of x)) => Bool


Existential Types
-----------------

In Haskell types, there's always an implicit top-level
universal quantification of all type variables

  duplicate :: a -> [a]
  duplicate a = [a,a]

is actually

  duplicate :: forall a. a -> [a]

- When we implement duplicate,
   we don't get to decide what type a is
  Instead, we must write our function
   so that it works for every a
- When we call duplicate, we get to
   instantiate a to be anything we want!

Universally quantified types give:
- a lot of freedom to the user (the consumer)
- a lot of constraints to the implementer (the producer)

Existentially quantified types flip this dynamic around:
- the constraints are all on the user's side (the consumer)
- the freedom is all on the implementer's side (the producer)

Intuitively:
- When you implement a module, you get to decide the
  implementation details
- When you use the module, you can't use it in a way that
  depends on the implementation details


Existential Type Example
------------------------

Yet another example. Here we want three interfaces:
- a starting value
- a way to add two to the current value
- a way to extract the current value

Let's represent the value as an Int
  body = (0, λx. x+2, λx. x)
  body :: Int × (Int -> Int) × (Int -> Int)

  Pack Int body :: ∃a. a × (a -> a) × (a -> Int)


Making a Module
---------------

Same example as above:

  ⊢ Int ok    ⊢ body :: (a × (a -> a) × (a -> Int))[a:=Int]
  _________________________________________________________
      ⊢ Pack Int body :: ∃a. a × (a -> a) × (a -> Int)

Note: The decision of which Ints to turn into a's is
entirely up to the developer's intentions for the module!


Importing a Module
------------------

This time, for the BagModule example from the slides.

An Open that passes the typecheck:

  Open bagModule
    (bag. (empty,add,average).
       average (add (add empty 4) 3)
    ) :: Int

An Open that fails the typecheck:

  Open bagModule
    (bag. (empty,add,average).
       (add (add empty 4) 3) :: bag
    ) -- not well typed

module W9 where

-- A Brief Introduction to Monads

data Exp =
  Num Int
  | Add Exp Exp
  | Div Exp Exp
  deriving (Eq,Show)

-- Haskell's inbuilt Maybe type is defined something like this:
-- data Maybe a = Nothing | Just a

-- But to define a function that takes an instance of such a
-- data type (e.g. to express the return type of a partial
-- function, as for eval below) we have to pattern match so
-- it's defined for all of the data type's constructors.
-- This leads to long-winded, tedious nested pattern matches:

eval :: Exp -> Maybe Int
eval (Num n) = Just n
eval (Add e1 e2) =
  case eval e1 of
    Nothing -> Nothing
    Just n ->
      case eval e2 of
        Nothing -> Nothing
        Just m ->
          Just $ n + m
eval (Div e1 e2) =
  case eval e1 of
    Nothing -> Nothing
    Just n ->
      case eval e2 of
        Nothing -> Nothing
        Just m ->
          if m == 0 then
            Nothing
          else
            Just $ n `div` m

{- Monads in general

  A monad is a type constructor m equipped with two functions:
     return :: a -> m a
     bind   :: m a -> (a -> m b) -> m b

  The bind function has infix (>>=) as syntactic sugar:
     bind m f == (m >>= f)

  Return and bind must satisfy three algebraic laws:
     m >>= return    =  m       (right identity)
     return x >>= k  =  k x     (left identity)
     (m >>= k1) >>= k2 = m >>= \x -> k1 x >>= k2 (associativity)
 -}

{- Haskell's Maybe type as a monad -}

-- Say we define bind and return for Maybe as follows:
-- (>>=)  :: m a -> (a -> m b) -> m b
bind :: Maybe a -> (a -> Maybe b) -> Maybe b
bind Nothing k = Nothing
bind (Just v) k = k v
-- (NB: avoid naming collision with Prelude.return)
return' :: a -> Maybe a
return' v = Just v

-- Then does it satisfy the algebraic laws?
--
-- (right identity? yes)
-- m >>= return
--   = bind m Just
--   = case m of
--       Nothing -> Nothing
--       Just v -> Just v
--   = m -- as required
--
-- (left identity? yes)
-- return x >>= k
--   = bind (Just x) k
--   = k x -- as required
--
-- (associativity? yes)
-- LHS
--   = (m >>= k1) >>= k2
--   = bind (bind m k1) k2
--   Case 1: when m = Nothing
--     bind (bind Nothing k1) k2
--     = bind Nothing k2
--     = Nothing
--     = RHS -- as required, see below
--   Case 2: when m = Just v
--     bind (bind (Just v) k1) k2
--     = bind (k1 v) k2
--     = RHS -- as required, see below
-- RHS
--   = m >>= \x -> k1 x >>= k2
--   = bind m (\x -> bind (k1 x) k2)
--   Case 1: when m = Nothing
--     bind Nothing (\x -> bind (k1 x) k2)
--     = Nothing
--     = LHS -- as required, see above
--   Case 2: when m = Just v
--     bind (Just v) (\x -> bind (k1 x) k2)
--     = (\x -> bind (k1 x) k2) v
--     = bind (k1 v) k2
--     = LHS -- as required, see above

{- Monads as a design pattern -}

-- Two kinds of syntactic sugar for bind can give us much
-- more readable code for our use of the Maybe type than before.

eval' :: Exp -> Maybe Int
eval' (Num n) = Just n
{- Original:
eval' (Add e1 e2) =
  case eval' e1 of
    Nothing -> Nothing
    Just n ->
      case eval' e2 of
        Nothing -> Nothing
        Just m ->
          Just $ n + m
 -}
{- With monads with bind as we defined above:
eval' (Add e1 e2) =
  bind (eval' e1)
  (\n ->
    bind (eval' e2)
    (\m ->
      (return (n + m))))
 -}
{- With monads with bind's infix (>>=) syntax, note this works
 - because (>>=) is Haskell's built-in bind operator and
 - Haskell recognises Maybe as a monad through typeclassing:
eval' (Add e1 e2) =
  eval' e1 >>=
  \n ->
    eval' e2 >>=
    \m -> return $ n + m
 -}
{- With Haskell's inbuilt monad do-syntax: -}
eval' (Add e1 e2) =
  do -- this is not a loop!
     -- implicitly, there is a >>= between each line
    n <- eval' e1
    m <- eval' e2
    return $ n + m
{- And we can do the same for Div -}
eval' (Div e1 e2) =
  do
    n <- eval' e1
    m <- eval' e2
    if m == 0 then
      Nothing
    else
      return (n `div` m)

class myClass:
    __mySecret = 55

myObject = myClass()
# Attempting to access myObject.__mySecret yields an error,
# but myObject._myClass__mySecret yields the "hidden" value.