1 Summary

(Programmers say ‘Type Constructor’, Mathematicians say ‘Type Formation’)

1. Type Constructor F where F A := Some Type involving Type A
2. Assume A -> B
3. Prove F B := Some Type involving Type B with the proof being Types

If we wanted to concretely build the Functor’s implementation fmap f :: F A -> F B,
we trace the Terms of the proof in step 3.

2 Recap Type Formation/Type Constructor

Example below is a Type Formation.

\[ \cfrac{X : Type}{F\ X : Type}\]

ListF is a Type Formation, we can do ListF Nat, ListF Bool , etc

\[ \cfrac {X : Type}{ListF\ X: Type}\]

inductive ListF (X : Type) :=       --Type Formation/Constructor
  | nil : LeafF X                   --Term Constructor
  | cons : X -> ListF X -> ListF X  --Term Constructor

• WARN: DO NOT confuse
  • Type formation/constructor (using X : Type to let the system know ListF X : Type is a possible type)
  • Term constructor (using cons x y to build a term of type ListF X).

3 Example 1

inductive F (X : Type) : Nat -> X := --type formation
  | ...term constructors...

is the type formation F X := (Nat -> X) shown above a functor?

p :: Nat -> A   --Given This
f :: A -> B     --Given This
q :: Nat -> B   --Build This

--once we build q, it is trivial to build
fmap f :: (Nat -> A) -> (Nat -> B)

1. Given function p :: Nat -> A
2. assume we have function f :: A -> B
3. can we build the goal function q :: (Nat -> B)

\[\cfrac{\cfrac{A\rightarrow B \qquad \cfrac{Nat \rightarrow A \qquad [Nat]}{A}}{B}}{Nat \rightarrow B}\]

\[\cfrac{\cfrac{f: A\rightarrow B \qquad \cfrac{p : Nat \rightarrow A \qquad x : [Nat]}{p\ x : A}}{f\ ( p\ x ) : B}}{\lambda x . f\ (p\ x) : Nat \rightarrow B }\]

we have successfully built q :: (Nat -> B) := λx. f (p x)

instance Functor F where
  def fmap (f : A -> B) (p : F A) : F B :=
    λx. f (p x)
--equivalently we can write 
instance Functor F where
  def fmap (f : A -> B) : F A -> F B :=
    λp. λx. f (p x)

Note: Just as we can have different proofs we can have different implementations of the same Functor.

4 Example 2

inductive F (X : Type) : ((X -> Nat) -> Nat) := --type formation
  | ...term constructors...

is the type formation F X := ((X -> Nat) -> Nat) shown above a functor?

p :: ((A -> Nat) -> Nat)  --Given This
f :: A -> B               --Given This
q :: ((B -> Nat) -> Nat)  --Build This

--once we build q, it is trivial to build
fmap f :: ((A -> Nat) -> Nat) -> ((B -> Nat) -> Nat)

1. Given function p :: ((A -> Nat) -> Nat)
2. assume we have function f :: A -> B
3. can we build the function q :: ((B -> Nat) -> Nat)

\[\cfrac{\cfrac{(A \rightarrow Nat) \rightarrow Nat \qquad \cfrac{\cfrac{[B \rightarrow Nat]^{1} \qquad \cfrac{A \rightarrow B \qquad [A]^{0}}{B}}{Nat}}{A^{0} \rightarrow Nat}}{Nat}}{(B \rightarrow Nat)^{1} \rightarrow Nat}\]

\[\cfrac{\cfrac{p : (A \rightarrow Nat) \rightarrow Nat \qquad \cfrac{\cfrac{x : [B \rightarrow Nat]^{1} \qquad \cfrac{f: A \rightarrow B \qquad a: [A]^{0}}{f\ a:B}}{x\ (f\ a):Nat}}{\lambda a.\ x\ (f\ a):A^{0} \rightarrow Nat}}{p\ (\lambda a.\ x\ (f\ a)): Nat}}{\lambda x.\ p\ (\lambda a.\ x\ (f\ a)):(B \rightarrow Nat)^{1} \rightarrow Nat}\]

