Ir al contenido
  1. Posts/

Tagless Final es semantica denotacional disfrazada

·10 mins
Rafael Fernandez
Autor
Rafael Fernandez
Matemáticas, programación y cosas de la vida

“Doing a tagless-final embedding is literally writing a denotational semantics for the DSL – in a host programming language rather than on paper.” – Oleg Kiselyov

Si alguna vez has definido un trait en Rust y proporcionado dos implementaciones, una para produccion, otra para tests, has hecho tagless final. Si alguna vez has escrito una type class de Scala con instancias given para diferentes tipos, has hecho tagless final. El patron que Kiselyov, Carette y Shan formalizaron en su paper de 2007 es el mismo patron que la arquitectura hexagonal llama “puertos y adaptadores” y que todo framework de inyeccion de dependencias llama “interfaz mas implementacion.”

El nombre formal no agrega ceremonia. Revela por que el patron funciona: porque definir una interfaz e intercambiar implementaciones es exactamente lo que hace la semantica denotacional: mapear sintaxis (que operaciones existen) a significado (que hacen). La serie Sintaxis y Semantica introdujo estos conceptos: las gramaticas definen la sintaxis, las funciones de interpretacion definen la semantica, y la brecha entre ellas es donde viven los bugs. Tagless final es la tecnica que cierra esa brecha a nivel de tipos.

Inicial vs final: dos formas de representar un lenguaje
#

Hay dos formas fundamentalmente diferentes de codificar un lenguaje pequeno dentro de un lenguaje anfitrion. La primera, la que aprendiste primero, es construir una estructura de datos.

Codificacion inicial: construye el arbol, luego interpretalo
#

// Rust: initial encoding
enum Expr {
    Lit(i32),
    Add(Box<Expr>, Box<Expr>),
    Neg(Box<Expr>),
}

fn eval(e: &Expr) -> i32 {
    match e {
        Expr::Lit(n) => *n,
        Expr::Add(l, r) => eval(l) + eval(r),
        Expr::Neg(e) => -eval(e),
    }
}
// Scala: initial encoding
sealed trait Expr
case class Lit(n: Int) extends Expr
case class Add(l: Expr, r: Expr) extends Expr
case class Neg(e: Expr) extends Expr

def eval(e: Expr): Int = e match {
  case Lit(n)    => n
  case Add(l, r) => eval(l) + eval(r)
  case Neg(e)    => -eval(e)
}

Construyes un AST, un arbol de sintaxis, y luego lo recorres con una funcion. Agregar una nueva interpretacion (digamos, pretty-printing) significa escribir otra funcion sobre el mismo arbol. Agregar un nuevo tipo de nodo (digamos, Mul) significa tocar cada funcion existente. Esta es el algebra inicial: constructores, induccion, construir hacia arriba.

Codificacion final: define la sintaxis como una interfaz, computa directamente
#

// Rust: final encoding (tagless final)
trait ExprSym {
    type Repr;
    fn lit(&self, n: i32) -> Self::Repr;
    fn add(&self, l: Self::Repr, r: Self::Repr) -> Self::Repr;
    fn neg(&self, e: Self::Repr) -> Self::Repr;
}

struct Eval;
impl ExprSym for Eval {
    type Repr = i32;
    fn lit(&self, n: i32) -> i32 { n }
    fn add(&self, l: i32, r: i32) -> i32 { l + r }
    fn neg(&self, e: i32) -> i32 { -e }
}

struct PrettyPrint;
impl ExprSym for PrettyPrint {
    type Repr = String;
    fn lit(&self, n: i32) -> String { n.to_string() }
    fn add(&self, l: String, r: String) -> String { format!("({l} + {r})") }
    fn neg(&self, e: String) -> String { format!("(-{e})") }
}

// Same program, different meanings:
fn program<S: ExprSym>(s: &S) -> S::Repr {
    s.add(s.lit(1), s.neg(s.lit(2)))
}
// Scala: final encoding (tagless final)
trait ExprSym[Repr] {
  def lit(n: Int): Repr
  def add(l: Repr, r: Repr): Repr
  def neg(e: Repr): Repr
}

given ExprSym[Int] with {
  def lit(n: Int) = n
  def add(l: Int, r: Int) = l + r
  def neg(e: Int) = -e
}

given ExprSym[String] with {
  def lit(n: Int) = n.toString
  def add(l: String, r: String) = s"($l + $r)"
  def neg(e: String) = s"(-$e)"
}

def program[R](using alg: ExprSym[R]): R =
  alg.add(alg.lit(1), alg.neg(alg.lit(2)))

No se construye ningun AST. La funcion program computa su resultado directamente, y el tipo del resultado depende enteramente de que interprete conectes. Llama program(&Eval) y obtienes -1. Llama program(&PrettyPrint) y obtienes "(1 + (-2))". Misma sintaxis, diferente semantica.

