12.13 — Lambda-calcul, ROP, Haskell / F# / OCaml, monades#

Ocarina n’invente rien sur le plan théorique. Il applique : du lambda-calcul d’Alonzo Church (1936) aux monades d’Eugenio Moggi (1989) et Philip Wadler (1992-95), formalisé en tant que Railway Oriented Programming par Scott Wlaschin (2014).

1. Lambda-calcul (Church, 1936)#

Définition#

Le lambda-calcul (λ-calcul) est un système formel inventé par Alonzo Church (1903-1995) pour étudier la calculabilité.

Pourquoi c’est fondateur#

1. 1936 : Church prouve que le λ-calcul est Turing-complet (Turing publie sa machine en 1937). Thèse Church-Turing : tout ce qui est calculable mécaniquement peut être exprimé en λ-calcul.
2. Alan Turing était le doctorant de Church à Princeton (PhD, 1938).
3. Le λ-calcul est plus simple que la machine de Turing : seulement 3 constructions. Tout le reste, entiers, booléens, structures de données, est encodé avec ces 3 briques (encodage de Church).

Lambda-calcul typé (Church, 1940)#

Church ajoute des types en 1940 (simply typed lambda calculus, STLC) pour interdire les paradoxes d’auto-application (λx.x x). Chaque variable a un type, et l’application de fonction n’est autorisée que si les types matchent.

C’est l’ancêtre direct des types de Haskell, OCaml, F#, TypeScript, Python, Rust, etc.

Curry-Howard (1934-1969)#

Haskell Curry observe le lien en 1934 (puis le raffine en 1958) et William Howard l’étend en 1969 :

Un programme typé est une preuve mathématique.
Un type est une proposition.
Le type-checker est un vérificateur de preuves.

C’est l’isomorphisme de Curry-Howard.
Si le code compile en étant strictement typé, il est mathématiquement correct sur les dimensions encodées par les types.

D’où mypy --strict dans Ocarina : ce n’est pas une obsession, ce n’est pas de l’autisme, c’est l’application du théorème Curry-Howard dans un cadre industriel.

2. ML (1973 à aujourd’hui)#

Robin Milner et ML (Edinburgh, 1973)#

Robin Milner (1934-2010, Turing Award en 1991) conçoit ML (Meta Language) à Édimbourg comme langage de preuves automatisées (Edinburgh LCF — Logic for Computable Functions).

• Hindley-Milner type system : inférence de types complète sans annotations. Le compilateur devine (infère) tous les types.
• Pattern matching : match x with | Cons (h, t) -> ... | Nil -> ....
• Polymorphism paramétrique : 'a list (liste de n’importe quoi).
• Functions as first-class values : passage d’une fonction comme argument.

Généalogie ML#

                      ML (Edinburgh, 1973)
                               │
             ┌─────────────────┼────────────────────┐
             │                 │                    │
             v                 v                    v
      Standard ML             Caml              Lazy ML
      (Milner, 1983)       (INRIA, 1985)     (Chalmers, ~1984)      SASL, KRC (Turner)
             │                 │                    │                       │
     ┌───────┤                 v                    │                       v
     │       │             Caml Light               │                    Miranda
   SML/NJ    │             (INRIA, 1990)            │                (Turner, 1985)
(Bell Labs & │                 │                    │                       │
 Princeton,  └──> Alice ML     │                    └───────────────────────┤
   1987)        (Saarland,     │                                            v
                  2000)        v                                         Haskell
                             OCaml                                 (SPJ, Wadler, 1990)
                       (Leroy, INRIA, 1996)                                 │
                               └────────────────────────────────────────────┤
                                                                            v
                                                                           F#
                                                                    (Don Syme, 2005)
                                                                            │
                                                                            │
                                                                           […]
                                                                            │
                                                                            │
                                                                            v
                                                               Railway Oriented Programming
                                                                (Wlaschin, NDC London, 2014)
                                                                            │
                                                                            v
                                                                 ┌───────────────────────┐
                                                                 │        Ocarina        │
                                                                 │    Casanova (2026)    │
                                                                 │  Python 3.14 · mypy   │
                                                                 │  Result[T]            │
                                                                 │  ChainRunner · fold   │
                                                                 │  action chain state   │
                                                                 └───────────────────────┘

Note : certaines dates indiquées correspondent aux débuts de conception.

Dates de première publication/implémentation :

• ML → 1979
• Standard ML → 1990
• Caml → 1987

Haskell#

• Type classes (Wadler & Blott, How to make ad-hoc polymorphism less ad hoc, POPL, 1989), ancêtre des traits Rust, des protocols Python Protocol, des interfaces Go.
• Monades comme structure pour la représentation d’effets (Wadler, 1992-95).
• Lazy evaluation par défaut, caractéristique quasi unique d’Haskell.

