What is the Category for Haskell?

Makoto Hamana
IPL, 2007, September1

We roughly believe · · ·B not just Set
B maybe CPO, due to lazyness, and mixed variance(D ∼= D ⇒ D)
B Folklore: initial algebra = ﬁnial coalgebrae.g. List datatype in Haskell is given by an initial algebra but
contains all inﬁnite lists
B But: there are subtle categorical diﬀerences in several variationsof cpos
I Clarify these!

2

We clarify · · ·B why coincidence?
– which is a suitable category of cpos?
B why inﬁnite data?
B how can we give a datatype functor?
– a non-strict continuous function given by a strict function
B what is Haskell’s algebraic datatype?

3

Categories of CPOs
Def.
A cpo is a poset such that every ω-chain has a lub.
NOTE: it may not have ⊥.
Consider slightly diﬀerent categories: Cpo, Cppo, Cppo⊥
All have cpos as objects.

4CategoryCpo

Cppo Cppo⊥

bottom?

no⊥functionscont. cont.

strictD ×E++[D → E]+++√D+E+noInitial object∅no{⊥}Terminal object{∗}{⊥}√{⊥}√D⊗E√[D →⊥ E]√D⊕Eclosed structure(co)completenessccc√

ccc
noi.alg.=ﬁnal coalg.
5⊥++monoidal closed√√

General Construction of Initial Algebras
Thm. (Basic Lemma [Smyth-Plotkin])
Let C be a category with initial object 0, and F : C → C a functor.
If F preserves the colimit of the ω-chain D0!

- F (0)F!

- F (0)
2F 2!

- ···

then, the initial F -algebra exists and is given by the mediating arrowfrom the colimit of the ω-chain F (0) → F 2 (0) → · · ·colim F D ∼= F (colim D) → colim D

I Why cocompleteness? At least, if C is · · ·cocomplete (existence of any colimit)⇒ 0 → F (0) → F 2 (0) → · · · has a colimit
6Why Cocompleteness?
Cor.
Let C be a cocomplete category. If F is ω-cocontinuos functor,
the initial F -algebra exists.

Note: If C is a cpo, this is Knaster-Tarski ﬁxpoint theorem.

7

Construction of ColimitsThm. [Mac Lane V.2.2]
Let C be a category with coproducts and coequalizers,
and D : I → C a diagram in C.
Then, colim D exists and is given by the coequalizera[φf ]
D(j)(f :j→k)∈arrI

-

[ιf ]

a- colim D

D(i)

i∈I

whereφf : D(j)
ιf : D(j)D(f )- D(k)

ι-ai

8

ι

-ai

D(i)

D(i)

Example: List Types in Cppo⊥
RemarkNon-strict functions can be represented by strict functions in Cppo⊥[X → Y ] ∼= (X)⊥ →⊥ Y
Type constructors are × ⊗ ⊕ (−)⊥
In Set, the list functor isF X = 1 + N×X

9

In Cppo⊥ , assume 1, N to be ﬂat cpos.
FXcons :how stricti. alg.

1 ⊕ N×X

N×L →⊥ Lcons(⊥, ⊥) = ⊥ but cons(a, ⊥) = a:⊥ﬁn.& inf.

1⊕N⊗XN ⊗ L →⊥ Lcons(⊥, l) = cons(a, ⊥) = ⊥N∗

1 ⊕ N ⊗ X⊥

N ⊗ L ⊥ →⊥ Lcons(⊥, l) = ⊥ but cons(a, ⊥) = a:⊥ﬁn.& inf.

cons(⊥, ⊥) = ⊥:⊥ 6= ⊥ﬁn.& inf.

1 ⊕ N⊥ ⊗X⊥ N⊥ ⊗L⊥ →⊥ LRemark(1) (⊥, ⊥) is the least element of N×L(2) cons is a bistrict function(3) cons is a left strict function(4) N⊥ ⊗ X⊥ ∼= (N×X)⊥ , cons is continuous.
“continuous algebra”. Haskell’s datatype10Others
B Initial algebra construction via repeated application of F
B Note: in Cppo⊥ , inﬁnite coproduct should contain lub of
ω-chain while ﬁnite coproduct is just a crushed disjoint sum

11Why Initial Algebra = Final Coalgebra?
Def. Injection-Projection pair (e, p)
C¾

e-Dp
s.t. p ◦ e = id, e ◦ p v id.
If such a pair (e, p) exists, p is uniquely determined by e.
Why coincidence:2!
F!
F!
- 2¾¾0¾F(0)
F(0)
···
HY
HH
HH
@HH
@@I
HH
@@HH
HHµ@@µ10HH
HH
@@HH
HH
@@HH
HH
@@R
HH@jHHH∼¡¡µ¡¡µ3 ¡¡¡µ2¡¡¡¡¡∃!m¡ª?¡ ¾∼
lim D = colim D ∼F(colimD)= F (lim D)=-Actually, µi = F i ! and injective, so has projection
12

Datatypes and Cocomplete Categories
B Set for polynomial types
B Cppo⊥ for initial/ﬁnial (co)algebra coincidence& mixed variant types (“fold” given by Johan Glimming[CALCO’07] for C that is algebraically compact, has products,coproducts, smc, generator)
B Cpo for polynomial with monad types T(“fold” given by Filinski & Stovring [ICFP’07])
B [C, C] for nested datatypes, where C is ω-cocomplete(“generalised fold” given by Johann & Ghani [TLCA’07])
B SetS for simple GADT (e.g. phantom type of Expr)
Conclusion: Cppo⊥ for core Haskell
13

Further Complication: Incorporating Function Types
To treat mixed-variant functor, e.g.,
F X = (X →⊥ X)⊥local continuity is easier to chk than cocontinuity of datatypefunctor.
This means that we need to use order-enriched category Cppo⊥ .
Thm. Every locally continuous functorop

op

F : Cppo⊥ ×Cppo⊥ → Cppo⊥ ×Cppo⊥
has an initial algebra, which is also a ﬁnal coalgebra.

14

References(1) Smyth, Plotkin, The category-theoretic solution of recursive
domain equations, SIAM J. Comput. Vol.11, No.4, 1982.
B Basic lemma (dual is for ﬁnal coalgebra)
B Embedding-projection pair construction for mixed variance inenriched setting ⇒ limit=colimit(2) Lehmann, Smyth, Algebraic Speciﬁcation of Data Types: A
Syntetic Approach, Mathematical Systems Theory 14, 97-139,
1981.
B More detailed account for initial algebras for datatypes, suchas lists, trees, stack, queues(3) Abramsky, Jung, Domain Theory, Handbook of LiCS, Vol.3,
1994.
B Survey and modern account(4) Fiore, PhD thesis, 1996.
15

(5) Simpson, Plotkin, Complete Axioms for Categorical Fixed-point
Operators, LICS’00.

16