The Next 700 Module Systems

Musa Al-hassy

Overview

Introduction —The Proposal's Story
1. A Programming Language Has Many Tongues
2. Exploring Grouping Mechanisms
3. Problem Statement
Solution Requirements
1. Desirable Features
2. Related Works
3. Visualisation of Parts of the Proposed “Package Polymorphism”
Approach
Timeline
Conclusion

A Programming Language Has Many Tongues

Expression
Statement
Type
Specification
Proof
Module
Meta-programming

The first five collapse into one uniform language within the dependently-typed language Agda.

So why not the module language?

What is a Module?

Definition: A typed module, context, telescope, package former, record, typeclass is a sequence of tuples:

   Name  :  Type  :=  Optional_Definition

Without types, we obtain essentially JSON Objects.

Purpose: Group related concepts together as single semantic units.

Expectations of Module Systems

Namespacing: New unique local scopes ⇒ de-coupling
Information Hiding: Inaccessibility ⇒ Implementation independence
Citizenship: Grouping mechanisms should be treated like ordinary values
Polymorphism: Grouping mechanisms should group all kinds of things without prejudice
Object-Orientation: Generative modules & Subtyping

What about ⋯

	Packages
≈?	modules
≈?	theories
≈?	contexts
≈?	typeclasses
≈?	⋯
≈?	dependent records

Differences ≈?⇒ Uses & Implementations

Facets of Structuring Mechanisms: An Agda Rendition

Different ways one would encode monoid definitions in their code for different purposes

⇒	Monoids with a dynamically known carrier
⇒	Monoids with a statically known carrier
⇒	Monoids as raw tuples
⇒	Monoids as telescopes
⇄	Derived operations

Monoids as Agda Records

record Monoid-Record : Set₁ where
  infixl 5 _⨾_
  field
    -- Interface
    Carrier  : Set
    Id       : Carrier
    _⨾_      : Carrier → Carrier → Carrier

    -- Constraints
    lid   : ∀{x} → (Id ⨾ x) ≡ x
    rid   : ∀{x} → (x ⨾ Id) ≡ x
    assoc : ∀ x y z → (x ⨾ y) ⨾ z  ≡  x ⨾ (y ⨾ z)

  -- derived result
  pop-Idᵣ : ∀ x y  →  x ⨾ Id ⨾ y  ≡  x ⨾ y
  pop-Idᵣ x y = cong (_⨾ y) rid

⇨ Carrier sets, functions, and axioms all are record fields.

Monoids as Typeclasses

record HasMonoid (Carrier : Set) : Set₁ where
  infixl 5 _⨾_
  field
    Id    : Carrier
    _⨾_   : Carrier → Carrier → Carrier
    lid   : ∀{x} → (Id ⨾ x) ≡ x
    rid   : ∀{x} → (x ⨾ Id) ≡ x
    assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)

  pop-Id-tc : ∀ x y →  x ⨾ Id ⨾ y  ≡  x ⨾ y
  pop-Id-tc x y = cong (_⨾ y) rid

{- We make this record type available
   to instance search, “typeclass”. -}
open HasMonoid {{...}} using (pop-Id-tc)

⇨ Only functions and axioms are record fields —the carrier set is a parameter.

These are the ‘Same’

⇨ Monoids as Agda Records

record Monoid-Record : Set₁ where
  field
    -- Interface
    Carrier  : Set
    Id       : Carrier
    _⨾_      : Carrier → Carrier → Carrier

    -- Constraints
    lid   : ∀{x} → (Id ⨾ x) ≡ x
    rid   : ∀{x} → (x ⨾ Id) ≡ x
    assoc : ∀ x y z → (x ⨾ y) ⨾ z  ≡  x ⨾ (y ⨾ z)

  -- derived result
  pop-Idᵣ : ∀ x y  →  x ⨾ Id ⨾ y  ≡  x ⨾ y
  pop-Idᵣ x y = cong (_⨾ y) rid

{-  Monoid-Record  ≅  Σ C ∶ Set • HasMonoid C  -}

⇨ Monoids as Typeclasses

record HasMonoid (Carrier : Set) : Set₁ where
  field
    -- Interface
    {- Notice that “Carrier” is a parameter. -}
    Id    : Carrier
    _⨾_   : Carrier → Carrier → Carrier

    -- Constraints
    lid   : ∀{x} → (Id ⨾ x) ≡ x
    rid   : ∀{x} → (x ⨾ Id) ≡ x
    assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)

  -- derived result
  pop-Id-tc : ∀ x y →  x ⨾ Id ⨾ y  ≡  x ⨾ y
  pop-Id-tc x y = cong (_⨾ y) rid

{-  HasMonoid  ≅  λ C → Σ M ∶ Monoid-Record • M.Carrier ≡ C  -}

Monoids as Direct Dependent Sums

