Prism: un lenguaje funcional impuro con efectos tipados

 (stephendiehl.com)
1 puntos por GN⁺ 1 시간 전 | 1 comentarios | Compartir por WhatsApp
  • Prism es un compilador experimental que no oculta efectos como variables mutables, excepciones y streams, sino que los expone en los tipos, mientras mantiene los cambios locales no observables desde afuera como tipos puros, por ejemplo Int -> Int
  • La idea central son los handlers de efectos algebraicos y el polimorfismo de filas (row polymorphism): los efectos se combinan en la fila del tipo de función, y los handlers procesan solo las etiquetas necesarias y reenvían el resto
  • El mismo sistema de efectos expresa excepciones, generadores/streams, lentes, estado con var y flujos fail/guard; algunas rutas se bajan sin listas intermedias ni composición en runtime
  • En rendimiento, combina evidence passing con conteo de referencias Perceus para evitar asignaciones por cada llamada de efecto, y optimiza las actualizaciones funcionales de valores con propiedad única como mutaciones in-place
  • Prism ofrece LLVM IR, MLIR, runtime en C, intérprete en Rust, modelo en Lean 4 y playground WASM para verificar directamente la inferencia de tipos y los resultados del lowering

Cambios no visibles desde afuera y efectos tipados

  • El punto de partida de Prism es que incluso una función fib que usa var y asignación internamente puede verse como una función pura para un observador externo
    • El ejemplo fib actualiza dos variables in-place, pero no expone estado fuera de la función
    • Su tipo es Int -> Int, y el efecto no aparece en el tipo
  • Prism es un compilador funcional de prueba de concepto desarrollado durante los últimos 3 años, que modela efectos a partir de ideas modernas de tipos de las familias OCaml 5, Haskell y Koka
  • La dirección central no es evitar los efectos, sino incorporarlos al sistema de tipos y optimizar para que el compilador elimine su costo

Los efectos funcionan como interfaces

  • Los efectos de Prism siguen el enfoque de handlers de efectos algebraicos: se declaran operaciones y un handler les da significado
    • effect Gen { ctl yield(Int) : Unit } declara la operación yield
    • El !{Gen} en fn produce(n) : !{Gen} Unit indica en el tipo que la función realiza yield
  • Incluso el mismo productor se interpreta con significados distintos según cómo se maneje la continuación k
    • total suma los valores de yield
    • count cuenta cuántas veces ocurre yield
    • Descartar k produce una excepción; llamarla una vez produce estado o un generador; llamarla varias veces produce comportamiento de búsqueda
  • El ejemplo del efecto Amb expresa la búsqueda de ternas pitagóricas con choose y reject
    • choose(n) proporciona valores en el rango 0..n-1
    • El handler reanuda la misma continuación para cada candidato y construye un árbol de búsqueda
  • A diferencia de OCaml 5, Prism incluye los efectos en los tipos, y no requiere levantar manualmente capas como en una pila de transformadores de mónadas de Haskell
    • Las filas de efectos se combinan estructuralmente a través de las llamadas
    • No se comportan como una pila, sino como un conjunto de etiquetas

Funcionalidades expresadas con un solo mecanismo

  • Excepciones

    • En Prism, una excepción es un handler que descarta la continuación
    • Una cláusula final ctl desecha k y usa el valor de su cuerpo como resultado del handler
    • No es un mecanismo de propagación de Result ni de repartir ? por la pila de llamadas
    • Como las excepciones son etiquetas en la fila de efectos, se componen como excepciones extensibles
    • Cada falla es una operación separada, y la fila del tipo de función indica qué excepciones pueden escapar
    • En el ejemplo de Abort y Timeout, fetch tiene !{Abort, Timeout}
    • with_default maneja solo Timeout y devuelve el fallback "cached"; después de manejarlo, en el tipo solo queda !{Abort}
    • A diferencia de las checked exceptions de Java, no están atadas a una jerarquía de clases, sino que funcionan como un conjunto estructural abierto

  • Generadores y streams

    • Un stream se compone de un productor que realiza emit, transformadores que lo capturan y lo vuelven a emitir, y consumidores que hacen fold
    • Como el pipeline tiene la forma de handlers anidados alrededor de un solo productor, no se generan listas intermedias por estructura
    • Ejemplo: srange(1, n).smap(square).skeep(even).stake(5).ssum()
    • Una interrupción temprana como stake(5) es un handler que descarta la continuación después de obtener los valores necesarios
    • La biblioteca de streams está influenciada por pipes y conduit de Haskell

  • Lentes

    • En Prism, las lentes no son una biblioteca separada, sino una combinación de rutas de actualización de registros y modelo de memoria
    • En registros anidados se pueden actualizar varios campos profundos con una sola expresión de ruta
    • Ejemplo: { g | player.pos.x = 30, player.hp = 95, score = 110 }
    • Se reconstruye el spine del registro anidado, pero si el valor tiene propiedad única, se reutiliza la celda descompuesta
    • Gracias a esta estructura, una actualización funcional puede compilarse a escrituras de punteros
    • No se asignan ni componen tipos optic en runtime
    • deriving (Lens) genera accesores comunes como score_of y with_score

  • Estado mutable

    • var se desazucara a operaciones get/set de un efecto privado
    • Un handler instalado al final del bloque maneja ese efecto
    • El análisis de escape de closures rechaza los casos en los que el estado se escapa hacia afuera
    • La función envolvente puede mantener una fila de efectos vacía

  • Falla

    • La falla se expresa como un efecto Fail anónimo, y el sistema de tipos maneja que “esta expresión puede no producir un valor”
    • fail() realiza la falla, y guard(cond) falla cuando la condición es falsa
    • ?? usa un fallback cuando el lado izquierdo falla
    • ?. recorre una cadena de opciones y se corta temprano
    • Una guard en una comprehension poda los elementos fallidos en vez de hacer crash
    • Como var también es azúcar sobre handlers, un bloque transact puede tomar snapshots de variables live y hacer rollback si falla

