Motivation

What is this talk about?

»type«

»object« »function«

»monad«

Programming concepts

• Where do they come from?
• How do they evolve?
• How are they used in practice?
• What is their nature?

Programming concepts

Multi-level nature of programming concepts

1. Metaphorical common sense

2. Formal models

3. Computer implementation

Multi-level nature of concepts

All have three levels

We always think, prove and implement!

One level sometimes dominates

Common sense types, formal monads, implementation functions

Programming concepts as entities

Learning from mathematical and scientific entities

Realism and anti-realism debate

More flexible than electrons

Paper on gravity does not change how apples fall

Not just abstraction

Types across languages don't share the abstract

Experimentalist view

Causing effects

Types are used to provide auto-complete

Scientific progress

We accumulate what we can implement

Learning from mathematical entities

How programming concepts evolve

Proofs and refutations (Imre Lakatos)

Where programming concepts come from

Conceptual metaphors (George Lakoff & Rafael Núñez)

Monads as mathematical entities

Variations on proofs and refutations

Mathematical layer

Monad is a monoid in the category of endofunctors

Metaphorical layer: Monads as boxes

return wraps thing in a box

>>= applies operation on all things in a box

Metaphorical layer: Monads as computations

Plumbing for composing computations with side-effects

Metaphorical layer: Monads as computations

Plumbing for composing computations with side-effects

Metaphorical layer: Monads as computations

Plumbing for composing computations with side-effects

Metaphorical layer: Monads as computations

Plumbing for composing computations with side-effects

Monad at multiple levels

Formal level

Pre-sheaves in category theory

Metaphorical layer

Containers like lists and sequencing of effects

Implementation layer

Artifacts such as do notation and LINQ

Shifts and adaptations

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

Types, functions and more

Variations on proofs and refutations

Types in programming languages

Formal layer

Types as sets, types as relations, types as proofs

Implementation layer

Types for error checking, assisting developers

Metaphorical layer

Category of a value, property specification

How the concept of a type evolves

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

Functions in programming languages

Implementation layer

Gluing tapes, compiling sub-routines

Formal layer

Mapping from inputs to outputs

Metaphorical layer

Mathematical lookup tables, math functions

How the concept of a function evolves

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
Unit-returning function with side-effects

Summary

Why understanding programming concepts matters

Computer science method questions

• Metaphors appears only in textbooks
• How to discuss conceptual metaphors
• What to study about implementation level

History and philosophy questions

• Origins of programming concepts
• Link between formal and implementation
• Proofs and refutations like developments

Shifts and adaptations?

• Shift at one layer, followed by adaptation at another
• Joining two concepts, splitting one concept
• Reversal of a shift caused by another layer

The inner life of programming concepts

Multi-level 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

tomasp.net | tomas@tomasp.net | @tomaspetricek

BACKUP SLIDES

Concepts as technical artifacts

Dual nature of technical artifacts

Function or specification vs. physical implementation

Function of programming concepts

Changes and evolves and stretched by implementations

Physical reality

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