OCaml (1996)#

F# (2005)#

F# est fortement inspiré d’OCaml, adapté à l’écosystème .NET avec une syntaxe plus accessible aux devs C#. C’est dans la communauté F# que Scott Wlaschin formalisera ROP.

Par ailleurs, F* (2011, Microsoft Research & Inria) est le cousin académique de F# : même syntaxe ML, mais orienté vérification formelle avec types dépendants, peut générer automatiquement du code F# ou OCaml à partir d’un programme vérifié formellement.

3. Monades#

Définition#

Une monade est un type paramétré M[T] (un container générique) accompagné de deux opérations qui obéissent à trois lois :

1. Identité gauche (Left) : return(x) >>= f ≡ f(x)
2. Identité droite (Right) : m >>= return ≡ m
3. Associativité : (m >>= f) >>= g ≡ m >>= (λx. f(x) >>= g)

Note : les monades sont parfois présentées comme des design patterns. La comparaison n’est pas entièrement fausse : elles structurent bien la composition, mais elle est réductrice. Les monades sont des abstractions mathématiques avec des lois formelles, là où les design patterns sont des recettes informelles sans garanties.

Monades célèbres#

Leibniz (1714)#

Le terme monade vient de Gottfried Wilhelm Leibniz (Monadologie, 1714), du grec μονάς (monos, « un, unique »). Leibniz y définit la monade comme « une substance simple, sans parties », l’atome métaphysique du monde. Mac Lane a repris le terme pour la théorie des catégories. Il n’y a aucune filiation conceptuelle entre la monade leibnizienne et la monade de la théorie des catégories : Mac Lane a emprunté le terme pour son sens étymologique.

Eugenio Moggi (1989-91)#

Eugenio Moggi publie en 1989 « Computational lambda-calculus and monads » (LICS). Il importe les monades de la théorie des catégories (Godement, 1958) vers la sémantique des langages. Avant Moggi, les monades étaient une construction abstraite. Après Moggi, c’est devenu le standard pour formaliser les effets de bord.

Philip Wadler (1990-95)#

Philip Wadler (alors à Glasgow, plus tard Edinburgh) popularise les monades en Haskell :

• « Comprehending Monads » (présenté en 1990, publié en 1992)
• « The essence of functional programming » (POPL, 1992)
• « Monads for functional programming » (1992/1995)

Wadler montre comment écrire du code qui ressemble à de l’impératif, séquence d’opérations, états, IO, tout en restant pur grâce aux monades.
C’est l’innovation pédagogique qui ancre les monades dans la pratique Haskell.

4. Railway Oriented Programming (ROP) — Scott Wlaschin, 2014#

Contexte#

Scott Wlaschin, auteur du site fsharpforfunandprofit.com et du livre Domain Modeling Made Functional (Pragmatic Bookshelf, 2018).

En 2014, à NDC London, il donne la conférence « Railway Oriented Programming ».
Vidéo sur Vimeo, transcript sur F# for Fun and Profit.

Pitch#

Most code looks like a railway with one track. Success goes through. Failure throws an exception, jumping off the rails.

Let me show you the two-track railway. Success on one track. Failure on the other. No exception. Every step decides which track to use. The composition is automatic.

Note : le pitch ci-dessus est une paraphrase, pas une citation directe.

C’est, en termes opérationnels, la monade Either rebaptisée avec une métaphore visuelle.

Diagramme#

        ╔═══════╗    ╔═══════╗    ╔═══════╗
in ────>║ step1 ║───>║ step2 ║───>║ step3 ║────> success ─┐
        ╠═══════╣    ╠═══════╣    ╠═══════╣               ├──► result
        ║       ║───>║       ║───>║       ║────> failure ─┘
        ╚═══════╝    ╚═══════╝    ╚═══════╝

Chaque step est une fonction T → Result[U].
La composition est mécanique : tant que c’est success, on continue.
Au premier failure, on bascule dans le rail inférieur et on court-circuite tous les steps suivants.

Théorie sous-jacente#

Either monad :

data Either a b = Left a | Right b

• Right = succès (rail haut).
• Left = échec (rail bas).
• >>= (bind) = la fonction qui chaîne en court-circuitant sur Left.

C’est identique à Result[T] dans Ocarina :

Result[T] = Ok[T] | Fail

Adoption industrielle#

5. Comment Ocarina l’implémente#

Lambda-calcul → closures#

Ocarina utilise systématiquement des closures là où la POO classique utiliserait l’héritage ou l’injection de dépendances.

