Skip to content

Instantly share code, notes, and snippets.

@cxandru

cxandru/Razor.lagda

Created January 12, 2026 12:40
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save cxandru/91b1497ca735bb251b688add18512c39 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save cxandru/91b1497ca735bb251b688add18512c39 to your computer and use it in GitHub Desktop.
Download ZIP
Alexandru's recursion razor
Raw
Razor.lagda
The question is how to encode the mutual nested recursion happening in "razor" using structured recursion (ideally recursive coalgebras)
\begin{code}
open import Level using (Level;_⊔_;0ℓ)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality.Core
module Razor where
open import Data.Nat
open import Data.Product
open import Function.Base
open import Data.String
mutual
data Expr : Set where
_:+:_ : Expr → Expr → Expr
Var : String → Expr
Lit : ℕ → Expr
Let_In : Assgt → Expr → Expr
data Assgt : Set where
_↦_ : String → Expr → Assgt
Env : Set
Env = String → ℕ
\end{code}
%<*razor>
\begin{code}
mutual
evA : Env → Assgt → Env
evE : Env → Expr → ℕ
evA env ( x ↦ expr ) = λ y → case x ≈? y of
λ{ (yes _) → evE env expr
; (no _) → env y }
evE env (x :+: y) = evE env x + evE env y
evE env (Var x) = env x
evE env (Lit n) = n
evE env (Let assgt In expr) = evE (evA env assgt) expr
\end{code}
%</razor>
\begin{code}
-- decode the mutual recursion:
data EoA : Set where
E : EoA
A : EoA
data AST : EoA → Set where
_:+:_ : AST E → AST E → AST E
Var : String → AST E
Lit : ℕ → AST E
Let_In : AST A → AST E → AST E
_↦_ : String → AST E → AST A
ev : Env → {i : EoA} → AST i → (case i of λ{A → Env ; E → ℕ})
ev env (x :+: y) = ev env x + ev env y
ev env (Var x) = env x
ev env (Lit n) = n
ev env (Let assgt In expr) = ev (ev env assgt) expr
ev env (x ↦ expr) = λ y → case x ≈? y of
λ{ (yes _) → ev env expr
; (no _) → env y }
\end{code}
@cxandru
Copy link
Copy Markdown
Author

cxandru commented Feb 2, 2026

@NathanielB123 I've translated your definition back into explicitly an algebra for the original functor:

ASTENV : EoA → Set
ASTENV = λ{A → Env → Env ; E → Env → ℕ}

module foo where
  data ASTF (r : EoA → Set) : EoA → Set where
    _:+:_ : r E → r E → ASTF r E
    Var : String → ASTF r E
    Lit : ℕ → ASTF r E
    Let_In : r A {- ev env assgt -} → r E {- ev env expr ↯ -} → ASTF r E
    _↦_ : String → r E → ASTF r A

  -- translation of Nathaniel's soln
  evAlg : {i : EoA} → ASTF ASTENV i → ASTENV i
  evAlg (x :+: x₁) env = x env + x₁ env
  evAlg (Var x) env = env x
  evAlg (Lit n) env = n
  evAlg (Let envt In expr) env = expr (envt env) 
  evAlg (x ↦ x₁) env = λ y → case x ≈? y of
    λ{ (yes  _) → x₁ env
     ; (no   _) → env y }

@cxandru
Copy link
Copy Markdown
Author

cxandru commented Feb 2, 2026

@NathanielB123 @lawcho I feel like there seems to be something going on with eliminating nestedness by eliminating to higher types (the hierarchy here as in System T, i.e. every arrow left or right increases the level of the type), since this is also how one does it for Ackermann

@NathanielB123
Copy link
Copy Markdown

NathanielB123 commented Feb 9, 2026

Ooh that's an interesting point. So I guess the concrete question is: can you write this interpreter with only primitive recursion? I'm not sure...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment