Tomas Petricek, The Alan Turing Institute
tomasp.net  tomas@tomasp.net  @tomaspetricek
What is this talk about?
Multilevel nature of programming concepts
Types

Monads

Functions

We always think, prove and implement!
Common sense types, formal monads, implementation functions
Learning from mathematical and scientific entities
Paper on gravity does not change how apples fall
Types across languages don't share the abstract
Types are used to provide autocomplete
We accumulate what we can implement
Proofs and refutations (Imre Lakatos)
Conceptual metaphors (George Lakoff & Rafael Núñez)
Variations on proofs and refutations
Monad is a monoid in the category of endofunctors
Data type M a
satisfying monad laws with operations:
return
of type a > M a
>>=
of type (a > M b) > (M a > M b)
return
wraps thing in a box
>>=
applies operation on all things in a box
Plumbing for composing computations with sideeffects
Plumbing for composing computations with sideeffects
Plumbing for composing computations with sideeffects
Plumbing for composing computations with sideeffects
Presheaves in category theory
Containers like lists and sequencing of effects
Artifacts such as do notation and LINQ
Motivation at formal level
Monads are logic for reasoning about effects
Used differently for implementation
Language abstraction for encoding effects
Shift at implementation level
Abstraction and notation for effects
Causes adaptation at formal level
Algebraic reasoning about syntactic structures
Variations on proofs and refutations
Types as sets, types as relations, types as proofs
Types for error checking, assisting developers
Category of a value, property specification
Rebirth at the implementation layer
No clue that "type" from logic had role in early Algol
Modelled at the formal layer
Type as a set of things (except for pointers)
Shifts at the application layer
Types used for effect tracking, tooling, proving
Adaptation at the formal layer
Types as relations, types as proofs
Gluing tapes, compiling subroutines
Mapping from inputs to outputs
Mathematical lookup tables, math functions
Formal and implementation appearance
Mathematics vs. gluing sequences of instructions
Getting closer at implementation layer
Functions and procedures in Pascal
Implementation and metaphorical shifts
Sending a message to an object in Smalltalk
Adaptation at the formal layer
Unitreturning function with sideeffects
Why understanding programming concepts matters
Multilevel nature
Conceptual, formal, implementation
Useful philosophy of science perspective
Where programs come from, scientific progress
Variations on proofs and refutations
Evolve across all three levels
Function or specification vs. physical implementation
Changes and evolves and stretched by implementations
Hard to cover all philosophy of science positions!
Scientific entities
There is some independent physical reality
Programming concepts
The physical is interlinked with the theoretical