Esto ES semantica denotacional. El trait define la sintaxis: que operaciones existen. Cada implementacion mapea esa sintaxis a un dominio matematico: enteros, cadenas, efectos. La notacion de doble corchete ⟦.⟧ del post de semantica formal es exactamente esto: ⟦program⟧_Eval = -1, ⟦program⟧_PrettyPrint = "(1 + (-2))".

Que significan “tagged” y “tagless”
#

Las primeras codificaciones de DSLs tipados dentro de un lenguaje anfitrion usaban etiquetas de tipo en tiempo de ejecucion para mantener la seguridad de tipos. Envolvias valores en un enum Value con variantes como IntVal(i32) y BoolVal(bool), y luego verificabas etiquetas en tiempo de ejecucion. Este es el enfoque “tagged”, y descarta el sistema de tipos del lenguaje anfitrion.

“Tagless” significa que el compilador anfitrion maneja los tipos directamente. En la codificacion final de arriba, Repr = i32 y Repr = String se verifican en tiempo de compilacion. Sin etiquetas, sin casts, sin errores de tipo en tiempo de ejecucion. El metalenguaje (Rust, Scala) hace el trabajo por ti.

Que significan “inicial” y “final”
#

Los nombres vienen de la teoria de categorias, pero la intuicion es concreta. Inicial significa “definido por constructores”: construyes una estructura (el AST) y luego la consumes. En terminos algebraicos, un algebra inicial es el menor punto fijo: la estructura mas pequena que satisface la gramatica. Puedes hacer pattern matching sobre ella, serializarla, optimizarla.

Final significa “definido por observaciones”: interactuas a traves de una interfaz y nunca ves la representacion interna. Una coalgebra final es el mayor punto fijo: se caracteriza no por como la construyes sino por lo que puedes preguntarle. No puedes inspeccionar un programa tagless-final; solo puedes interpretarlo.

El ADT es inicial. El trait es final.

Tagless final en Scala: el patron del ecosistema
#

El ecosistema de Scala, particularmente Cats-Effect, adopto tagless final como su patron de arquitectura dominante. La receta es siempre la misma: define un algebra (un trait parametrizado por un tipo de efecto F[_]), escribe programas polimorficos en F, y elige un efecto concreto en el borde del mundo.

trait UserRepo[F[_]] {
  def find(id: UserId): F[Option[User]]
  def save(user: User): F[Unit]
}

def createUser[F[_]: Monad](repo: UserRepo[F], name: String): F[User] =
  for {
    user <- Monad[F].pure(User(name))
    _    <- repo.save(user)
  } yield user

// Production: F = IO
// Testing:    F = State[TestState, *]

El trait UserRepo[F[_]] es el algebra. Cada implementacion, una respaldada por PostgreSQL, otra por un mapa en memoria, es un interprete. La logica de negocio en createUser es un programa que funciona con cualquier interprete. Eliges IO para produccion y State para testing. Esto es polimorfismo de efectos: el programa se escribe una vez y se ejecuta bajo diferentes modelos computacionales.

El patron tagless final en Scala ES inyeccion de dependencias, pero a nivel de tipos en vez de a nivel de tiempo de ejecucion. El algebra es la interfaz. El interprete es la implementacion. El parametro F[_] es el grado extra de libertad que te permite abstraer sobre todo el sistema de efectos.

John De Goes critico famosamente este patron como “inyeccion de dependencias con pasos extra.” La critica es justa cuando nunca explotas realmente el polimorfismo de efectos, cuando F siempre es IO y tienes un solo interprete por algebra. En ese caso, pagas por la abstraccion sin usarla. Pero la critica es injusta cuando genuinamente necesitas multiples interpretaciones: produccion vs test, sincrono vs asincrono, real vs mock. El poder del patron es proporcional al numero de interpretes que realmente escribes.

Tagless final en Rust: ya lo estas haciendo
#

Aqui esta la afirmacion: si has escrito arquitectura hexagonal basada en traits en Rust, has escrito tagless final. Simplemente nunca lo llamaste asi.

Considera el port trait de la serie todo-cli:

// This IS a tagless-final algebra:
pub trait TaskRepository {
    fn save(&mut self, task: &Task) -> Result<(), RepoError>;
    fn find_all(&self) -> Result<Vec<Task>, RepoError>;
    fn delete(&mut self, id: &TaskId) -> Result<(), RepoError>;
}

// These are interpreters:
impl TaskRepository for JsonFileTaskRepository { /* ... */ }
impl TaskRepository for InMemoryTaskRepository { /* ... */ }

// This is a program polymorphic in the interpreter:
pub struct AddTaskService<R: TaskRepository> {
    repo: R,
}