Monoid-Σ  :  Set₁
Monoid-Σ  =    Σ Carrier ∶ Set
	     • Σ Id ∶ Carrier
	     • Σ _⨾_ ∶ (Carrier → Carrier → Carrier)
	     • Σ lid ∶ (∀{x} → Id ⨾ x ≡ x)
	     • Σ rid ∶ (∀{x} → x ⨾ Id ≡ x)
	     • (∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z))

pop-Id-Σ : ∀{{M : Monoid-Σ}}
		       (let Id  = proj₁ (proj₂ M))
		       (let _⨾_ = proj₁ (proj₂ (proj₂ M)))
		   →  ∀ (x y : proj₁ M)  →  (x ⨾ Id) ⨾ y  ≡  x ⨾ y
pop-Id-Σ {{M}} x y = cong (_⨾ y) (rid {x})
		     where  _⨾_    = proj₁ (proj₂ (proj₂ M))
			    rid    = proj₁ (proj₂ (proj₂ (proj₂ (proj₂ M))))

⇨ The navigational feature of record fields is replaced by projections —i.e., it's just a different encoding.

                   {- Boilerplate -}
		   Carrier′  : Monoid-Σ → Set
		   Carrier′ = proj₁

A Missing Polymorphism

ℕ-record : Monoid-Record
ℕ-record = record { Carrier = ℕ; Id = 0; _⨾_ = _+_; ⋯ }

instance
   ℕ-tc : HasMonoid ℕ
   ℕ-tc = record { Id = 0; _⨾_ = _+_; ⋯ }

   ℕ-Σ : Monoid-Σ
   ℕ-Σ = ℕ , 0 , _+_ , ⋯

ℕ-pop-0ᵣ : ∀ (x y : ℕ) → x + 0 + y  ≡  x + y
ℕ-pop-0ᵣ = pop-Idᵣ ℕ-record

ℕ-pop-0-tc : ∀ (x y : ℕ) → x + 0 + y  ≡  x + y
ℕ-pop-0-tc = pop-Id-tc

ℕ-pop-0-Σ : ∀ (x y : ℕ) → x + 0 + y  ≡  x + y
ℕ-pop-0-Σ = pop-Id-Σ

⇨ One would expect these pop-0 programs
to be instances of one polymorphic function.

⇨ Instead, we currently have three programs that are
instances of three different polymorphic functions.

Monoids as Telescopes

module Monoid-Telescope-User
     (Carrier : Set                      )
     (Id    : Carrier                    )
     (_⨾_   : Carrier → Carrier → Carrier )
     (lid   : ∀ {x}    →  Id ⨾ x  ≡  x   )
     (rid   : ∀ {x}    →  x ⨾ Id  ≡  x   )
     (assoc : ∀ x y z  →  (x ⨾ y) ⨾ z  ≡  x ⨾ (y ⨾ z))
  where

  pop-Id-tel : ∀(x y : Carrier)  →  (x ⨾ Id) ⨾ y  ≡  x ⨾ y
  pop-Id-tel x y = cong (_⨾ y) (rid {x})

open Monoid-Telescope-User ℕ 0 _+_ …

ℕ-pop-tel : ∀(x y : ℕ)  →  x + 0 + y  ≡  x + y
ℕ-pop-tel =   pop-Id-tel

◈	Carrier sets, functions, and axioms all are parameters.

◈	This parameter listing constitutes a ‘telescope’.

Interdefinability

⇨	Different notions are thus interdefinable
⇨	Use-cases distinguish packages
⇨	Distinctions ⇒ duplication of efforts

Generalise! Use a ‘package former’, rather than a particular variation.

Foundational Basis: MMT-Style Theory Presentations

-- Contexts
Γ  ::= ·                       -- empty context
     | x : T [:= T], Γ         -- context with declaration, optional definition
     | includes X, Γ           -- theory inclusion

-- Terms
T ::= x | T₁ T₂ | λ x : T' • T -- variables, application, lambdas
    | Π x : T' • T             -- dependent product
    | [Γ] | ⟨Γ⟩ | T.x          -- record “[type]” and “⟨element⟩” formers, projections
    | Mod X                    -- contravariant “theory to record” internalisation

-- Theory, external grouping, level
Θ ::= .                        -- empty theory
    | X := Γ, Θ                -- a theory can contain named contexts
    | (X : (X₁ → X₂)) := Γ     -- a theory can be a first-class theory morphism

A knowledge-capture mechanism ─not a programming environment.

Problem Summary

😧 :: Coders have to copy-paste-modify packaging structures to obtain different perspectives.

E.g., lifting fields to parameters to ensure correct-by-construction invariants.
Infrastructure is either rewritten for the new perspective, or conversion functions are used.

😄 :: A package should be written once.

Desired perspectives are declared on demand.
Code is written polymorphically along the package, not a particular perspective.

Desirable Features

Uniformity: Treat different notions of packaging the same way.
Genericity: Polymorphism along packages types / package formers.
First-class Extensiblity: Primitives to form new package combinators using the host language.

We can then have better …

Expressivity ⇒ “Package Polymorphism”
Excerption ⇒ “flattening”

Expressivity ─Select Bundling Level