Funciones modernas de tipos

  • Prism usa inferencia de tipos bidireccional higher-rank de la familia Dunfield-Krishnaswami para que en la mayoría del código no haga falta escribir signaturas de tipos
  • En límites donde se necesita polimorfismo de orden superior, se explicita el binder con forall
    • pick(g : forall a. (a) -> a) puede aplicar g tanto a Bool como a Int
    • En un core Damas-Milner, a se unificaría con Bool en la primera llamada y la segunda sería rechazada
  • El polimorfismo ad hoc se expresa con clases de tipos al estilo Lean
    • Las instancias son valores con nombre
    • given Ord(a) requiere un diccionario
    • Cuando hay varias instancias, una se marca como canonical y las demás se explicitan con using
  • deriving genera instancias repetitivas y accesores de campos como Eq, Ord, Show y Lens
  • El pattern matching también se conecta con las clases
    • pattern First(n) for Peek = view peek es un patrón que usa un método de clase como view
    • head_or puede usar el mismo patrón para varios tipos que tienen una instancia Peek
  • show funciona orientado por tipos, sin una clase separada
    • El compilador sintetiza un printer estructural a partir del tipo estático
    • No decide cómo imprimir leyendo tags de tipo en runtime
  • Las filas de efectos también son polimórficas
    • fn twice(f : (Unit) -> Int ! {| e}) suma los resultados sin importar cuál sea la fila de efectos e de la función recibida
    • En un thunk puro, e se unifica con la fila vacía {}
    • En un thunk que realiza efectos como Tick o Say, esa fila se reenvía tal cual

Estrategia de compilación para reducir el costo de los efectos

  • Una implementación académica clásica de efectos algebraicos puede reconstruir la computación como un árbol en forma de free monad y asignar pequeñas celdas por cada operación
  • La ruta rápida de Prism es evidence passing, en la línea de Koka
    • En vez de reconstruir la computación para encontrar el handler, las cláusulas de handlers activas se pasan a cada punto de operación como parámetros normales
    • do op se baja a una llamada directa
    • Al instalar un handler se asigna solo un closure, por lo que el costo es O(handlers) y no proporcional al número de operaciones
  • La codificación como free monad queda como fallback
    • Cálculos que se escapan a estructuras de datos
    • Resumptions multishot reales
    • Patrones como handlers enmascarados
  • Los pipelines de streams calculan la evidence de efectos necesaria más allá de los límites de funciones mediante análisis de flujo interprocedural
    • Se enhebra la evidence por productores y transformadores
    • Toda la cadena se baja a un único bucle
    • No hay listas intermedias ni asignaciones de celdas por operación
  • Esta estrategia obtiene en un compilador de efectos resultados parecidos a la stream fusion de Haskell o a la unificación de adaptadores de iteradores de Rust

Modelo de memoria y runtime

  • Prism usa conteo de referencias Perceus
    • Las celdas del heap se liberan de forma determinista en puntos conocidos estáticamente
    • No hay pausas ni tracing
  • La reutilización limitada al frame vuelve a pasar al constructor las celdas recién descompuestas por pattern matching
    • Un map sobre una lista con propiedad única parece una función pura que devuelve una lista nueva, pero en realidad puede modificarse in-place
    • El mismo mecanismo permite que una actualización con lentes se compile a escrituras de punteros
  • La estructura del runtime se parece a la disciplina de memoria de Lean 4, pero Prism emite LLVM IR
    • El LLVM IR se genera mediante inkwell
    • Para el mismo programa también genera un módulo MLIR textual
    • El resultado se enlaza con clang contra un runtime en C escrito a mano, prism_rt.c
  • prism_rt.c es un runtime pequeño, de unas 2 mil líneas
    • Las celdas del heap son estructuras de 4 o más words con forma { refcount, tag, arity, fields... }
    • Incluye allocator, rc_inc/rc_dec, allocator de reutilización in-place, y primitivas de bignum y strings
    • No hay collector thread, card table ni safepoints
  • El allocator por defecto es malloc de libc, con una configuración opt-in de mimalloc para benchmarks
  • El oracle de celdas live hace assert al finalizar que el balance del heap sea 0, para que la suite de pruebas verifique la propiedad garbage-free

