Implementation of the algorithm `adm`

This file is a companion to the paper How functorial are (deep) GADTs?. We implement here the algorithm presented in the paper designed to determine which functions can be mapped over a given term of a given GADT.

We would like to emphasize that this is merely proof-of-concept. There is room for improvement in both design choices and running time optimization. It is important to understand that Agda has been chosen for its ability to handle dependent types, which proved useful in the encoding of the GADT language, and not for verification purposes. In particular, the main function adm implementing the algorithm adm of the paper does not enforce the requirements listed in the beginning of Section 3 which make a call to adm legal: it will actually run on any correctly formed term, independently of it being an instance of the given specification or not. Of course, any non-legal call will yield results that are not meaningful. With this in mind, the reader should not be suprised by the presence of default cases in the function admissible and most of the helper functions that accompany it.

module map where

open import Relation.Nullary
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Binary.Core
open import Data.Unit using (⊤) renaming (tt to ∗)
open import Data.Empty using (⊥)
open import Data.Product using (_×_ ; _,_ ; Σ ; proj₁ ; proj₂ )
open import Data.Sum using (_⊎_)
open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ; _≡ᵇ_ )
open import Data.Nat.Properties using (≡ᵇ⇒≡)
open import Agda.Builtin.String
open import Data.Bool using (Bool ; true ; false ; _∧_ ; _∨_ ; not)
open import Data.List
  using (
    List ;
    _++_ ;
    _∷_ ;
    [] ;
    map ;
    zip ;
    zipWith ;
    foldl
  )
  renaming (length to len)
open import Data.Vec
  renaming (
    Vec to tuple ;
    [] to [||] ; _∷_ to _¦_  ;
    map to tuple-map ;
    foldl to tuple-fold ;
    _++_ to _⊕⊕_ ;
    reverse to tuple-reverse ;
    last to _[-1] ;
    length to tuple-len ;
    [_] to [|_|] ;
    zip to tuple-zip ;
    zipWith to tuple-zip-with ;
    toList to [||]→[] ;
    fromList to []→[||]
  )
open import Agda.Builtin.Equality
open import Level renaming (zero to ℓ0 ; suc to ℓnext ; _⊔_  to ℓ∪)

Let us start with some standard proofs that will be useful later. These handle path algebras, properties of natural numbers, and some helper functions on tuples and booleans.

-- induced action of functions on paths
app : ∀ {A B : Set} {a₀ a₁} (f : A → B) → a₀ ≡ a₁ → (f a₀) ≡ (f a₁)
app f refl = refl

-- composition of paths
_∙_ : ∀ {A : Set} {a₀ a₁ a₂ : A} → a₁ ≡ a₂ → a₀ ≡ a₁ → a₀ ≡ a₂
q ∙ refl = q

-- inverse operation on paths
_⁻¹ : ∀ {A : Set} {a₀ a₁ : A} → a₀ ≡ a₁ → a₁ ≡ a₀
refl ⁻¹ = refl

-- transport of an element in a dependent type family over a path
trp : ∀ {A : Set} {a₀ a₁} → (a₀ ≡ a₁) → ∀ {B : A → Set} → B a₀ → B a₁
trp refl b = b

-- transform a path in a sum type into a sum of paths 
Σ≡←≡Σ :
  ∀ {A : Set} {B : A → Set} {a₀ a₁ : A} {b₀ : B a₀} {b₁ : B a₁}
  → (a₀ , b₀) ≡ (a₁ , b₁) → Σ (a₀ ≡ a₁) (λ p → (trp p b₀) ≡ b₁)
Σ≡←≡Σ refl = refl , refl

-- transform a sum of paths into as path in the sum type
≡Σ←Σ≡ :
  ∀ {A : Set} {B : A → Set} {a₀ a₁ : A} {b₀ : B a₀} {b₁ : B a₁}
  → Σ (a₀ ≡ a₁) (λ p → (trp p b₀) ≡ b₁) → (a₀ , b₀) ≡ (a₁ , b₁) 
≡Σ←Σ≡ (refl , refl) = refl

-- neutrality of 0 for addition on the right
n≡n+0 : ∀ {n} → n ≡ n + 0
n≡n+0 {zero} = refl
n≡n+0 {suc n} = app suc n≡n+0

-- restricted case of commutativity of addition : n + 1 + m = n + m + 1
sn+m≡n+sm : ∀ {n m} → suc n + m ≡ n + suc m
sn+m≡n+sm {zero} = refl
sn+m≡n+sm {suc n} = app suc sn+m≡n+sm

-- commutativity of addition
n+m≡m+n : ∀ {n m} → n + m ≡ m + n
n+m≡m+n {zero} {m} = n≡n+0
n+m≡m+n {suc n} {m} = sn+m≡n+sm ∙ (app suc (n+m≡m+n {n} {m}))

-- delete the last element of the tuple
cut-last : ∀ {A : Set} {n : ℕ} → tuple A (suc n) → tuple A n
cut-last {n = zero} xs =  [||]
cut-last {n = suc n} (x ¦ xs) = x ¦ cut-last xs

-- extend a tuple with the given element
insert-last : ∀ {A : Set} {n : ℕ} → A → tuple A n → tuple A (suc n)
insert-last a [||] = [| a |]
insert-last a (x ¦ xs) = x ¦ insert-last a xs

-- create a tuple of the given size with the given element in each cell
dummy-tuple : ∀ {A : Set} n → A → tuple A n
dummy-tuple zero a = [||]
dummy-tuple (suc n) a = a ¦ dummy-tuple n a

-- the usual if-then-else
if_then_else_ : ∀ {A : Set} → Bool → A → A → A
if false then _ else that = that
if true then this else _ = this

Now we will define the syntax of types in our language.

In our language, we are dealing with data type constructors, so we need a set of data type constructor variables. Each such variable is identified by an arity and a label (i.e., an element of ℕ). It is important that we use a set of identifiers with decidable equality so that we can look up a named data type constructor in a given list/tuple.

id-TC-var = ℕ

data TC-var : ℕ → Set where
  TC : id-TC-var → ∀ k → TC-var k

