Has estado escribiendo gramaticas formales durante toda tu carrera. Cada enum en Rust, cada sealed trait en Scala, cada union discriminada de TypeScript: no son solo “tipos.” Son gramaticas formales que definen la sintaxis de tu dominio. Dicen que valores pueden existir, que formas pueden tomar los datos, que estados son expresables. Eso es exactamente lo que hace una gramatica.
La mayoria de los ingenieros nunca toman un curso de metodos formales. Los que lo hacen tienden a olvidarlo en cuanto termina el examen. Pero los conceptos nunca se fueron. Migraron a las herramientas que usamos a diario: sistemas de tipos, pattern matching, tipos de datos algebraicos. Y los usamos sin reconocer su ascendencia.
Esta serie trata de hacer visible esa ascendencia. No por credito academico, sino porque entender la distincion entre sintaxis (lo que puede expresarse) y semantica (lo que significa) cambia la forma en que disenas tipos, validas datos y previenes errores. En este primer post, empezamos con las gramaticas.
Que es una gramatica formal #
En 1956, Noam Chomsky publico “Three models for the description of language” e introdujo lo que hoy llamamos la jerarquia de Chomsky: una clasificacion de gramaticas segun su poder generativo. Una gramatica es un conjunto de reglas que define que cadenas pertenecen a un lenguaje. La jerarquia clasifica las gramaticas desde la mas restrictiva hasta la mas poderosa.
| Tipo | Nombre | Forma de regla | Reconocedor | Relevancia en programacion |
|---|---|---|---|---|
| 3 | Regular | A -> aB o A -> a |
Automata finito | Regex, analisis lexico (tokenizacion) |
| 2 | Libre de contexto | A -> gamma |
Automata de pila | Gramaticas de parsers, BNF, la mayoria de definiciones de sintaxis |
| 1 | Sensible al contexto | alpha A beta -> alpha gamma beta |
Automata linealmente acotado | Verificacion de tipos, resolucion de nombres, reglas de alcance |
| 0 | Sin restricciones | alpha -> beta |
Maquina de Turing | Computacion arbitraria |
Los lenguajes de programacion viven mayoritariamente en el Tipo-2 (gramaticas libres de contexto) para su sintaxis: el parser verifica si tu codigo fuente esta estructuralmente bien formado. Pero un programa que se parsea correctamente puede seguir siendo absurdo: referencia a variables no definidas, aplicar una funcion al tipo equivocado. Detectar esos errores requiere analisis sensible al contexto. Eso es lo que hace el verificador de tipos. La sintaxis dice que la oracion es gramatical. La semantica dice si significa algo.
BNF: la notacion que ya conoces #
Cuando John Backus y Peter Naur formalizaron la gramatica de ALGOL 60, nos dieron la Forma de Backus-Naur (BNF), una notacion para escribir gramaticas libres de contexto como reglas de produccion. La has visto en cada especificacion de lenguaje. Aqui hay una gramatica pequena para expresiones aritmeticas:
<expr> ::= <num>
| <expr> "+" <expr>
| <expr> "*" <expr>Tres reglas de produccion. Una expresion es un numero, una suma de dos expresiones, o una multiplicacion de dos expresiones. Ahora mira la misma gramatica expresada como un enum de Rust:
// Rust: the BNF grammar as a type
enum Expr {
Num(f64),
Add(Box<Expr>, Box<Expr>),
Mul(Box<Expr>, Box<Expr>),
}// Scala: the same grammar as a type
sealed trait Expr
case class Num(value: Double) extends Expr
case class Add(left: Expr, right: Expr) extends Expr
case class Mul(left: Expr, right: Expr) extends ExprLa correspondencia es exacta. Cada variante (Rust) o case class (Scala) es una regla de produccion. Las referencias recursivas a Expr / Box<Expr> son no terminales, simbolos que se expanden en mas estructura. Los valores hoja (f64, Double) son terminales, los atomos que no pueden descomponerse mas. La definicion del tipo ES la gramatica, expresada en un lenguaje que el compilador puede hacer cumplir.
AST vs CST: lo que tu parser descarta #
Cuando un parser lee la cadena (1 + 2) * 3, primero construye un Arbol de Sintaxis Concreta (CST), un arbol que preserva cada detalle del texto fuente: parentesis, espacios en blanco, tokens de operadores, comentarios. El CST es una representacion fiel de lo que se escribio.
Luego el parser lo transforma en un Arbol de Sintaxis Abstracta (AST). El AST descarta todo lo que solo se necesitaba para el parseo. Los parentesis desaparecen porque la estructura del arbol ya codifica la precedencia: Mul(Add(Num(1), Num(2)), Num(3)). Los espacios en blanco desaparecen porque no llevan informacion estructural. Lo que queda es estructura pura.
Cuando defines enum Expr con esas tres variantes, estas definiendo el AST, la sintaxis abstracta de tu lenguaje de expresiones. Estas declarando que formas puede tomar un valor, sin prescribir como esas formas aparecen como texto. Esta es una distincion fundamental. La gramatica define el espacio de estructuras validas. El parseo es la funcion que mapea texto concreto a ese espacio. El tipo es la gramatica. El parser es el puente.
ADTs como gramaticas de dominio #
Los ejemplos hasta ahora han sido sobre lenguajes de expresiones, el hogar tradicional de las gramaticas formales. Pero la intuicion se generaliza. Cada tipo de dato algebraico que escribes es una gramatica para algun dominio. Considera un flujo de trabajo de pedidos:
// Rust
enum OrderStatus {
Pending,
Confirmed { confirmed_at: DateTime<Utc> },
Shipped { tracking: String, shipped_at: DateTime<Utc> },
Delivered { delivered_at: DateTime<Utc> },
Cancelled { reason: String },
}// Scala
sealed trait OrderStatus
case object Pending extends OrderStatus
case class Confirmed(confirmedAt: Instant) extends OrderStatus
case class Shipped(tracking: String, shippedAt: Instant) extends OrderStatus
case class Delivered(deliveredAt: Instant) extends OrderStatus
case class Cancelled(reason: String) extends OrderStatusEsto es una gramatica. Define el vocabulario de tu dominio de pedidos. Cinco reglas de produccion, cada una generando una forma diferente de oracion. Pending es un terminal: no toma argumentos, simplemente es. Shipped es una produccion con dos campos: una cadena de seguimiento y una marca de tiempo. Juntas, las variantes definen que estados son expresables.
Observa lo que esta gramatica NO define. No dice que un pedido Pending deba transicionar a Confirmed antes de poder convertirse en Shipped. No dice que un pedido Cancelled nunca deba convertirse en Delivered. No dice que tracking deba ser no vacio. La gramatica define lo que puede decirse. No dice nada sobre lo que deberia decirse. Esa distincion, entre sintaxis y semantica, es el punto central de esta serie.
Una gramatica bien disenada reduce el espacio de estados expresables a algo cercano al espacio de estados significativos. Pero “cercano” no es “igual.” Siempre hay una brecha.
La brecha: sintacticamente valido, semanticamente vacio #
En 1957, Chomsky escribio una oracion que se hizo famosa precisamente porque ilustra la frontera entre sintaxis y semantica:
“Colorless green ideas sleep furiously.”
La oracion es gramaticalmente perfecta. Sujeto, adjetivo, verbo, adverbio, todo en las posiciones correctas. Un parser la aceptaria. Pero no significa nada. La sintaxis es valida; la semantica esta vacia.
Lo mismo ocurre en el codigo. Considera este valor perfectamente bien tipado:
let status = OrderStatus::Shipped {
tracking: String::new(), // empty string
shipped_at: Utc::now(),
};val status: OrderStatus = Shipped(tracking = "", shippedAt = Instant.now())El sistema de tipos lo acepta. La gramatica dice que Shipped toma un String y una marca de tiempo, y eso es exactamente lo que proporcionamos. Pero un envio con un numero de seguimiento vacio es absurdo. Es el equivalente de dominio de las ideas verdes incoloras. La gramatica, tu enum, tu sealed trait, define la sintaxis de tu dominio. Controla que formas pueden tomar los valores. Pero no controla lo que esas formas significan.
Esto no es un fallo del sistema de tipos. Es una declaracion sobre lo que las gramaticas pueden y no pueden hacer. Las gramaticas generan estructura. El significado requiere algo mas: un marco semantico que asigne interpretacion a las estructuras que la gramatica produce. Cerrar esta brecha, hacer imposibles los valores sintacticamente validos pero semanticamente vacios, es el desafio central del diseno dirigido por tipos.
Lo que viene despues #
En la Parte 2, vemos los tres enfoques clasicos para definir semantica: operacional, denotacional y axiomatica. Mostramos como cada uno se mapea a una tecnica concreta que ya usas: brazos de match, funciones puras y contratos a nivel de tipos. La gramatica define lo que tu dominio puede decir. La semantica define lo que deberia significar.