Une closure est une λ-abstraction avec capture d’environnement : λx.λy.M partiellement appliqué à N donne λy.M[N/x], une fonction qui capture N dans son environnement.

def my_scenario(driver: WebDriver, logger: ILogger) -> Scenario:
    page = MyPage(driver=driver)

    return Scenario(
        # logger is captured in a closure, not "injected"
        setup=lambda: seed_test_user(logger=logger),
        teardown=lambda: delete_test_user(logger=logger),
        test_chain=[...],
    )

C’est de l’IoC par closure, pas par injection.
Le lambda-calcul à l’œuvre.

Hindley-Milner → mypy strict + PEP 695#

class ActionChain[T]:
    def then(
        self, action_or_start: Action[T] | ActionStart[T]
    ) -> ActionStart[T] | NeutralActionStart[T]:
        ...

@final
class ValidationStartBlock[T]:
    def assert_that(
        self, predicate: Predicate[T], *, msg: str | None = None
    ) -> ValidationAssertBlock[T]:
        predicate = _with_msg(predicate, msg, self._name)
        self._chain.add_assertion(self._value, predicate, self._name)
        return ValidationAssertBlock(
            self._value, self._chain, self._name, last_predicate=predicate
        )

def then[U](
    self, new_value: U, *, name: str | None = None
) -> ValidationStartBlock[U]:
    return ValidationStartBlock(new_value, self._chain, name)

PEP 695 (Python 3.12+) introduit la syntaxe [T, U].

Tests de types#

Ocarina intègre une suite de tests dédiée aux types (test_types.yml).

Les cas succès confirment que mypy infère correctement, par exemple que T est préservé de ActionStart jusqu’à ActionChain :

- case: generic_type_preserved_through_chain
  main: |
    chain = ActionStart(lambda: Ok("hello")).failure(lambda e: None).success(lambda: None).execute()
    reveal_type(chain)  # N: Revealed type is .*ActionChain\[.*str.*\]

Les cas échec vérifient que mypy rejette bien ce qui doit être rejeté, qu’un prédicat incompatible ou un handler mal signé produisent une erreur :

- case: incompatible_predicate_type
  main: |
    validate(1234).assert_that(is_email)
  out: |
    main:4: error: .* incompatible type .*

- case: execute_on_action_start_not_allowed
  main: |
    ActionStart(lambda: Ok(42)).execute()
  out: |
    main:4: error: .* has no attribute "execute".*

Le runtime ne vérifie pas les types (c’est du typage STATIQUE !). mypy le fait. Les tests de types vérifient que mypy fait bien son travail dans les deux sens : qu’il accepte ce qui est valide et qu’il refuse ce qui ne l’est pas.

Either / Result → ROP#

Le cœur d’Ocarina est littéralement ROP :

• Result[T] = Ok[T] | Fail, c’est l’Either Monad.
• ChainRunner[T], c’est la composition >>=.
• action chain state, c’est la machine à états qui implémente la dichotomie rail de succès / rail d’échec.
• neutral, convention de Wlaschin : un rail failure continue de faire comme si sans modification jusqu’au bout (équivalent du Left e qui traverse les bind sans s’évaluer).

Computation expressions F# → ChainRunner / chain_actions / drive_page#

F# a les computation expressions (result { … }), Haskell la do-notation.
Les deux proposent bind/>>=.

ChainRunner[T] + chain_actions s’inspirent de la même idée (séquentialité lazy, court-circuit sur échec), mais avec une API manuelle. drive_page dans ocarina-example en est l’alias sémantique direct, il appelle chain_actions à l’identique :

# ocarina/opinionated/dsl/drive_page.py
def drive_page(
    first: ActionSuccess[TPOM], *rest: ActionSuccess[TPOM]
) -> ChainRunner[TPOM]:
    return chain_actions(first, *rest)

Ce qui donne en usage réel dans ocarina-example :

# tests/scenarios/dashboard/access/happy_paths.py
return [
    drive_page(
        act(on_dashboard_login_page, open_dashboard_login_page)
        .failure(just_log_error("Failed to open the dashboard login page..."))
        .success(just_log_success("Opened the dashboard login page!")),
        act(on_dashboard_login_page, verify_dashboard_login_page)
        .failure(log_error_with_current_url("Failed to verify the dashboard login page..."))
        .success(log_success_with_current_url_and_take_screenshot("Verified!")),
    ),
    drive_page(
        act(on_dashboard_welcome_page, verify_dashboard_welcome_page)
        .failure(log_error_with_current_url("Failed to verify the welcome page..."))
        .success(log_success_with_current_url_and_take_screenshot("Verified!")),
    ),
]

Le court-circuit est explicite dans le reducer de chain_actions, si un drive_page échoue, les suivants ne s’exécutent pas :