we have successfully built q :: ((B -> Nat) -> Nat) := λx. p (λa. x (f a))

instance Functor F where
  def fmap (f : A -> B) (p : F A) : F B :=
    λx. p (λa. x (f a))
--equivalently we can write 
instance Functor F where
  def fmap (f : A -> B) : F A -> F B :=
    λp. (λx. p (λa. x (f a)))

5 Monad parser example

• monad has type M S -> (S -> M T) -> M T
• parser has type inductive parser {A : Type} : String -> List (String × A)

Is this parser a monad?

• We need to build a monadparser with type (String -> (String × S)) -> (S -> (String -> (String × T))) -> (String -> (String × T))

\[\cfrac{\cfrac{bind_1 : MA \rightarrow (A \rightarrow M X) \rightarrow M X \qquad lower : M A }{bind_1\ lower : (A \rightarrow M X) \rightarrow M X} \qquad \cfrac{\cfrac{\cfrac{[x : A]}{\cfrac{bind_2 : M B \rightarrow (B \rightarrow M X) \rightarrow M X \qquad upper : M B}{bind_2\ upper : (B \rightarrow M X) \rightarrow M X} \qquad \cfrac{{\cfrac{[y: B]}{\cfrac{result : X \rightarrow M X \qquad list (x, y) : X}{ result\ list (x, y) : M X }}}}{\lambda y . result\ list(x,y) : B \rightarrow M X}}}{bind_2 \ upper\ (\lambda y . result\ list (x,y)) : M X} }{\lambda x. (bind_2 \ upper\ (\lambda y . result\ list(x,y))) : A \rightarrow M X}}{bind_1\ lower (\lambda x. (bind_2 \ upper\ (\lambda y . result\ list(x,y)))) :M X}\]

def newparser : M X = 
  lower `bind` \x =>
  upper `bind` \y =>
  result [x,y]

\[\cfrac{\cfrac{bind_1 : MA \rightarrow (A \rightarrow M X) \rightarrow M X \qquad lower : M A }{bind_1\ lower : (A \rightarrow M X) \rightarrow M X} \qquad \cfrac{\cfrac{\cfrac{[x : A]}{\cfrac{bind_2 : M B \rightarrow (B \rightarrow M X) \rightarrow M X \qquad upper : M B}{bind_2\ upper : (B \rightarrow M X) \rightarrow M X} \qquad \cfrac{{\cfrac{[y: B]}{\cfrac{\cfrac{bind_3 : M C \rightarrow ( C \rightarrow M X) \rightarrow M X \qquad space : M C}{bind_3\ space : (C \rightarrow M X) \rightarrow M X} \qquad \cfrac{\cfrac{[z :C ]}{\cfrac{result : X \rightarrow M X \qquad list (x, y, z) : X}{ result\ list (x, y, z) : M X }}}{\lambda z. result\ list (x, y, z) : C \rightarrow M X}}{ bind_3\ space (\lambda z. result\ list (x, y, z)) : M X}}}}{\lambda y . (bind_3\ space (\lambda z. result\ list (x, y, z))) : B \rightarrow M X}}}{bind_2 \ upper\ \lambda y . (bind_3\ space (\lambda z. result\ list (x, y, z))) : M X} }{\lambda x. (bind_2 \ upper\ \lambda y . (bind_3\ space (\lambda z. result\ list (x, y, z)))) : A \rightarrow M X}}{bind_1\ lower (\lambda x. (bind_2 \ upper\ \lambda y . (bind_3\ space (\lambda z. result\ list (x, y, z))))) : M X}\]

def newparser : M X = 
  lower `bind` \x =>
  upper `bind` \y =>
  space `bind` \z =>
  result [x,y,z]

TODO: But WAIT, we still need to define the implementation of bind