Which aspects of a structure should be exposed?

record Semigroup0 : Set₁ where …

record Semigroup1 (Carrier : Set) : Set₁ where …

record Semigroup2
 (Carrier : Set)
 (_⨾_     : Carrier → Carrier → Carrier) : Set where …

record Semigroup3
 (Carrier : Set)
 (_⨾_ : Carrier → Carrier → Carrier)
 (assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)) : Set where
  -- no fields

Expressivity ─Code along one type, use for another

We want to code along Semigroup1 and use for Semigroup0.

{- Recall -}
record Semigroup0 : Set₁ where …
record Semigroup1 (Carrier : Set) : Set₁ where …

{- Write elegantly along Semigroup1 -}
translate1 : ∀{A B} → (f : A → B) → Bijection f
	   → Semigroup1 A → Semigroup1 B

{- Be able to use the previous for Semigroup0 -}
translate0 : ∀{B : Set} (AS : Semigroup0)
	     (f : Semigroup0.Carrier AS → B)
	   → Bijection f → Semigroup0

Excerption ─Instantiating Deeply Nested Theories

Can we please just declare a Monad without having to declare redundant Applicative and Functor instances.

{- (0) -} instance Monad M       where …  -- (0) needs (1), which needs (2)
{- (1) -} instance Applicative M where …  -- (1, 2) redundant if (0) is given
 {- (2) -} instance Functor M     where …

Excerption ─Instantiating Deeply Nested Theories

Accessing deeply nested fields; e.g., Monoid.Semigroup.Magma.Carrier M.

⇒ flatten hierarchies!

Related Works

C-family: Records, JSON modules ─everything is explicit
Haskell: Single instance typeclasses ─an ‘inference’ mechanism.
OCaml: First-class modules are essentially glorified parameters; enforces a “functor vs. function” dichotomy
[Shields, Peyton Jones 2016]: First-Class Modules for Haskell
Slightly beyond OCaml, but not far enough.

Agda: Dependently-typed typeclasses ─solves diamond problem
Coq: Typeclasses with unification; canonical stuctures triggered by projections
Category Theory: Pullbacks! Declared coercions are found by inference then used in seemingly ill-typed expressions.

Random notes:

A canonical structure is a declaration of a particular instance of a record to be used by the type checker to solve unification problems.
OCaml functors are more or less functions on records in Agda.
Typeclasses are tremendously helpful for having derived constructions be inferrable, e.g., in Haskell instance f a => f (a ,a) to produce Cartesian products for some structure f on a provided there is such a structure on a.

One now uses f methods, that act on a homogeneously-typed pair, and it is inferred that an instance of f a is what is desired –even though no explicit instance for such a pair type was declared! Neato ^_^
Coq's unification is essentially Prolog in disguise.
In some sense, I intend to produce Agda package combinators that are essentially Lisp in disguise.

Solve Diamond Problem using dependent types as follows:

  record X : Set where field doit : Set
  record Y : Set where field x : X
  record Z : Set where field x : X

  record Ω : Set where filed y : Y, z : Z
  {- We now can refer to two X's, possibly different -}

  {- Instead, using typeclasses -}
  record X         : Set where field doit : Set
  record Y (x : X) : Set where
  record Z (x : X) : Set where

  record Ω : Set where filed x : X, y : Y x, z : Z x

With dependent types, X can be lifted to be any telescope of functions that cold conflict ^_^

Competing works?

There are none!

Visualisation of Parts of the Proposed “Package Polymorphism”

Why can't this be done now?

⇨	Agda has a tremendously weak reflection mechanism
⇨	Package formers need to be introduced into the back-end
⇨	Unclear semantics of package formers
⇨	Unclear whether semantics don't break other language features

Proposed Contributions

Module system for DTLs: Modules are ordinary values
- Enables rather than inhibits efficiency
- Well-defined denotational semantics
Use-cases contrasting resulting system with previous approaches
Replace metaprogramming processing with module primitives
An implementation to obtain validation that our system ‘works’

Next Steps

Distill the true requirements for a solution
Deepen understanding of the opportunities given by DTL
Demonstrate the power of the system
Evaluate the mechanisms
- Additions actually contribute to program design?
Ensure a denotational semantics for the mechanisms
Refine above until elegance, or deadline, is reached, whichever comes first

Timeline

The First Pass: May-October 2019: Thorough familiarity with approaches, Agda internals, begun thesis writing
The Middle Pass: November 2019 - February 2020: Implement module formation primitives from the thesis proposal, while forming & extending semantics
The Final Pass: March - April 2020: Implementations meet requirements; mechanise proofs

Conclusion ─Intended Outcomes

Copy-paste-modify is almost always a mistake!

— Wolfram Kahl (•̀ᴗ•́)و

A clean module system for DTLs
Utility Objectives: A variety of use-cases contrasting the resulting system with previous approaches
Demonstrate that module features usually requiring meta-programming can be brought to the data-value level

No more preprocessing for the end-user!

Thank-you

Questions?