Modelo en Lean y validación de backends

  • El intérprete de Prism pertenece a la familia de máquinas CEK, y esa máquina está reflejada en el modelo Lean 4 models/Prism.lean
  • El modelo Lean 4 tiene un teorema verificado por máquina de que la relación small-step es determinista
    • Un programa avanza exactamente a un único siguiente estado
  • El intérprete implementado en Rust también se usa como oracle diferencial
    • Todos los programas del corpus pasan por el intérprete y por los backends LLVM, MLIR y binario enlazado con C
    • La build solo pasa si la salida de los cuatro resultados es byte-identical
  • El determinismo es la base de una ejecución durable reproducible
    • La idea es que, si se fijan las entradas y se registra la ejecución, se pueda reproducir bit a bit
    • En versiones futuras se imagina un Prism que verifique como propiedad de tipos la seguridad de replay después de un crash

Playground WASM y código fuente

  • El mismo intérprete se compila a WASM, por lo que se puede ejecutar código Prism sin instalar nada en el playground
  • El playground ejecuta los programas en un worker
  • Con botones se pueden volcar las signaturas de tipos inferidas, la fila de efectos y el core IR bajado
    • Se puede ver en qué forma se baja realmente un bucle var o un pipeline de streams
  • Los ejemplos del texto están incluidos en un dropdown
  • Todo el código fuente, el modelo Lean y el runtime en C están en el repositorio de Prism en GitHub

Linaje de implementación y carácter del proyecto

Lecturas relacionadas

1 comentarios

 
GN⁺ 1 시간 전
Comentarios en Lobste.rs

  • No entiendo qué tienen que ver las lentes con los efectos. Cada vez que el artículo menciona lentes, no parecen estar relacionadas, salvo por quedar agrupadas bajo “un truco de cinco maneras”.
    Y tampoco entiendo qué se supone que hace tick_use(). ¿De verdad esperan que el lector entienda un ejemplo tan enredado sin explicación? Unas anotaciones de tipo habrían ayudado.

    • Acá explican más sobre las lentes: https://sdiehl.github.io/prism/spec.html#86-optic-paths
      Aun así, más allá del nivel metafórico, no se ve muy bien qué tienen que ver las lentes con los efectos. El autor escribe esto:

      This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
      O sea, entiendo que la metáfora es esta: las mónadas son valores, pero los efectos no son valores sino una especie de estructura de control. Del mismo modo, las lentes son valores, pero los optic paths de Prism no son valores; son más bien estructuras de control con sintaxis hardcodeada.

  • Tendré que dedicarle más tiempo para entenderlo, pero de verdad se ve hermoso.

  • Realmente impresionante. Justamente por eso me da curiosidad que Diehl llame juguete al compilador al final del artículo. Parece una prueba de concepto exitosa que muestra un nuevo nivel de elegancia.

  • Me gustaría ver con más detalle cómo se ve en la práctica la representación intermedia call-by-push-value. En particular, me intriga cómo maneja los puntos de unión (join points).
    Ha habido papers sobre la teoría de agregar efectos a CBPV. Decir que los cálculos tienen tipos de efecto y los valores no suena bastante natural, pero no había visto algo lo bastante concretado como para aplicarlo directamente al paso de evidencias de Koka, así que es interesante.
    En general, quisiera entender cómo se posiciona frente a Koka. Por FBIP, Perceus y el paso de evidencias, claramente está muy inspirado en el trabajo de Koka, y al mismo tiempo es definitivamente distinto porque usa CBPV en la representación intermedia. Pero no me queda claro qué tan distinto es.

  • Se parece mucho a algo para lo que llevo tiempo intentando hacerme un espacio para construir. ¡Me gusta!

  • Un poco fuera de tema, pero siempre me dio algo de pena que el proyecto “write you a haskell” de Stephen se haya detenido hace unos años. Me gustaría ver una explicación de implementación a nivel tutorial para Prism.

  • Me pregunto qué tiene de “impuro” este lenguaje. Esa palabra aparece solo en el título y no vuelve a aparecer en el cuerpo.
    Como parece que todos los efectos se rastrean, una función sin efectos sigue siendo una función matemática. ¿Me estoy perdiendo algo?

    • Parece estar relacionado con usar variables mutables locales dentro de definiciones de funciones, como en la definición dada de fib. var x es una variable mutable impura, y let x es una variable inmutable pura.

  • Me parece genial que cosas que normalmente se tratan como funcionalidades del lenguaje, por ejemplo yield en el lenguaje X o throw en el lenguaje Y, se implementen como una interfaz más.
    Que se puedan construir varios flujos de control, como efectos secundarios, excepciones y continuaciones, sobre una sola abstracción es una forma interesante de replantear todo el conjunto de preguntas de diseño, y espero que ayude o inspire más exploración e innovación. Creo que volveré a mirarlo durante años para inspirarme.