El trait TaskRepository define la sintaxis: que operaciones existen. JsonFileTaskRepository mapea esas operaciones a I/O de archivos JSON. InMemoryTaskRepository las mapea a un HashMap. Estas son dos denotaciones diferentes de la misma sintaxis. El parametro generico R: TaskRepository juega el mismo rol que F[_] en Scala: abstrae sobre el interprete, y la logica de negocio nunca sabe con cual esta hablando.

Rust no tiene higher-kinded types nativos, asi que no puedes escribir trait UserRepo[F[_]] como lo hace Scala. Esto significa que la version completa de tagless final con polimorfismo de efectos, donde F abstrae sobre IO, State, Future simultaneamente, requiere GATs o tipos asociados y es mas verbosa. Pero para el caso sin polimorfismo de efectos, que cubre la mayoria de la arquitectura de aplicaciones, trait + impl + generic es suficiente. Y ese caso es el comun.

El patron se mapea limpiamente:

Scala (tagless final) Rust (arquitectura hexagonal)
Algebra (trait Repo[F[_]]) Port trait (trait TaskRepository)
Interprete (given Repo[IO]) Adapter (impl TaskRepository for JsonFile...)
Programa (def logic[F[_]: Monad]) Servicio (struct Service<R: TaskRepository>)
Tipo de efecto (F[_]) Parametro generico (R: TaskRepository)

El vocabulario difiere. El patron es identico.

Resolviendo el Expression Problem
#

El Expression Problem, articulado por primera vez por Philip Wadler en 1998, pregunta: puedes agregar tanto nuevas variantes de datos como nuevas operaciones sin modificar codigo existente? Con la codificacion inicial (ADTs), agregar una nueva operacion es facil (escribe una nueva funcion) pero agregar una nueva variante te obliga a actualizar cada funcion existente. Con la codificacion final (traits), ambos ejes son independientemente extensibles.

Agregar nueva sintaxis? Define un trait de extension:

trait MulSym: ExprSym {
    fn mul(&self, l: Self::Repr, r: Self::Repr) -> Self::Repr;
}
trait MulSym[Repr] extends ExprSym[Repr] {
  def mul(l: Repr, r: Repr): Repr
}

Agregar nueva semantica? Escribe una nueva implementacion. Ningun cambio toca codigo existente. El post del Expression Problem explora esta tension en detalle; tagless final es una de sus resoluciones mas limpias.

Cuando usar inicial vs final
#

Ninguna codificacion es universalmente mejor. La eleccion depende de lo que necesitas hacer con el lenguaje.

Usa inicial (ADTs) cuando… Usa final (tagless final) cuando…
Necesitas inspeccionar, serializar u optimizar el AST Necesitas multiples interpretaciones
Pattern matching es tu herramienta principal Quieres intercambiar implementaciones a nivel de tipos
Las operaciones crecen mas rapido que los tipos de datos Los tipos de datos crecen mas rapido que las operaciones
Necesitas transformaciones de multiples pasadas Quieres polimorfismo de efectos (Scala)
Necesitas depurar imprimiendo el arbol Estas haciendo arquitectura hexagonal (Rust)

En la practica, muchos sistemas reales usan ambas. Un front-end de compilador construye un AST (codificacion inicial) y luego lo interpreta a traves de un pipeline de pasadas. Una capa de servicios define port traits (codificacion final) e inyecta implementaciones al inicio. La distincion no es una religion; es una dimension de diseno.

El isomorfismo de Boehm-Berarducci demuestra que las dos codificaciones son equivalentes en poder expresivo: cualquier codificacion inicial puede transformarse mecanicamente en una final via Church encoding, y viceversa. Son perspectivas duales de la misma estructura. La pregunta nunca es “cual es correcta” sino “cual hace que el cambio sea mas facil para este codebase.”

Cierre
#

La conexion entre la semantica formal y la ingenieria diaria no es una metafora. Es una correspondencia precisa. Construir un ADT es escribir una gramatica. Escribir un match sobre el es escribir semantica operacional. Definir un trait y proporcionar implementaciones es escribir semantica denotacional. La intuicion de Kiselyov no fue inventar un patron nuevo; fue notar que el patron que los programadores ya usaban tenia un nombre formal y un cuerpo de teoria detras.

La proxima vez que definas un trait con multiples implementaciones, sabe exactamente lo que estas haciendo: estas escribiendo semantica denotacional en un lenguaje de programacion en vez de en papel. El algebra es tu sintaxis. La implementacion es tu funcion semantica. El compilador es tu asistente de pruebas. Has estado haciendo metodos formales todo este tiempo.

Referencias:

  • Kiselyov, Carette, Shan, “Finally Tagless, Partially Evaluated” (JFP 2009; version de conferencia 2007)
  • Wadler, “The Expression Problem” (1998)
  • okmij.org/ftp/tagless-final/, pagina de recursos de Kiselyov sobre tagless final