\begin{code}
{-# OPTIONS_GHC -Wall #-}
module Feb23 where
— import qualified Prelude as P
import Prelude hiding (Functor)
\end{code}
Learning objectives:
\begin{itemize}
\item Unification
\item Functor, laws
\end{itemize}
Unification: Given two types t, u, find (if possible) a set of substitutions
s such that
subst s t == subst s u
where == means syntactical equal, i.e. identical
ex: t = [ Char ], u = [ a ]
then s = [ a |-> Char ] is such a solution
[a |-> Char] @ t = [ Char ]
[a |-> Char] @ u = [ Char ]
ex: t = Either a (b -> c) u = Either b (b -> d)
s = [ a |-> b, c |-> d]
s @ t = Either b (b -> d) s @ u = Either b (b -> d)
s = [ b |-> a, c |-> d]
s @ t = Either a (a -> d) s @ u = Either a (a -> d)
where s @ t is “apply substitution s to type t”
Unification algorithm, in pseudo code:
unify :: pattern -> pattern -> Maybe Unifier
Unifier = list of substitions
substituion = variable |-> type
ex: t = Char u = Bool
— fail, cannot unify
ex: t = Either a b u = [ c ]
valid patterns:
1. constant names of types, like Char, Bool
2. variables, like a, b, c
3. constructors, like Either a b, [ c ], Maybe a, …
all constructors have a fixed ‘arity’, i.e. number of
arguments.
====
Aside, to answer a question:
Hindley-Milner types, Damas-Milner algorithm
– have extremely good properties
If you try to put *functions* at the type level, things go weird fast…
– second-order unification is undecidable
====
unify :: pattern -> pattern -> Maybe Unifier
unify X X = Just [] — where X is a constant type name
unify X Y = Nothing — where X , Y are a constant type names
unify X v = Just [ v |-> X ] — v variable, X type constant name
unify v X = Just [ v |-> X ] — ditto
unify v (C t1 t2 … tn) = Just [v |-> C t1 t2 … tn]
— and symmetric case
unify (C t1 t2 … tn) (D u1 .. um)
| C == D && n == m = unify t1 u1, unify t2 u2, .. unify tn un
— also need to check solution is ‘coherent’
| otherwise = Nothing
ex: (where things go wrong)
t = a u = a -> a
“occurs check”
————————————-
\begin{code}
class Functor f where
fmap :: (a -> b) -> f a -> f b
\end{code}
for ‘f a’ to be well-typed, f must have kind * -> *, i.e. be a
/type constructor/
A type constructor ‘f’ satisfies ‘Functor’, roughly when
1. f is a sort of container
2. f is a JIT container, i.e. something that will contain ‘a’s when needed
\begin{code}
instance Functor [] where
fmap f l = map f l
instance Functor Maybe where
fmap _ Nothing = Nothing
fmap f (Just a) = Just (f a)
— for Either b c
— thus fmap :: (c -> d) -> Either b c -> Either b d
instance Functor (Either b) where
fmap _ (Left b) = Left b
fmap f (Right c) = Right (f c)
\end{code}
For those who want to go deep: explore |BiFunctor|.
Somewhat more interesting:
\begin{code}
newtype State s a = State (s -> (s , a))
instance Functor (State s) where
fmap f (State g) = State $ \s ->
let (s’, a) = g s in
(s’, f a)
\end{code}
Laws:
1. forall x. fmap id x = id x
2. forall x, f, g. fmap f (fmap g x) = fmap (f . g) x