notes.org

Overview and Objectives

Overview - why these topics?

digraph {
  Cats [label="The Categorical Perspective"]
  Expr [label="The Expression Problem"]
  Deno [label="Denotational Design"]
  eDSL [label="Domain Specific Languages"]

  Cats -> Deno
  Deno -> Expr
  Expr -> eDSL
}       

The Categorical Perspective

Category theory grew out of the fields of abstract algebra and algebraic topology it’s goal is to provide a unified abstract view of mathematical strcuture across multiple fields or domains of study. In general mathematical practice if we can show that some object has the same structure, upto isomorphism, as some other well studied object in terms of proofs of it’s theorems; then we can freely inherit all of those results.

The application of Category has become de-riguer in the field of computer science and many strcutures been retro-fitted into many functional languages such as Scala and most notably Haskell.

Whilst the theoretical underpinnings of functional programming, the λ-calculus, type theory etc. can be cast in the language of category theory, cartesian closed categories etc. No language currently rests on category theory foundations although there is at least one proposal of how this could be achieved.

The main advantage in a more general setting is allowing software engineers and programmers to build thier applications in terms of well defined mathematical structures much like engineers in other disciplines. This view underpins the goals of denotational design, the practise of which demands proof of the denotation’s mathematical properties and relies on homomorphic translation to implementations to ensure correctness.

See: Computational trilogy and trinitarianism

graph {
  Comp  [label="Computation and Programming Languages" shape=box]
  Logic [label="Intuitionist Logic and Type Theory" shape=box]
  Cats  [label="Category and Topos Theory" shape=box]

  Comp -- Logic
  Logic -- Cats
  Cats -- Comp
}

Category Theory for Programmers – Bartosz Milewski

The Expression Problem

• Extensibility
• Composability
• Static type-safety

Denotational Design

Conal Elliott

1. Find a well studied mathematical abstraction that is adequate, simple, precise and closely models the domain entity (the denotation) e.g.:
2. Prove the properties in a formal setting.

presentation : Knowledge -> Knowledge

is that a good model? is it mathematically well defined? is it simple and precise?

or the canonical:

image : R x R -> Color

or as I am playing with as an example:

möbius : ℂ -> ℂ

i.e. function composition rather than the normal implementation bound matrix multiplication.

Domain Specific Vocabularies

Aka. Embedded Domain Specific Language (eDSL)

The next 700 Programming Languages – Peter Landin

Notes

Abstract algebra

Structure	Associativity	Identity	Inverse
semigroup	✓
monoid	✓	✓
group	✓	✓	✓

Category Theory Illustrated – Boris Marinov

Algebraic Types

Sum	Either a b
Product	(a, b)
Exponent	(->) a b

“Category” Hask and its Endofunctors

Typeclass	methods	Concept
Functor	fmap <$>	mapping
Applicative	ap <*>	sequence actions
Monad	bind >>=, join, >=>	sequence actions
Traversable	traverse, sequenceA

Not a functor but a Catamorphism (for which we need to understand F-Algebras):

Foldable	fold	reduction
		inductive-types