# ocarina/dsl/testing_with_railway/chain_actions.py
def reducer(chain: ActionChain[T], step: ActionSuccess[T]) -> ActionChain[T]:
    if chain.has_failed():
        return chain  # court-circuit — les étapes suivantes ne s'exécutent pas
    return (
        chain.then(step.__action__)
        .failure(step.__failure_handler__)
        .success(step.__success_handler__)
        .execute()
    )

match_page s’inscrit dans la même famille lazy, il retourne un ChainRunner dont le _thunk() n’évalue les conditions et n’exécute la branche correspondante qu’au moment du .run(), exactement comme chain_actions. Ce qui le distingue, c’est la nature de la composition : conditionnelle plutôt que séquentielle, et il peut s’imbriquer. Dans ocarina-example, il sert à naviguer sur des pages dont l’état est non déterministe à l’avance (A/B tests, bannières aléatoires, anti-bots) :

# tests/scenarios/randomness/level_4/walkthrough.py
return [
    open_madness_random_page,
    match_page(
        branches=[
            when(check_that_madness.is_cors_page, name="is_cors_page",
                 then=go_from_cors_page_to_homepage),
            when(check_that_madness.is_bastia_page, name="is_bastia_page",
                 then=[
                     go_from_this_is_bastia_page_to_random_dsed_page,
                     match_page(
                         branches=[
                             when(check_that_dsed_result.is_bsod_page,
                                  name="is_bsod_page", then=[bsod_dead_end]),
                             when(check_that_dsed_result.is_ids_bypassed_page,
                                  name="is_ids_bypassed_page",
                                  then=go_from_ids_bypassed_page_to_homepage),
                         ],
                     ),
                 ]),
        ],
    ),
]

La différence avec F#/Haskell : dans result { let! x = fetch(); let! y = parse(x) }, le compilateur génère le bind automatiquement. Dans Ocarina, chaque étape câble ses handlers manuellement, .failure() / .success(), et chain_actions / drive_page font le reduce explicitement. Même intention de séquentialité avec court-circuit, mais pas le même mécanisme.

Note : Python n’offrant ni do-notation ni computation expressions, Ocarina n’implémente pas de bind généralisé. La fluent API manuelle (.failure() / .success() / .execute()) est le choix naturel dans ce contexte : il reste lisible sans infrastructure théorique, et suffisant pour les besoins d’un framework de test.

Pur à travers tout l’ISTQB, impur à travers les POM#

L’orchestration, la déclaration des scénarios de test, des suites, des campagnes et du cycle sont pures et implémentent les définitions formelles auxquelles sont habitués les testeurs fonctionnels (ISTQB).

Les POMs, quant à eux, restent présents pour s’adapter à ceux à quoi les automaticiens en test logiciel sont eux-mêmes habitués plutôt que de chercher à « briller » en imposant des abstractions que personne ne comprend.

Holy Book (chapitre « Premiers retours ») :

Et moi je ne suis pas là pour le prestige. Ni même pour le profit.
Je suis là pour notre communauté.

Pour en arriver là, la question n’a jamais été de “briller” plus que les autres.
Il ne s’agit d’ailleurs pas d’un réel challenge.
La question a juste été : de quoi ai-je réellement besoin ?

6. Conclusions#

Le Holy Book ne dit pas « ROP », « monade », « Curry-Howard ».
Mais il applique chacun de ces concepts. Et son argument implicite est :

1. La théorie est disponible depuis 90 ans (Church, 1936).
2. L’industrie du test e2e n’en a rien retenu. Cypress, Playwright, Robot Framework, aucun ne fait de ROP, aucun n’a mypy --strict, aucun n’est formel.
3. Ocarina l’applique dans un cadre tangible pour les testeurs fonctionnels (Python, ISTQB).

Le shift que représente Ocarina (cf. 08-ocarina-in-testing-industry.md) n’est pas une invention, c’est une redistribution de théories matures vers un domaine qui les ignorait.

C’est la posture de Graham dans Beating the Averages : prendre une idée académique mature que l’industrie n’a pas retenue, et en faire un avantage tangible dans un livrable.

7. Rabbit hole — fragments d’un parcours#

… So fuck that little mouse ‘Cause I’m an Albatraoz (Whoo!)

• Algèbre - Les fonctions
• Qu’est-ce que la théorie des groupes
• Le style de code le plus pur, où les bugs sont quasi impossibles
• La State Monad en TypeScript, avec Giuseppe Maggiore
• Des maths, du Python, les réseaux de neurones artificiels de 0
• Mais c’est quoi, un GPT ? Introduction visuelle aux Transformers
• Écrire ma propre base de données de zéro