-- boolean test for equality, checking the decidable equality of both the arities and the identifiers
⌊_≟ᴳ_⌋ : ∀ {k k'} → TC-var k → TC-var k' → Bool
⌊ (TC G k) ≟ᴳ (TC G' k') ⌋ = ⌊ G ≟ G' ⌋ ∧ ⌊ k ≟ k' ⌋

Next we will have identifiers for the data constructors that make elements of the data types. We choose ℕ as the set of identifiers again in order to have decidable equality.

id-data-constructor = ℕ

We are now ready to describe the syntax of raw type expressions. We express the syntax over a set var of variables that will be instantiated later. We define the syntax via three mutually recursive data types: type-expr, data-constructor and user-defined. To guide the reader, in this setting the usual inductive definition of lists would be represented by give an element List of user-defined 1, where the usual data constructors nil and cons would each be elements of data-constructor 1, and an expression like List (ℕ × α) would then be an element of type-expr.

module type-syntax {var : Set} where

  interleaved mutual
    data type-expr : Set  -- set of type expressions
    data data-constructor : ℕ → Set  -- data constructors of given type-arity
    data user-defined : ℕ → Set  -- data-type definitions of given arity

A type expression is either the basic type 0, the basic type 1, a type variable, or a composed expression which can take one of three forms:

φ₁ × φ₂ where the φᵢs are type expressions,
φ₁ + φ₂ where the φᵢs are type expressions,
G (φ₁,…,φₙ) where the φᵢs are type expressions, and G is a (non-built-in) data type constructor.

However, the last form needs to be refine into two subcases. Either:

the application of G is done after its definition is completed, or
the application of G is done during the declaration of one of its own data constructors.

For the former, we choose to write the whole definition of the type constructor as the first argument of the application. For the latter, we write only the name of the currently defined data type. (Note that it is impossible to write the whole definition, since the data type is not yet fully defined.)

Because Agda already has types constructions named 0, 1, ×, + and data_where_, we use the superscript ᵀ to differentiate our constructors in what follows.

    data type-expr where
      0ᵀ 1ᵀ : type-expr 
      varᵀ : var → type-expr
      _×ᵀ_ _+ᵀ_ : type-expr → type-expr → type-expr

      -- appᵀ G [ φs ] is the application of G to type expressions φs during the process of defining G
      appᵀ_[_] : ∀ {k} → (TC-var k) → tuple type-expr k → type-expr

      -- data-typeᵀ G [ φs ] is the application of a previously defined data type constructor G to type expressions φs
      data-typeᵀ_[_] : ∀ {k} → user-defined k → tuple type-expr k → type-expr

A user-defined data type constructor is given by a type constructor variable of a certain arity, together with a list of data constructors (for which we recall this type-arity).

    data user-defined where
      dataᵀ_whereᵀ_ : ∀ {k} → (TC-var k) → List (data-constructor k) → user-defined k

A data constructor of a data type constructor G of type-arity k is given by an identifier together with a list of type expressions (the types of the arguments of the constructor), and a k-tuple of type-expressions expressing the instance of G for which the data constructor is constructing an element.

    data data-constructor where
      _∷_⇒ᵀ_ : ∀ {k} → id-data-constructor → List type-expr → tuple type-expr k → data-constructor k

We define as well some helper functions dealing type expressions.

    -- return the arity of the outermost constructor in a type expression
    outmost-arity : type-expr → ℕ
    outmost-arity 0ᵀ = 0
    outmost-arity 1ᵀ = 0
    outmost-arity (varᵀ x) = 1
    outmost-arity (e ×ᵀ e₁) = 2
    outmost-arity (e +ᵀ e₁) = 2
    outmost-arity (appᵀ_[_] {k} _ _) = k
    outmost-arity (data-typeᵀ_[_] {k} _ _)  = k
    
    -- return the number of arguments that a data constructor is expecting
    data-constructor-term-arity : ∀ {k} → data-constructor k → ℕ
    data-constructor-term-arity (_ ∷ Fs ⇒ᵀ _) = len Fs

    -- return the identifier of the type constructor variable used in the definition of a given data type
    user-defined-name : ∀ {k} → user-defined k → TC-var k
    user-defined-name (dataᵀ G whereᵀ _) = G

    -- return the list of data constructors in the definition of a given data type
    user-defined-cs : ∀ {k} → user-defined k → List (data-constructor k)
    user-defined-cs (dataᵀ _ whereᵀ cs) = cs

open type-syntax public

Of course, this raw syntax is very permissive. To structure our type calculus and make sure that it captures the informal idea of GADTs explained in the paper, we will coerce the raw syntax through inference rules. In order to do so, we first introduce contexts:

module context-handling {var : Set} where

  -- a context is either empty or Γ,α with Γ a context and α a variable 
  data context : Set where 
    ∅ : context
    _,_ : context → var → context


  -- length of a context
  ⌈_⌉ : context → ℕ
  ⌈ ∅ ⌉ = 0
  ⌈ Γ , _ ⌉ = suc ⌈ Γ ⌉


  --concatenation of contexts
  _,,_ : context → context → context
  Γ ,, ∅ = Γ
  Γ ,, (Γ' , α) = (Γ ,, Γ') , α


  -- make a context from a tuple of variables
  ⟦_⟧ : ∀ {k} → tuple var k → context
  ⟦ [||] ⟧ = ∅
  ⟦ α ¦ αs ⟧ = (∅ , α) ,, ⟦ αs ⟧

  
  -- the length of the concatenation of two contexts is the sum of the lengths of those contexts
  ⌈,,⌉ : ∀ Γ Γ' → ⌈ Γ ,, Γ' ⌉ ≡ ⌈ Γ ⌉ + ⌈ Γ' ⌉
  ⌈,,⌉ Γ ∅ = n≡n+0
  ⌈,,⌉ Γ (Γ' , x) = sn+m≡n+sm ∙ (app suc (⌈,,⌉ Γ Γ'))

  -- the length of a singleton context is 1
  ⌈∅,α⌉≡1 : ∀ {α} → ⌈ ∅ , α ⌉ ≡ 1
  ⌈∅,α⌉≡1 = refl

  -- the length of a context made from a k-tuple of variables is k
  ⌈⟦k-tuple⟧⌉≡k : ∀ {k} (αs : tuple var k) → ⌈ ⟦ αs ⟧ ⌉ ≡ k
  ⌈⟦k-tuple⟧⌉≡k [||] = refl
  ⌈⟦k-tuple⟧⌉≡k (α ¦ αs) = (app suc (⌈⟦k-tuple⟧⌉≡k αs)) ∙ (⌈,,⌉ (∅ , α) ⟦ αs ⟧)

  -- make a tuple of variables from a context
  tuple-from-context : ∀ Γ → tuple var ⌈ Γ ⌉
  tuple-from-context ∅ = [||]
  tuple-from-context (Γ , α) = insert-last α (tuple-from-context Γ)

In order to perform substitution in a correctly formed type expression, we need to keep track of the variables appearing in the expression. We do so by keeping track of where the variable is located in the context. In other words, we use an indexing system à la de Bruijn.

  data _∋_ : context → var → Set where
    ∋-last : ∀ {α : var} {Γ : context} → ((Γ , α) ∋ α)  -- either a variable is the last one is the context 
    ∋-rec : ∀ {α β : var} {Γ : context} → (Γ ∋ α) → ((Γ , β) ∋ α)  -- or it is in the first part of the context

The way we handle membership of variables in a context implies that there is no repetition of variables, or more precisely that a repeated variable in a context will be treated independently from its previous occurrence. For example, given the type expression α × α in the context α , α, if the first occurrence of α is justified by ∋-last while the second is justified by ∋-rec ∋-last, then the type expression is in effect the same as β × α in the context α , β. For this reason, and to avoid confusion, we always use contexts whose elements are pairwise distinct. Notice that we don’t enforce this rule through Agda, but instead trust the user to follow this guideline.

