CS计算机代考程序代写 algorithm \begin{code}

\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