The inner life of programming concepts

Tomas Petricek, The Alan Turing Institute
tomasp.net | tomas@tomasp.net | @tomaspetricek

Motivation

What is this talk about?


»type«

»object« »lock«

»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

Types

  • category or kind
  • sets or relations
  • ML or Java types

Monads

  • box or sequencing
  • category theory
  • Haskell or LINQ

Locks

  • physical lock
  • set of names
  • mutual exclusion

Multi-level nature of concepts

All have three levels

We always think, prove and implement!


One level dominates

Common sense types, formal monads, implementation locks

Scientific entities

Programming concepts as 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

Mathematical entities

Variations on proofs and refutations


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)

How the concept of a monad evolves

Originates at formal level
Pre-sheaves in category theory

Metaphors evolve from applications
Containers like lists and sequencing of effects

Implementations drift from theory
Artifacts such as do notation and LINQ

How the concept of a type evolves

Background combines all levels
Type theory, common sense and implementation in Algol

Formalisms change to reflect use
Types as sets, types as relations, types as proofs

Implementations stretches the theory
Unsound type systems for documentation and auto-complete

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

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