We define now functions to weaken contexts.

  -- weaken context with one new variable on the right
  weakenr-context : ∀ {Γ α β} → Γ ∋ α → (Γ , β) ∋ α
  weakenr-context = ∋-rec

  -- weaken context with a whole new context on the right
  weakenr-context-with-context : ∀ {Γ Γ' α} → Γ ∋ α → (Γ ,, Γ') ∋ α
  weakenr-context-with-context {Γ' = ∅} Γ∋α = Γ∋α
  weakenr-context-with-context {Γ' = Γ' , x} Γ∋α = weakenr-context (weakenr-context-with-context {Γ' = Γ'} Γ∋α)

  -- weaken context with one new variable on the left
  weakenl-context :
    ∀ {Γ} {α β}
    → Γ ∋ α → ((∅ , β) ,, Γ) ∋ α
  weakenl-context ∋-last = ∋-last
  weakenl-context (∋-rec Γ∋α) = ∋-rec (weakenl-context Γ∋α)

  -- weaken context with a whole new context on the left
  weakenl-context-with-context :
    ∀ {Γ Γ'} {α}
    → Γ ∋ α → (Γ' ,, Γ) ∋ α
  weakenl-context-with-context ∋-last = ∋-last
  weakenl-context-with-context (∋-rec Γ∋α) = ∋-rec (weakenl-context-with-context Γ∋α)

  -- spot the first variable
  ∋-first :
    ∀ {α Γ} →((∅ , α) ,, Γ) ∋ α
  ∋-first {Γ = ∅} = ∋-last
  ∋-first {Γ = Γ , x} = ∋-rec ∋-first
  
open context-handling public

Before we can define our type calculus properly, we need to define general constructions on families of dependent types. Given a list [x₁,…,xₙ] of elements of type A and a type family B over A, the type foreach B [x₁,…,xₙ] comprises elements that are dependent sequences (p₁,…,pₙ) of elements pᵢ in B(xᵢ). The construction foreach-tuple performs the analogous operation for tuples instead of lists.

foreach : ∀ {A : Set} (B : A → Set) → List A → Set
foreach B [] = ⊤
foreach B (x ∷ xs) = (B x) × (foreach B xs)

foreach-tuple : ∀ {k} {A : Set} (B : A → Set) → tuple A k → Set
foreach-tuple B [||] = ⊤
foreach-tuple B (x ¦ xs) = (B x) × (foreach-tuple B xs)

These new types come together with their own associated map functions.

map-foreach :
  ∀ {A A' : Set} {B : A → Set} {B' : A' → Set} {xs : List A} {g : A → A'}
  → (∀ {x} → B x → B' (g x)) → foreach B xs  
  → (List A') × foreach B' (map g xs)
map-foreach {xs = []} _ _ = [] , ∗
map-foreach {xs = x ∷ xs} {g = g} f (fst , rest) =
  let gxs , frest =  map-foreach f rest in (g x ∷ gxs) , f fst , frest

map-foreach-tuple :
  ∀ {k} {A A' : Set} {B : A → Set} {B' : A' → Set} {xs : tuple A k} {g : A → A'}
  → (∀ {x} → B x → B' (g x)) → foreach-tuple B xs  
  → (tuple A' k) × foreach-tuple B' (tuple-map g xs)
map-foreach-tuple {xs = [||]} _ _ = [||] , ∗
map-foreach-tuple {xs = x ¦ xs} {g = g} f (fst , rest) =
  let gxs , frest =  map-foreach-tuple f rest in (g x ¦ gxs) , f fst , frest

-- the version of map-foreach-tuple for which the underlying function g is id
-- needed since Agda cannot normalize tuple-map id xs to xs 
map-foreach-tuple-over-id :
  ∀ {k} {A : Set} {B B' : A → Set} {xs : tuple A k}
  → (∀ {x} → B x → B' x) → foreach-tuple B xs  
  → foreach-tuple B' xs
map-foreach-tuple-over-id {xs = [||]} _ _ = ∗
map-foreach-tuple-over-id {xs = x ¦ xs} f (fst , rest) = (f fst) , map-foreach-tuple-over-id f rest

We will also need these helper functions in the rest of the file:

-- fold with for foreach-tuples
foreach-tuple-zip-fold-with :
 ∀ {k} {A A' : Set} {B : A → Set} {B' : A' → Set} {C : Set} {xs : tuple A k} {xs' : tuple A' k}
  → (∀ {x x'} → B x → B' x' → C → C) → C → foreach-tuple B xs → foreach-tuple B' xs'
  → C
foreach-tuple-zip-fold-with {xs = [||]} {xs' = [||]} f acc ∗ ∗ = acc
foreach-tuple-zip-fold-with {xs = x ¦ xs} {xs' = x' ¦ xs'} f acc (fst , rest) (fst' , rest') = 
  foreach-tuple-zip-fold-with f (f fst fst' acc) rest rest'

-- remove the last element of a dependent sequence
cut-last-foreach-tuple :
  ∀ {k} {A : Set} {B : A → Set} {xs : tuple A (suc k)}
   → foreach-tuple B xs → foreach-tuple B (cut-last xs)
cut-last-foreach-tuple {xs = _ ¦ [||]} _ =  ∗
cut-last-foreach-tuple {xs = _ ¦ _ ¦ _} (fst , rest) = fst , cut-last-foreach-tuple rest

-- extend a dependent sequence by the given element
insert-last-foreach-tuple :
  ∀ {k} {A : Set} {B : A → Set} {xs : tuple A k} {x : A} (b : B x) 
   → foreach-tuple B xs → foreach-tuple B (insert-last x xs)
insert-last-foreach-tuple {xs = [||]} b _ = b , ∗ 
insert-last-foreach-tuple {xs = _ ¦ _} b (fst , rest) = fst , insert-last-foreach-tuple b rest

-- create the constant dependent sequence with given value over a constant tuple 
dummy-foreach-tuple :
  ∀ k {A : Set} {B : A → Set} (x : A) (b : B x)
  → foreach-tuple B (dummy-tuple k x)
dummy-foreach-tuple 0 x b = ∗
dummy-foreach-tuple (suc k) x b = b , dummy-foreach-tuple k x b

We need to be able to pass back and forth between a foreach-tuple (p₁,…,pₙ) over [x₁,…,xₙ] and its tuple of elements, by which we mean the tuple whose iᵗʰ cell is the dependent pair (xᵢ,pᵢ).

-- return the tuple of elements of a foreach-tuple
elt-foreach-tuple :
   ∀ {k} {A : Set} {B : A → Set} {xs : tuple A k}
   → foreach-tuple B xs → tuple (Σ A B) k
elt-foreach-tuple {xs = [||]} ∗ = [||]
elt-foreach-tuple {xs = x ¦ _} (fst , rest) = (x , fst) ¦ elt-foreach-tuple rest

-- return the foreach-tuple of a tuple of dependent pairs
foreach-tuple-from-tuple :
   ∀ {k} {A : Set} {B : A → Set} 
   → ∀ (xs : tuple (Σ A B) k) → foreach-tuple B (tuple-map proj₁ xs)  
foreach-tuple-from-tuple [||] = ∗
foreach-tuple-from-tuple ((_ , b) ¦ xs) = b , foreach-tuple-from-tuple xs

-- return the list of dependent pairs (xᵢ,yᵢ) in Σ A B such that (y₁,…,yₙ) is 
-- the element of foreach B [x₁,…,xₙ] given as input 
elt-foreach :
   ∀ {A : Set} {B : A → Set} {xs : List A}
   → foreach B xs → List (Σ A B)
elt-foreach {xs = []} ∗ = []
elt-foreach {xs = x ∷ _} (fst , rest) = (x , fst) ∷ elt-foreach rest

-- map function for foreach-tuples when the function to be mapped is a dependent function
dmap-foreach-tuple :
  ∀ {k} {A A' : Set} {B : A → Set} {B' : A' → Set} {xs : tuple A k} {g : ∀ {x} → B x → A'}
  → (∀ {x} (b : B x) → B' (g {x} b)) → ∀ (bs : foreach-tuple B xs)  
  → foreach-tuple B' (tuple-map (λ where (x , b) → g {x} b) (elt-foreach-tuple bs))
dmap-foreach-tuple {xs = [||]} _ _ = ∗
dmap-foreach-tuple {xs = x ¦ xs} f (fst , rest) = (f fst) , dmap-foreach-tuple f rest

Now we can define the rules of the calculus defining the correctly formed types. It comprises two mutually recursive types written in judgment-style. The turnstile ⊢ takes two contexts on its left, one of type variables and the other of type constructors variables, and allows a type expression on the right. The turnstile ⊢ᶜ takes the same kinds of contexts of the left, but admits a data constructor definition on the right. To guide the reader, we suggest reading Γ ∥ χ ⊢ φ as “the type of justifications of φ in type context Γ and TC-context χ”.

We adopt the following convention: type expressions will be denoted by variables by small (Greek) letters, while their justifications will be prepended by the symbol ⊢. For example, for a type expression φ, the elements of the type Γ ∥ χ ⊢ φ will typically be denoted ⊢φ. When the type context Γ of the justification of φ is of importance, we will use Γ⊢φ instead of ⊢φ to signify that. A typical use-case will be when weakening the context: if we have a type expression φ with justification in type context Γ, then we will use Γ⊢φ to refer to it. We will similarly use Γ,α⊢φ to refer to the induced justification in the extended context. We will reserve the letter Γ for type contexts, and the letter χ for TC-contexts. Small Greek letters from the beginning of the alphabet (α , β , γ , …) will typically denote type variables, whereas φ , ψ , σ, ζ will typically denote type expressions.

module type-calculus {var : Set} where
  type-context = context {var}
  TC-context = context {Σ ℕ TC-var}

  interleaved mutual
    data _∥_⊢_ : type-context → TC-context → type-expr → Set 
    data _∥_⊢ᶜ_ : ∀ {k} → type-context → TC-context → data-constructor k → Set

    data _∥_⊢_ where
      0-intro : ∀ {Γ χ} → Γ ∥ χ ⊢ 0ᵀ  -- justification of 0
      1-intro : ∀ {Γ χ} → Γ ∥ χ ⊢ 1ᵀ  -- justification of 1
      var-intro : ∀ {Γ χ} {α} → (Γ ∋ α) → Γ ∥ χ ⊢ (varᵀ α) -- justification of a projection to a variable
      ×-intro : ∀ {Γ χ G H} → (Γ ∥ χ ⊢ G) → (Γ ∥ χ ⊢ H) → Γ ∥ χ ⊢ (G ×ᵀ H) -- justification of a product
      +-intro : ∀ {Γ χ G H} → (Γ ∥ χ ⊢ G) → (Γ ∥ χ ⊢ H) → Γ ∥ χ ⊢ (G +ᵀ H) -- justification of a sum
      app-intro : -- justification of an application of a currently defined data type
        ∀ {Γ χ} {k} {G : TC-var k}
        → ∀ {φs} → foreach-tuple (λ φ → Γ ∥ χ ⊢ φ) φs
        → (χ ∋ (k , G)) → Γ ∥ χ ⊢ (appᵀ G [ φs ])
      data-intro : ---- justification of an application of a previously defined data type
        ∀ {Γ χ} {k} {G : TC-var k}
        → ∀ {Γcs χcs cs} → foreach (λ (c , Γc , χc) → Γc ∥ χc ⊢ᶜ c) (zip cs (zip Γcs χcs))
        → ∀ {φs} → foreach-tuple (λ φ → Γ ∥ χ ⊢ φ) φs
        → Γ ∥ χ ⊢ data-typeᵀ (dataᵀ G whereᵀ cs) [ φs ]

    data _∥_⊢ᶜ_ where
      dcᵀ-intro : -- justification of the definition of a data constructor
        ∀ {Γ χ c k G}
        → ∀ {Fs} → foreach (λ F → Γ ∥ (χ , (k , G)) ⊢ F) Fs
        → ∀ {Ks : tuple _ k} → foreach-tuple (λ K → Γ ∥ ∅ ⊢ K) Ks
        → Γ ∥ χ ⊢ᶜ (c ∷ Fs ⇒ᵀ Ks)

The type Γ ∥ χ ⊢ᶜ (c ∷ Fs ⇒ᵀ Ks) should be understood as the type of justifications of the constructor c in the given contexts. Notice how it comprises justifications of the domain of its arguments (the Fs) in the TC context extended by G, and justifications of the types at which the instance of G is defined (the Ks) in the empty TC context. This is important: we don’t want to allow any non-previously defined data types among the Ks. In particular, G itself should not appear in the Ks.

We use the following helper functions to recover the implicit arguments of an element of Γ ∥ χ ⊢ φ.

  extract-context :  ∀ {Γ χ φ} → Γ ∥ χ ⊢ φ → context
  extract-context {Γ} _ = Γ
  
  extract-TC-context :  ∀ {Γ χ φ} → Γ ∥ χ ⊢ φ → TC-context
  extract-TC-context {χ = χ} _ = χ

  extract-type-expr :  ∀ {Γ χ φ} → Γ ∥ χ ⊢ φ → type-expr
  extract-type-expr {φ = φ} _ = φ

  both : ∀ {Γ χ φ} → Γ ∥ χ ⊢ φ → Σ type-expr (λ ψ → Γ ∥ χ ⊢ ψ)
  both ⊢φ = extract-type-expr ⊢φ , ⊢φ

We can now define substitution on types Γ ∥ χ ⊢ φ. It will be crucial in the main function adm to be able to instantiate a type expression at other given type expressions.

  -- return the substitution φ[xs] in the type expression φ of the
  -- variables in its context Γ by the (justified) type expressions xs
  {-# NON_TERMINATING #-}
  _[_] :
    ∀ {Γ χ} {Γ'} {φ} {xs : tuple type-expr ⌈ Γ ⌉}
    → Γ ∥ χ ⊢ φ → foreach-tuple (λ x → Γ' ∥ χ ⊢ x) xs
    → Σ type-expr (λ φ[xs] → Γ' ∥ χ ⊢ φ[xs])

  -- constant types do not contain variables, so substitution is neutral
  0-intro [ _ ] = 0ᵀ , 0-intro 
  1-intro [ _ ] = 1ᵀ , 1-intro 
  
  -- α₁,…,αₙ ⊢ αᵢ instantiated at x₁,…,xₙ is simply xᵢ
  var-intro ∋-last [ ⊢xs ] = (elt-foreach-tuple ⊢xs) [-1]  -- the notation [-1] returns the last element of a tuple
  var-intro {χ = χ} (∋-rec Γ∋α) [ ⊢xs ] =  (var-intro {χ = χ} Γ∋α) [ cut-last-foreach-tuple ⊢xs ]

  -- substitution in a product (resp., sum) is the product (resp., sum) of the substitutions
  (×-intro ⊢φ₁ ⊢φ₂) [ ⊢xs ] =
    let φ₁[xs] ,  ⊢φ₁[xs] =  ⊢φ₁ [ ⊢xs ] in
    let φ₂[xs] ,  ⊢φ₂[xs] =  ⊢φ₂ [ ⊢xs ] in
    (φ₁[xs] ×ᵀ φ₂[xs] , ×-intro ⊢φ₁[xs] ⊢φ₂[xs])
  (+-intro ⊢φ₁ ⊢φ₂) [ ⊢xs ] =
    let φ₁[xs] ,  ⊢φ₁[xs] = ⊢φ₁ [ ⊢xs ] in
    let φ₂[xs] ,  ⊢φ₂[xs] = ⊢φ₂ [ ⊢xs ] in
    (φ₁[xs] +ᵀ φ₂[xs] , +-intro ⊢φ₁[xs] ⊢φ₂[xs])

  -- substitution in (either) application of a data type G is the application to the substitutions
  app-intro {G = G} ⊢φs χ∋G [ ⊢xs ] =
    both (app-intro (dmap-foreach-tuple (λ ⊢φ → let φ[xs] , ⊢φ[xs] = ⊢φ [ ⊢xs ] in ⊢φ[xs]) ⊢φs) χ∋G)
  data-intro {G = G} ⊢cs ⊢φs [ ⊢xs ] =
    both (data-intro {G = G} ⊢cs (dmap-foreach-tuple (λ ⊢φ → let φ[xs] , ⊢φ[xs] = ⊢φ [ ⊢xs ] in ⊢φ[xs]) ⊢φs))

We now define the justification of a type expression in a weakened context.

  -- weakening by a single variable on the right
  {-# NON_TERMINATING #-}  
  weakenr : ∀ {Γ χ} {φ} {β : var} → Γ ∥ χ ⊢ φ → (Γ , β) ∥ χ ⊢ φ
  weakenr 0-intro = 0-intro
  weakenr 1-intro = 1-intro
  weakenr (var-intro Γ∋α) = var-intro (weakenr-context Γ∋α)
  weakenr (×-intro ⊢φ₁ ⊢φ₂) = ×-intro (weakenr ⊢φ₁) (weakenr ⊢φ₂)
  weakenr (+-intro ⊢φ₁ ⊢φ₂) = +-intro (weakenr ⊢φ₁) (weakenr ⊢φ₂)
  weakenr (app-intro ⊢φs χ∋G) = app-intro (map-foreach-tuple-over-id weakenr ⊢φs) χ∋G 
  weakenr (data-intro ⊢cs ⊢φs) = data-intro ⊢cs (map-foreach-tuple-over-id weakenr ⊢φs)

  -- weakening by a whole context on the right
  {-# NON_TERMINATING #-}
  weakenr-with-context :
    ∀ {Γ Γ' χ} {φ : type-expr {var}} → (Γ ∥ χ ⊢ φ) → (Γ ,, Γ') ∥ χ ⊢ φ
  weakenr-with-context 0-intro = 0-intro
  weakenr-with-context 1-intro = 1-intro
  weakenr-with-context (var-intro Γ∋α) =  var-intro (weakenr-context-with-context Γ∋α)
  weakenr-with-context (×-intro ⊢φ₁ ⊢φ₂) = ×-intro (weakenr-with-context ⊢φ₁) (weakenr-with-context ⊢φ₂)
  weakenr-with-context (+-intro ⊢φ₁ ⊢φ₂) = +-intro (weakenr-with-context ⊢φ₁) (weakenr-with-context ⊢φ₂)
  weakenr-with-context (app-intro ⊢φs χ∋G) = app-intro (map-foreach-tuple-over-id weakenr-with-context ⊢φs) χ∋G 
  weakenr-with-context (data-intro ⊢cs ⊢φs) = data-intro ⊢cs (map-foreach-tuple-over-id weakenr-with-context ⊢φs)

  -- weakening by a single variable on the left of a variable introduction
  weakenl-var :
    ∀ {Γ} {χ} {α β : var}
    → Γ ∥ χ ⊢ varᵀ α
    → ((∅ , β) ,, Γ) ∥ χ ⊢ varᵀ α
  weakenl-var (var-intro Γ∋α) = var-intro (weakenl-context Γ∋α)

  -- weakening by a whole context on the left
  {-# NON_TERMINATING #-}
  weakenl-with-context :
    ∀ {Γ Γ' χ} {φ} → Γ ∥ χ ⊢ φ → (Γ' ,, Γ) ∥ χ ⊢ φ
  weakenl-with-context 0-intro = 0-intro
  weakenl-with-context 1-intro = 1-intro
  weakenl-with-context (var-intro Γ∋α) =  var-intro (weakenl-context-with-context Γ∋α)
  weakenl-with-context (×-intro ⊢φ₁ ⊢φ₂) = ×-intro (weakenl-with-context ⊢φ₁) (weakenl-with-context ⊢φ₂)
  weakenl-with-context (+-intro ⊢φ₁ ⊢φ₂) = +-intro (weakenl-with-context ⊢φ₁) (weakenl-with-context ⊢φ₂)
  weakenl-with-context (app-intro ⊢φs χ∋G) = app-intro (map-foreach-tuple-over-id weakenl-with-context ⊢φs) χ∋G 
  weakenl-with-context (data-intro ⊢cs ⊢φs) = data-intro ⊢cs (map-foreach-tuple-over-id weakenl-with-context ⊢φs)

  -- provide justifications of each of the variables in the context made out the given tuple of variables
  vars-in-context :
    ∀ {k} {χ}
    → ∀ (αs : tuple var k)
    → (foreach-tuple (λ α → ⟦ αs ⟧ ∥ χ ⊢ varᵀ α) αs)
  vars-in-context [||] = ∗
  vars-in-context {χ = χ} (α ¦ αs) =
    var-intro ∋-first , map-foreach-tuple-over-id weakenl-var (vars-in-context αs)

  -- weakening the TC context on the right by a single variable
  {-# NON_TERMINATING #-}
  weakenr-TC-var :
    ∀ {Γ χ G} {φ} → Γ ∥ χ ⊢ φ → Γ ∥ (χ , G) ⊢ φ
  weakenr-TC-var 0-intro = 0-intro
  weakenr-TC-var 1-intro = 1-intro
  weakenr-TC-var (var-intro x) = var-intro x
  weakenr-TC-var (×-intro ⊢φ₁ ⊢φ₂) = ×-intro (weakenr-TC-var ⊢φ₁) (weakenr-TC-var ⊢φ₂)
  weakenr-TC-var (+-intro ⊢φ₁ ⊢φ₂) = +-intro (weakenr-TC-var ⊢φ₁) (weakenr-TC-var ⊢φ₂)
  weakenr-TC-var (app-intro ⊢φs χ∋G) = app-intro (map-foreach-tuple-over-id weakenr-TC-var ⊢φs) (∋-rec χ∋G)
  weakenr-TC-var (data-intro ⊢cs ⊢φs) = data-intro ⊢cs (map-foreach-tuple-over-id weakenr-TC-var ⊢φs)

  -- weakening the TC context on the right by a whole TC context
  {-# NON_TERMINATING #-}
  weakenr-TC-context :
    ∀ {Γ χ χ'} {φ} → Γ ∥ χ ⊢ φ → Γ ∥ (χ ,, χ') ⊢ φ
  weakenr-TC-context {χ' = ∅} ⊢φ = ⊢φ
  weakenr-TC-context {χ' = χ' , G} ⊢φ = weakenr-TC-var {G = G} (weakenr-TC-context {χ' = χ'} ⊢φ)

  -- weakening the TC context on the left by a whole TC context
  {-# NON_TERMINATING #-}
  weakenl-TC-context :
    ∀ {Γ χ χ'} {φ} → Γ ∥ χ ⊢ φ → Γ ∥ (χ' ,, χ) ⊢ φ
  weakenl-TC-context 0-intro = 0-intro
  weakenl-TC-context 1-intro = 1-intro
  weakenl-TC-context (var-intro x) = var-intro x
  weakenl-TC-context (×-intro ⊢φ₁ ⊢φ₂) = ×-intro (weakenl-TC-context ⊢φ₁) (weakenl-TC-context ⊢φ₂)
  weakenl-TC-context (+-intro ⊢φ₁ ⊢φ₂) = +-intro (weakenl-TC-context ⊢φ₁) (weakenl-TC-context ⊢φ₂)
  weakenl-TC-context (app-intro ⊢φs χ∋G) = app-intro (map-foreach-tuple-over-id weakenl-TC-context ⊢φs) (weakenl-context-with-context χ∋G)
  weakenl-TC-context (data-intro ⊢cs ⊢φs) = data-intro ⊢cs (map-foreach-tuple-over-id weakenl-TC-context ⊢φs)
  
open type-calculus public

Up to now, our constructions have been done over a set var of variables, that can be instantiated to different kind of variables. We now define such instances.

We need first a set of type variables, each of them identified by a label (here an element of ℕ). We also define functions whose purpose is to make variables which are fresh relative to a given tuple.

id-type-var = ℕ
type-var = id-type-var -- interface to the identifiers

-- create a fresh natural number out of a tuple by returning the successor of the maximum 
fresh-ℕ : ∀ {k} → tuple ℕ k → ℕ
fresh-ℕ xs =
  suc (find-max xs 0)
  where
    max : ℕ → ℕ → ℕ
    max zero m = m
    max (suc n) zero = suc n
    max (suc n) (suc m) = suc (max n m)
    
    find-max : ∀ {k} → tuple ℕ k → ℕ → ℕ
    find-max [||] n = n
    find-max (x ¦ xs) zero = find-max xs x
    find-max (zero ¦ xs) n+1@(suc n) = find-max xs n+1
    find-max (suc x ¦ xs) (suc n) = find-max xs (suc (max x n))

-- interface for type-var
fresh-type-var : ∀ {k} → tuple type-var k → type-var
fresh-type-var = fresh-ℕ 

-- make a whole fresh tuple of variables
make-distinct-tuple : ∀ {var : Set} {m} → tuple var m → (∀ {k} → tuple var k → var) → ∀ n → tuple var n
make-distinct-tuple xs f zero = [||]
make-distinct-tuple xs f (suc n) = let new = f xs in new ¦ make-distinct-tuple (new ¦ xs) f n

Next we need to define a set of function variables. We want to be just a bit more cautious with function variables: since they will be used to express the set of constraints that adm returns, we want to carefully track a state specifying which function variables have already been used. By tracking this state in the various recursive calls to adm, we can ensure that fresh function variables are produced.

id-fun-var = ℕ  -- identifiers for function variables
fun-var = id-fun-var  -- interface to function variables

fresh-id-fun-var : id-fun-var → id-fun-var  -- function creating the next fresh identifier
fresh-id-fun-var = suc

record state (id : Set) (fresh : id → id) : Set where  -- generic type of states
  field
    curr : id
fun-var-state = state id-fun-var fresh-id-fun-var  -- interface to the state tracking function variables


-- return a tuple with pairwise distinct elements, all of which are fresh relative to the argument tuple, by keeping track of the function variable state
make-fresh-tuple : ∀ {id fresh} (k : ℕ) → state id fresh → tuple id k × state id fresh 
make-fresh-tuple zero s = [||] , s
make-fresh-tuple {fresh = fresh} (suc n) s =
  let (ids , s') = make-fresh-tuple n (record { curr = fresh (state.curr s) }) in
  state.curr s ¦ ids , s'

We now craft a type of variables that can be either a type variable or a function variable. This is done in order to be able to represent a substitution of the form Σ[φs] when Σ is a type expression with variable of type type-var and the φs are type expressions with variables of type fun-var. For a way to avoid this intermediate set of variables mix-var, see the list of improving ideas at the end of the file.

data mix-var : Set where
  fvar : fun-var → mix-var
  tvar : type-var → mix-var

-- version of fresh-type-var within mix-var
fresh-tvar-mix-var : ∀ {k} → tuple mix-var k → mix-var
fresh-tvar-mix-var tvars = tvar (fresh-type-var (tuple-map (λ {(tvar id) → id ; _ → 0}) tvars))

-- boolean equality for elements of mix-var. The decidability of equality in the type of identifiers (ℕ here) is crucial here.
mix-var-bool-= : mix-var → mix-var → Bool
mix-var-bool-= (fvar i) (fvar j) = ⌊ i ≟ j ⌋
mix-var-bool-= (tvar i) (tvar j) = ⌊ i ≟ j ⌋
mix-var-bool-= _ _ = false

The algorithm adm acts on terms of a given type in a certain specification. So we need to encode the syntax of our terms next. We only deal with closed terms, since the presence of open terms is not relevant to the algorithm adm. A term is either ∗ in the type 1ᵀ, or an inl or an inr in a sum type, or a pair in a product, or a term constructed by a data constructor of one of the user-defined data types of our language.

module term-calculus where

  data term-expr : Set where
    ∗ᵗ : term-expr
    inl inr : term-expr → term-expr
    _,_ : term-expr → term-expr → term-expr
    dc : ∀ {k} (c : data-constructor {mix-var} k) → tuple term-expr (data-constructor-term-arity c)  → term-expr
    
open term-calculus public

We now give definitions relative to the constraint and assignments presented in the algorithm.

data constraint (var : Set) : Set where
  ⟨_,_⟩ : type-expr {var} → type-expr {var} → constraint var

data assignment (var : Set) {Γ Γ' : context {var}} {χ χ' : TC-context {var}} : Set where
  _≣_ : ∀ {φ φ'} → Γ ∥ χ ⊢ φ → Γ' ∥ χ' ⊢ φ' → assignment var


-- return the list of assignments obtained after top-unifying a given assignment
-- The *should not happen!*-cases should indeed not happen since we will only solve top-unifiable assignments.
{-# NON_TERMINATING #-}
solve-matching : ∀ {Γ Γ' χ χ'} → assignment mix-var {Γ} {Γ'} {χ} {χ'} → List (assignment mix-var {Γ} {Γ'} {χ} {χ'})

-- base cases: a variable is assigned to a type expression
solve-matching a@(var-intro _ ≣ _) = a ∷ []
solve-matching a@(_ ≣ var-intro _) = a ∷ []

-- peeling off the outermost constructor whenever possible
solve-matching (×-intro ⊢φ₁ ⊢φ₂ ≣ ×-intro ⊢φ₁' ⊢φ₂') = 
  solve-matching (⊢φ₁ ≣ ⊢φ₁') ++ solve-matching (⊢φ₂ ≣ ⊢φ₂')
solve-matching (+-intro ⊢φ₁ ⊢φ₂ ≣ +-intro ⊢φ₁' ⊢φ₂') =
  solve-matching (⊢φ₁ ≣ ⊢φ₁') ++ solve-matching (⊢φ₂ ≣ ⊢φ₂') 
solve-matching (data-intro {G = TC k G} ⊢cs ⊢φs ≣ data-intro {G = TC k' G'} ⊢cs' ⊢φs') with ⌊ G ≟ G' ⌋ ∧ ⌊ k ≟ k' ⌋
... | true = foldl (λ acc a → acc ++ solve-matching a) [] (zipWith (λ (_ , ⊢φ) (_ , ⊢φ') → ⊢φ ≣ ⊢φ')
        ([||]→[] (elt-foreach-tuple ⊢φs))
        ([||]→[] (elt-foreach-tuple ⊢φs')))
... | false = []  -- *should not happen!* 
solve-matching (app-intro {G = TC k G} ⊢φs χ∋G ≣ app-intro {G = TC k' G'} ⊢φs' χ∋G') with ⌊ G ≟ G' ⌋ ∧ ⌊ k ≟ k' ⌋
... | true = foldl (λ acc a → acc ++ solve-matching a) [] (zipWith (λ (_ , ⊢φ) (_ , ⊢φ') → ⊢φ ≣ ⊢φ')
        ([||]→[] (elt-foreach-tuple ⊢φs))
        ([||]→[] (elt-foreach-tuple ⊢φs')))
... | false = []  -- *should not happen!*
solve-matching _ = (0-intro ≣ 1-intro) ∷ []  -- *should not happen!*

We define a type that encloses the data needed for the full definition of a user-defined data type. Elements of that type will be carried over the different calls to adm to recall the user-defined data type already encountered during the process. In that way, when we encounter the name of a data type, we can look up this list of already-encountered data types to recover the associated constructors.

record recorded-data-type : Set where
  constructor arity_def_ctx_∥_der_
  field
   arity : ℕ
   def : user-defined {mix-var} arity
   type-ctxs : List (type-context {mix-var})
   TC-ctxs : List (TC-context {mix-var})
   der : foreach (λ (c , Γc , χc) → _∥_⊢ᶜ_ {k = arity} Γc χc c) (zip (user-defined-cs def) (zip type-ctxs TC-ctxs))

-- return the list of constaints [⟨σ₁,σⱼ⟩ : j ∈ {2,…,n}] when the input list is [σ₁,σ₂,…,σₙ].  
constraint-with-fst :
  ∀ {Γ χ}
  → List (Σ (type-expr {mix-var}) (λ σ → Γ ∥ χ ⊢ σ))
  → List (constraint mix-var)
constraint-with-fst [] = []
constraint-with-fst (_ ∷ []) = []
constraint-with-fst ((σ₁ , ⊢σ₁) ∷ (σ₂ , _) ∷ σs) = ⟨ σ₂ , σ₁ ⟩ ∷ (constraint-with-fst ((σ₁ , ⊢σ₁) ∷ σs))

We are now ready to implement the algorithm adm of the paper. For reasons specific to the implementation, adm takes more arguments than in the paper. We keep the same name as in the paper for the arguments that are common. We will also keep, as much as possible, the names of the various local variables in adm, with the exception that the tuples named with an overline in the paper are here marked with an ending ‘s’. For example, the tuple f̅ is written as fs in the algorithm. We will also indicate in comments the correspondence between a code excerpt and the steps of the algorithm in the paper. However, the correspondence is not perfect and sometimes a step of the paper is divided in the following code. The comments indicating the steps are thus to be taken more as an aid to reading the code than an exact match with the algorithm described in the paper.

Here is a high-level description of the explicit arguments (in order) of adm:

t is the term we want to map over.
⊢Φ is the justification of the specification Φ in which we are considering t.
fs is a tuple of functions for which adm will return constraints to be mappable over t
s is the state of function variables with which to start the algorithm in order to be sure to have fresh function variables when needed.
Gs is a list of already-encountered data types in the recorded-data-type format. The function adm return a list of constraints together with the new state of function variables.

The function adm is mutually recursively defined with handle which is basically a glorified switch case that performs the recursive calls to adm described in the paper. Described at a high level, the call handle t ⊢𝐷(ζ₁,…,ζₙ) ⊢gs s Gs, where 𝐷 ∈ {+,×} ∪ 𝒢, performs first the substitution of the gs in each type expression ζⱼ and then calls adm t ⊢𝐷(ζ₁,…,ζₙ) (ζ₁[gs],…,ζₙ[gs]) s Gs.

Another difference with the algorithm in the paper lies in the handling of the lengths of the various tuples involved. In the paper, some of these tuples have obviously the same length. Unfortunately, this fact can not always be derived by Agda, in particular when the lengths involved are not definitionally equal (that is, when Agda can’t normalize them to the same term). In these cases we have to guide Agda. In particular, when we use a transport over a path p : k ≡ k' of an element b in a type family B : ∀ {n : ℕ} → tuple A n → Set (that is, B is dependent over tuples of given type), the resulting element will typically be denoted b-corr (standing for corrected version of b).

{-# NON_TERMINATING #-}
adm :
  term-expr -- term we want to map over
  → ∀ {Γ χ} {Φ : type-expr {mix-var}} → Γ ∥ χ ⊢ Φ -- type expression the term should be regarded as an element of
  → tuple (type-expr {mix-var}) (outmost-arity Φ) -- function expressions to map over the term
  → fun-var-state -- current state for fresh function variables
  → List recorded-data-type
  -- return a list of constraints on the function expressions and the new current state
  → List (constraint mix-var) × fun-var-state 

-- Mutually recursive function to handle the recursive calls of adm
handle :
  term-expr -- term to call adm recursively on
  → ∀ {Γ Γ'} {χ} {Φ} → (Γ' ∥ χ ⊢ Φ) -- type expression the term should be regarded as an element of
  → ∀ {gs} → foreach-tuple {k = ⌈ Γ' ⌉} (λ v → Γ ∥ χ ⊢ v) gs -- function expressions to feed the recursive calls after substitution
  → fun-var-state -- current state for fresh function variables
  → List recorded-data-type -- list of user-defined data types already encountered
  -- return a list of constraints on the function expressions and the new current state
  → List (constraint mix-var) × fun-var-state

handle _ (var-intro x) _ s Gs = [] , s
handle t (×-intro {G = ζ₁} {H = ζ₂} ⊢ζ₁ ⊢ζ₂) ⊢gs s Gs =
  let ζ₁[gs] , _ = ⊢ζ₁ [ ⊢gs ] in
  let ζ₂[gs] , _ = ⊢ζ₂ [ ⊢gs ] in
  adm t (×-intro ⊢ζ₁ ⊢ζ₂) ( ζ₁[gs] ¦ ζ₂[gs] ¦ [||]) s Gs
handle t (+-intro {G = ζ₁} {H = ζ₂} ⊢ζ₁ ⊢ζ₂) ⊢gs s Gs =
  let ζ₁[gs] , _ = ⊢ζ₁ [ ⊢gs ] in
  let ζ₂[gs] , _ = ⊢ζ₂ [ ⊢gs ] in
  adm t (+-intro ⊢ζ₁ ⊢ζ₂) (ζ₁[gs] ¦ ζ₂[gs] ¦ [||]) s Gs
handle t D@(data-intro {k = k} {G = TC _ k} _ ⊢ζs) ⊢gs s Gs =
  adm t D (tuple-map (λ (_ , ⊢ζ) → proj₁ (⊢ζ [ ⊢gs ])) (elt-foreach-tuple ⊢ζs)) s Gs
handle t D@(app-intro ⊢ζs χ∋G) ⊢gs s Gs =
  adm t D (tuple-map (λ (_ , ⊢ζ) → proj₁ (⊢ζ [ ⊢gs ])) (elt-foreach-tuple ⊢ζs)) s Gs
handle _ 0-intro _ s _ = [] , s
handle _ 1-intro _ s _ = [] , s

-- handle built-in pairs: case A in the paper
adm (t₁ , t₂) {Γ} {χ} {Σ₁ ×ᵀ Σ₂} (×-intro {Γ = Γ} ⊢Σ₁ ⊢Σ₂) (f₁ ¦ f₂ ¦ [||] ) s Gs = 
  let (ids-gs , s') = make-fresh-tuple ⌈ Γ ⌉ s in  -- step A.(i)
  let gs-vars = vars-in-context (tuple-map fvar ids-gs) in 
  let _ , gs = map-foreach-tuple (λ ⊢α → ⊢α) gs-vars in
  let handle-t₁ , s₁ = (handle t₁ ⊢Σ₁ gs s' Gs) in  -- step A.(ii) for j=1
  let handle-t₂ , s₂ = (handle t₂ ⊢Σ₂ gs s₁ Gs) in  -- step A.(ii) for j=2
  let Σ₁[gs] , _ = ⊢Σ₁ [ gs ] in
  let Σ₂[gs] , _ = ⊢Σ₂ [ gs ] in
  ⟨ Σ₁[gs] , f₁ ⟩ ∷ ⟨ Σ₂[gs] , f₂ ⟩ ∷  handle-t₁ ++ handle-t₂ , s₂  -- step A.(iii)

-- handle built-in injections
-- inl: case B in the paper
adm (inl t) {Γ} {χ} {Σ₁ +ᵀ Σ₂} (+-intro {Γ = Γ} ⊢Σ₁ ⊢Σ₂) (f₁ ¦ f₂ ¦ [||] ) s Gs = 
  let (ids-gs , s') = make-fresh-tuple ⌈ Γ ⌉ s in  -- step B.(i)
  let gs-vars = vars-in-context (tuple-map fvar ids-gs) in
  let _ , gs = map-foreach-tuple (λ ⊢α → ⊢α) gs-vars in
  let handle-t , s'' = (handle t ⊢Σ₁ gs s' Gs) in -- step B.(ii)
  let Σ₁[gs] , _ = ⊢Σ₁ [ gs ] in
  let Σ₂[gs] , _ = ⊢Σ₂ [ gs ] in
  ⟨ Σ₁[gs] , f₁ ⟩ ∷ ⟨ Σ₂[gs] , f₂ ⟩ ∷  handle-t , s''  -- step B.(iii)

-- inr: case C of the paper
adm (inr t) {Γ} {χ} {Σ₁ +ᵀ Σ₂} (+-intro {Γ = Γ} ⊢Σ₁ ⊢Σ₂) (f₁ ¦ f₂ ¦ [||] ) s Gs = 
  let (ids-gs , s') = make-fresh-tuple ⌈ Γ ⌉ s in  -- step C.(i) 
  let gs-vars = vars-in-context (tuple-map fvar ids-gs) in
  let _ , gs = map-foreach-tuple (λ ⊢α → ⊢α) gs-vars in
  let handle-t , s'' = (handle t ⊢Σ₂ gs s' Gs) in  -- step C.(ii)
  let Σ₁[gs] , _ = ⊢Σ₁ [ gs ] in
  let Σ₂[gs] , _ = ⊢Σ₂ [ gs ] in
  ⟨ Σ₁[gs] , f₁ ⟩ ∷ ⟨ Σ₂[gs] , f₂ ⟩ ∷  handle-t , s''  -- step C.(iii)

We are now tackling case D of the paper. This is where the interesting constraints on morphisms can appear. The informal version in the paper works under the implicit assumption that we can recover the constructors of a data type merely from its name. This is a fair assumption when working in a high-level fashion. In contrast, the implementation of our language presented here needs extra care for calls to admissible where the specification Φ has the form 𝐷(ζ₁,…,ζₙ): the specification is indeed fairly different depending on whether the application of 𝐷 is extracted from the definition of a data constructor (that is, the application is a appᵀ name-of-𝐷 [ζ₁,…,ζₙ]) or the application of 𝐷 is the application of a previously completely defined data type (that is, the application is a data-typeᵀ full-definition-of-𝐷 [ζ₁,…,ζₙ]). These two cases should be both handled by case D of the paper, hence we just translate the former into the latter and treat only the latter according to case D.

-- handle expression of the form appᵀ G [ Σs ]. It searches for G in
-- the list Gs of already-encountered user-defined data types. G MUST
-- be in the list. Then it simply calls admissible on data-typeᵀ (dataᵀ
-- G whereᵀ cs) [ Σs ], where the cs is the list of data constructors
-- associated to G found in Gs.
adm
  t -- the term doesn't matter here, but it should be of the form `dc …`
  {Γ} {χ} {appᵀ G@(TC _ k) [ Σs ]}
  (app-intro {Γ = Γ} {χ} ⊢Σs χ∋G)
  fs s Gs =

  let arity k' def Gdef ctx _ ∥ _ der ⊢cs , k≡k' = lookup-data-type G Gs in  -- find G in Gs

  -- the arity k' of G' is equal to k, but we have to guide Agda to
  -- get the version of ⊢Σs over the correct size k'
  let _ , ⊢Σs-corr = trp k≡k' {B = λ n → Σ (tuple _ n) (λ xs → foreach-tuple _ xs)} (Σs , ⊢Σs) in
  -- same for fs
  let fs-corr = trp k≡k' {B = tuple type-expr} fs in
  adm t (data-intro {G = user-defined-name Gdef} ⊢cs ⊢Σs-corr) fs-corr s Gs

    where

    -- return the element in the input list whose field definition is `dataᵀ
    -- G' whereᵀ …` with G' equal to G, together with a proof of
    -- equality of the respective arities of G' and G.
    lookup-data-type :
      ∀ {k} → TC-var k → List recorded-data-type
      → Σ recorded-data-type (λ (arity k' def _ ctx _ ∥ _ der _) → k ≡ k') 
    lookup-data-type {k} G (head@(arity k' def (dataᵀ G' whereᵀ _) ctx _ ∥ _ der _) ∷ Gs) with k ≟ k'
    ... | false because _ = lookup-data-type G Gs
    ... | true because (ofʸ k≡k') = if ⌊ G ≟ᴳ G' ⌋ then (head , k≡k') else (lookup-data-type G Gs)
    -- should not happen
    lookup-data-type {k} G [] = arity k def (dataᵀ G whereᵀ []) ctx [] ∥ [] der ∗ , refl

-- handle user-defined data types: case D in the paper
adm
  (dc (c ∷ Fs ⇒ᵀ Ks) ts)
  {Γ} {χ} {data-typeᵀ (dataᵀ G@(TC _ k) whereᵀ cs) [ Σs ]}
  (data-intro {Γ = Γ} {χ = χ} {Γcs = Γcs} {χcs = χcs} ⊢cs ⊢Σs)
  fs s Gs = 

  -- we just encountered a (possibly) new data type, so we push it on the stack of the already-encountered ones. 
  let Gs-updated = (arity k def (dataᵀ G whereᵀ cs) ctx Γcs ∥ χcs der ⊢cs) ∷ Gs in -- 

  -- create the variables in βs in context
  let βs = tuple-from-context Γ in
  let Γβs = ⟦ βs ⟧ in let βs⊢βs-var = vars-in-context {χ = χ} βs in
  let βs-size-⌈Γβs⌉ = correct-size βs in 
  let _ , βs⊢βs = map-foreach-tuple {B' = λ Φ → Γβs ∥ χ ⊢ Φ} (λ ⊢α → ⊢α) βs⊢βs-var in

  -- create the fresh function variables in gs in context (step D.(i))
  let (ids-gs , s-after-gs) = make-fresh-tuple ⌈ Γβs ⌉ s in
  let Γgs = ⟦ tuple-map fvar ids-gs ⟧ in let gs-vars = vars-in-context {χ = χ} (tuple-map fvar ids-gs) in
  let gs , gs⊢gs = map-foreach-tuple {B' = λ Φ → Γgs ∥ χ ⊢ Φ} {g = varᵀ} (λ ⊢α → ⊢α) gs-vars in
  let gs⊢gs-corr = foreach-tuple-from-tuple (trp (⌈⟦k-tuple⟧⌉≡k βs) {B = tuple (Σ type-expr (λ Φ → Γgs ∥ χ ⊢ Φ))} (elt-foreach-tuple gs⊢gs)) in

  -- add new constraints to C (step D.(i))
  let C = [||]→[] (tuple-map (λ ((_ , ⊢Σ) , f) → ⟨ proj₁ (⊢Σ [ gs⊢gs-corr ]) , f ⟩) (tuple-zip (elt-foreach-tuple ⊢Σs) fs)) in


  -- look for the data constructor c in the list of data constructors associated to G
  let ( Gc , Γc , χc ) , (Fsc , ⊢Fsc) , (Ksc , ∅⊢Ksc) = lookup-dc {G = G} c ⊢cs in
  -- set the element of the tuple Ks in the correct context
  let ⊢Ksc = map-foreach-tuple-over-id (λ ⊢K → weakenl-TC-context {χ' = χ} ⊢K) ∅⊢Ksc in

  -- create the variables in γs in context 
  let γs = make-distinct-tuple βs fresh-tvar-mix-var ⌈ Γc ⌉ in
  let Γγs = ⟦ γs ⟧ in let γs⊢γs-var = vars-in-context {χ = ∅} (γs) in
  let γs-size-⌈Γγs⌉ = correct-size γs in
  let _ , γs⊢γs = map-foreach-tuple {B' = λ Φ → Γγs ∥ χ ⊢ Φ} (λ ⊢α → weakenl-TC-context ⊢α) γs⊢γs-var in

  -- consider each Σₗ in variables βs and each Kₗ in variables γs 
  let ⊢Σs[βs] = dmap-foreach-tuple {B' = λ Φ → Γβs ∥ χ ⊢ Φ} {g = λ {Σ} (⊢Σ : Γ ∥ χ ⊢ Σ) → proj₁ (⊢Σ [ βs⊢βs ])} (λ ⊢Σ → proj₂ (⊢Σ [ βs⊢βs ])) ⊢Σs in
  let ⊢Ksc[γs] = dmap-foreach-tuple {B' = λ Φ → Γγs ∥ χ ⊢ Φ} {g = λ {K} (⊢K : Γc ∥ χ ⊢ K) → proj₁ (⊢K [ γs⊢γs ])} (λ ⊢K → proj₂ (⊢K [ γs⊢γs ])) ⊢Ksc in

  -- create the system of matching problems of step D.(ii)
  let system = foreach-tuple-zip-fold-with (λ ⊢Σ[βs] ⊢K[γs] acc → ( ⊢Σ[βs] ≣  ⊢K[γs]) ∷ acc) [] ⊢Σs[βs] ⊢Ksc[γs] in
  -- solve the system to get the assignments in the form described in the last paragraph of step D.(ii)
  let assignments = foldl (λ acc a → acc ++ solve-matching {Γ = Γβs} {Γ' = Γγs} a) [] system in 

  -- make a pass on the list of assignments to sort them into the tuples called ψs and σs in case D (these are tuples of lists of type expressions)
  let ψs , σs = sort-assignments {Γ = Γβs} {Γ' = Γγs} assignments βs-size-⌈Γβs⌉ γs-size-⌈Γγs⌉ (dummy-tuple ⌈ ⟦ βs ⟧ ⌉ []) (dummy-tuple ⌈ ⟦ γs ⟧ ⌉ []) in

  -- helping functions
  let βs→βs,γs = λ Φ (⊢Φ : Γβs ∥ χ ⊢ Φ) → weakenr-with-context {Γ = Γβs} {Γ' = Γγs} {χ = χ} {φ = Φ} ⊢Φ in  -- weakening on the right by γs
  let γs→βs,γs = λ Φ (⊢Φ : Γγs ∥ χ ⊢ Φ) → weakenl-with-context {Γ = Γγs} {Γ' = Γβs} {χ = χ} {φ = Φ} ⊢Φ in  -- weakening on the left by βs

  -- put the type expressions in each of the σᵢ in the context βs,γs
  let βs,γs⊢σs = tuple-map {B = List (Σ type-expr (λ Φ → (Γβs ,, Γγs) ∥ χ ⊢ Φ))} (map (λ (σ , ⊢σ) → σ , βs→βs,γs σ ⊢σ)) σs in
  -- put each variable γᵢ in context βs,γs (with corrected size when needed)
  let βs,γs⊢γs-off = tuple-map (λ (γ , ⊢γ) → γ , γs→βs,γs γ ⊢γ) (elt-foreach-tuple γs⊢γs) in
  let βs,γs⊢γs = dcorrect-size {B = λ {n} γs → tuple (Σ type-expr (λ Φ → (Γβs ,, Γγs) ∥ χ ⊢ Φ)) n} {αs = γs} βs,γs⊢γs-off in

  -- create the elements of τs of step D.(iii)
  let τs-off = tuple-zip-with (λ {_ (σ ∷ σi) → σ ; γ [] → γ}) βs,γs⊢γs βs,γs⊢σs in
  let τs-tuple = trp (⌈⟦k-tuple⟧⌉≡k γs) {B = tuple (Σ type-expr (λ Φ → _ ∥ χ ⊢ Φ))} τs-off in
  let ⊢τs = foreach-tuple-from-tuple τs-tuple in

  -- create the fresh function variables in hs (step D.(iv))
  let ids-hs , s-after-hs = make-fresh-tuple ⌈ Γγs ⌉ s-after-gs in
  let Γhs = ⟦ tuple-map fvar ids-hs ⟧ in let hs-vars = vars-in-context {χ = χ} (tuple-map fvar ids-hs) in
  let hs , hs⊢hs = map-foreach-tuple {B' = λ Φ → Γhs ∥ χ ⊢ Φ} (λ ⊢α → ⊢α) hs-vars in

  -- add the constraints of step D.(v) 
  let hs⊢ψs[hs] = tuple-map (map (λ (_ , ⊢ψ) → ⊢ψ [ hs⊢hs ] )) ψs in
  let Cψs = tuple-zip-with (λ ψi g → map (λ (ψ , ⊢ψ) → ⟨ ψ , g ⟩) ψi) hs⊢ψs[hs] gs in

  -- add the constraints of step D.(vi)
  let gs⊢σs[gs] = tuple-map (map (λ (_ , ⊢σ) → _[_] {Γ' = Γgs} ⊢σ gs⊢gs )) σs in
  let Cσs = tuple-map constraint-with-fst gs⊢σs[gs] in
  
  -- create the proof ⊢g and ⊢h for each g and h in the context gs,hs (with corrected size when needed)
  let gs,hs⊢gs = map-foreach-tuple-over-id (weakenr-with-context {Γ' = Γhs}) gs⊢gs in
  let gs,hs⊢hs = map-foreach-tuple-over-id (weakenl-with-context {Γ' = Γgs}) hs⊢hs in
  let gs,hs⊢gs,hs-off = (elt-foreach-tuple gs,hs⊢gs ⊕⊕ elt-foreach-tuple gs,hs⊢hs) in
  let gs,hs⊢gs,hs = foreach-tuple-from-tuple (trp ((⌈,,⌉ Γβs Γγs) ⁻¹) {B = tuple (Σ type-expr (λ Φ → (Γgs ,, Γhs) ∥ χ ⊢ Φ))} gs,hs⊢gs,hs-off) in
  
  -- compute each Rⱼ in step D.(vii)
  let ⊢Rs = map (λ (_ , ⊢F) → (weakenl-TC-context {χ' = χ} ⊢F) [ map-foreach-tuple-over-id (weakenr-TC-context {χ' = (χc , (k , Gc))}) ⊢τs ]) (elt-foreach ⊢Fsc) in

  -- make each of the recursive calls of step D.(vii) through handle
  let handle-ts-s'' = foldl (λ (acc , curr) (t , (R , ⊢R)) → let Cₜ , next = handle t ⊢R (map-foreach-tuple-over-id weakenr-TC-context gs,hs⊢gs,hs) curr Gs-updated in (acc ++ Cₜ) , next) (C , s-after-hs) (zip ([||]→[] ts) ⊢Rs) in

  -- collect all of the constraints obtained in step D.(vii) and add them to C before returning it (step D.(viii)) 
  (foldl (λ acc elt → acc ++ elt) [] (([||]→[] Cψs) ++ ([||]→[] Cσs))) ++ proj₁ handle-ts-s'' , proj₂ handle-ts-s'' 
    where

    -- return the exact same tuple as the input but considered with modified length
    correct-size : ∀ {k} (αs : tuple mix-var k) → tuple mix-var ⌈ ⟦ αs ⟧ ⌉
    correct-size αs = trp ((⌈⟦k-tuple⟧⌉≡k αs) ⁻¹) {B = tuple mix-var} αs

    -- same but for elements of a family dependent on tuples of type mix-var
    dcorrect-size :
      ∀ {k} {B : ∀ {n} → tuple mix-var n → Set} {αs : tuple mix-var k}
      → B αs
      → B (correct-size αs)
    dcorrect-size {B = B} {αs = αs} b = trp (≡Σ←Σ≡ (((⌈⟦k-tuple⟧⌉≡k αs) ⁻¹) , refl)) {B = λ (n , αs) → B {n} αs} b

    -- look for the input identifier in a given list of data
    -- constructors and return its associated data, namely, the
    -- identifier itself, the type expressions in its domain, and the 
    -- type expressions in its codomain. The identifier MUST be present.
    lookup-dc :
      ∀ {k} {G : TC-var k} → id-data-constructor
      → ∀ {Γcs χcs} {cs :  List (data-constructor {mix-var} k)} → foreach (λ (c , Γc , χc) → Γc ∥ χc ⊢ᶜ c) (zip cs (zip Γcs χcs))
      →
        Σ (TC-var k × type-context {mix-var} × TC-context {mix-var})
        (λ (G' , Γc , χc) → 
          Σ (List type-expr) (λ Fs → foreach (λ F → Γc ∥ (χc , (k , G')) ⊢ F) Fs)
          ×
          Σ (tuple type-expr k) (λ Ks → foreach-tuple (λ K → Γc ∥ ∅ ⊢ K) Ks)
        )
    lookup-dc {k} {G} c {Γc' ∷ _} {χc' ∷ _} {(c' ∷ _ ⇒ᵀ _) ∷ _} ((dcᵀ-intro {G = G'} {Fs = Fsc'} ⊢Fsc' {Ks = Ksc'} ⊢Ksc') , ⊢cs) =
      if ⌊ c ≟ c' ⌋ ∧ ⌊ G ≟ᴳ G' ⌋ then (G' , Γc' , χc') , (Fsc' , ⊢Fsc') , (Ksc' , ⊢Ksc')
      else lookup-dc {G = G} c ⊢cs
    lookup-dc {k} _ _ =
      (TC 0 k , ∅ , ∅) , ([] , ∗) , (dummy-tuple k 0ᵀ , dummy-foreach-tuple k 0ᵀ 0-intro)  -- default, should not happen

    -- return the tuple given as first argument where the position
    -- corresponding to the first occurrence of the third argument in
    -- the tuple given as second argument has been updated according
    -- to the function in fourth argument; the boolean equality to find
    -- the first occurrence is determined by the function given in
    -- fifth argument
    lookup&update : ∀ {A B : Set} {k} → tuple A k → tuple B k → B → (A → A) → (B → B → Bool) → tuple A k
    lookup&update [||] [||] _ _ _ = [||]
    lookup&update (x ¦ datas) (i ¦ indexs) i' update _?=_ with i ?= i'
    ... | true = (update x) ¦ datas
    ... | false = x ¦ (lookup&update datas indexs i' update _?=_)

    -- sort the assignments (solutions to the matching problem of step D.(ii)) 
    sort-assignments :
      ∀ {Γ Γ'} {χ χ'} {k k'}
      → List (assignment mix-var {Γ} {Γ'} {χ} {χ'})
      → tuple (mix-var) k → tuple (mix-var) k'
      → tuple (List (Σ type-expr (λ Φ → Γ' ∥ χ' ⊢ Φ))) k
      → tuple (List (Σ type-expr (λ Φ' → Γ ∥ χ ⊢ Φ'))) k'
      → (
        tuple (List (Σ type-expr (λ Φ → Γ' ∥ χ' ⊢ Φ))) k
        ×
        tuple (List (Σ type-expr (λ Φ' → Γ ∥ χ ⊢ Φ'))) k'
      )
    sort-assignments [] _ _ ψs σs = ψs , σs
    sort-assignments ((σ ≣ var-intro {α = γ} _) ∷ as) βs γs ψs σs =
      sort-assignments as βs γs ψs (lookup&update σs γs γ (λ σi → (both σ) ∷ σi) (mix-var-bool-=)) 
    sort-assignments ((var-intro {α = β} _ ≣ ψ) ∷ as) βs γs ψs σs =
      sort-assignments as βs γs (lookup&update ψs βs β (λ ψi → (both ψ) ∷ ψi) (mix-var-bool-=)) σs
    -- default case, should not happen
    sort-assignments _ βs γs _ _ = (tuple-map (λ _ → []) βs) , (tuple-map (λ _ → []) γs) 
    
-- default case, should not happen; we use the 'warning code' 2000 to
-- indicate that the user has called the function with an illegal set
-- of inputs (e.g., in the case where the term cannot be seen in the
-- given specification)
adm _ _ _ _ _ = (⟨ varᵀ (fvar 2000) , varᵀ (fvar 2000) ⟩ ∷ []) , record { curr = 2000 }

We emphasize again that this implementation is offered solely as proof-of-concept. There is lots of room for improvement, and we list some ideas below.

It would be nice to have a unified signature for variable sets, perhaps something along the lines of:

module variable-set where
  
  data Var : Set₁ where
    make-var-set :
      ∀ (name : String)  -- label
      → ∀ (id : Set)  -- identifiers
      → ∀ (fresh : ∀ {k} → tuple id k → id)  -- fresh function
      → Var

open variable-set public

Although we don’t use it in the algorithm as it is, we could envision having a term calculus over the type calculus described above:

data ⊨_∷_ : term-expr → type-expr {mix-var} → Set where
  ∗-intro : (∅ ∥ ∅ ⊢ 1ᵀ {var = mix-var}) → ⊨ ∗ᵗ ∷ 1ᵀ
  -- …

In that way, we could actually force the inputs to adm to be legal in the sense described in the paper (beginning of section 3).

We could also improve space and time efficiency, by only pushing a newly encountered data type on the stack Gs if not already there (first operation done in the last case of adm above). In the examples that we handle here, it does not matter, since the recursive calls would not blow up the size of the stack (notice that the stack’s length never exceeds the depth of the tree of calls). But we could imagine running out of memory for this reason when dealing with complex examples.

Implementation of the algorithm adm

Implementation of the algorithm `adm`