Handling substitutions of mutually defined types with Agda's standard library's Data.Fin.Substitution

Question

I'm trying to encode a call-by-push-value lambda calculus with isorecursive types in Agda. So I mutually define value types and computation types with up to n free value type variables (I only need to substitute value types for the isorecursive types) as follows (this is just a fragment).

data VType (n : ℕ) : Set where
  vunit : VType n                -- unit type
  var   : Fin n → VType n        -- type variable
  u     : CType n → VType n      -- thunk
  μ    : VType (1 + n) → VType n -- isorecursive type

data CType (n : ℕ) : Set where
  _⇒_ : VType n → CType n → CType n -- lambda abstraction
  f    : VType n → CType n          -- a value-producer

In the style here, I want to be able to do substitutions like

example : CType 0
example = f (var (# 0)) C[/ vunit ]

where

_C[/_] : ∀ {n} → CType (1 + n) → VType n → CType n
ct [/ vt ] = ?

post-substitutes vt into ct. Notice I want to substitute a value type into a computation type. I am able to use the standard library to substitute VTypes into VTypes, but not VTypes into CTypes, like above. I do that like so, using Data.Fin.Substitution (see here):

module TypeSubst where
  -- Following Data.Substitutions.Example
  module TypeApp {T} (l : Lift T VType) where
    open Lift l hiding (var)

    -- Applies a substitution to a type
    infixl 8 _/v_

    _/v_ : ∀ {m n} → VType m → Sub T m n → VType n
    _/c_ : ∀ {m n} → CType m → Sub T m n → CType n
    vunit /v ρ = vunit
    (var x) /v ρ = lift (lookup x ρ)
    (u σ) /v ρ = u (σ /c ρ)
    (μ τ) /v ρ = μ (τ /v ρ ↑)
    (σ ⇒ τ) /c ρ = σ /v ρ ⇒ τ /c ρ
    f x /c ρ = f (x /v ρ)

    open Application (record { _/_ = _/v_ }) using (_/✶_)

  typeSubst : TermSubst VType
  typeSubst = record { var = var; app = TypeApp._/v_ }

  open TermSubst typeSubst public hiding (var)

  weaken↑ : ∀ {n} → VType (1 + n) → VType (2 + n)
  weaken↑ τ = τ / wk ↑

  infix 8 _[/_]

  -- single type substitution
  _[/_] : ∀ {n} → VType (1 + n) → VType n → VType n
  τ [/ σ ] = τ / sub σ

I've tried working with a new datatype Type:

data VorC : Set where
  v : VorC
  c : VorC

data Type : VorC → ℕ → Set where
  vtype : ∀ {n} → VType n → Type v n
  ctype : ∀ {n} → CType n → Type c n

I tried using the natural unwrapping function to go from Types to VType's or CType's, but this doesn't seem to work or leads to termination checking problems if I try mimicking the standard library's module.

Does anyone know if it is possible to use Data.Fin.Substitution from the standard library to accomplish something like this? Could someone explain that module to me? There is no documentation on this... If it isn't possible to use the standard library for this, any pointers on how to approach this problem is also welcome. Thanks!

Answer 1

You can open Application in the CType case instead of opening TermSubst which looks inappropriate (I don't know what's wrong with it). Here is the relevant part:

typeSubst : TermSubst VType
typeSubst = record { var = var; app = TypeApp._/v_ }

open TermSubst typeSubst public hiding (var)

module TypeSubst where
  _[/v_] : ∀ {n} → VType (1 + n) → VType n → VType n
  τ [/v σ ] = τ / sub σ

open Application (record { _/_ = TypeApp._/c_ termLift }) renaming (_/_ to _/c_) using ()

_[/c_] : ∀ {n} → CType (1 + n) → VType n → CType n
τ [/c σ ] = τ /c sub σ

The whole code.

To understand what's going in the standard library you need to read the Type-Preserving Renaming and Substitution paper. Though, the code in stdlib is quite more abstract.

BTW, you can use order preserving embeddings to define renaming and renaming to define substitution. Fill the holes here.