17 noticias
El tipo `!` (never) se añadió recientemente a Rust como anotación válida en cualquier posición del código, con su estabilización prevista para Rust 1.100. Aunque suele presentarse como el tipo bottom de la teoría de tipos, el artículo explica que en Rust se trata en realidad del tipo vacío, no del t
En 1992, Leslie Lamport, conocido por sus trabajos en sistemas distribuidos y por haber creado LaTeX, publicó una nota titulada "Types Considered Harmful", en la que defendía que los lenguajes de especificación debían basarse en formalismos no tipados (una suerte de teoría de conjuntos) en lugar de
Alcides Fonseca sostiene que los sistemas de permisos actuales de los agentes de inteligencia artificial —ya sean permisos granulares por solicitud o un modo “yolo” sin restricciones— son insuficientes para proteger datos críticos. El problema se agrava con el llamado “trío letal”: cuando un agente
Este ensayo, escrito como complemento de un texto anterior titulado 'Type Theory Weary', cuestiona la necesidad de tratar los tipos como un constructo especial dentro de la informática y la lógica. El autor sostiene que los sistemas de tipos surgieron históricamente para resolver problemas que en su
Serokell publica la quinta entrega de su serie sobre tipos dependientes en Haskell, centrada en el trabajo que Vladislav Zavialov y su equipo desarrollan en el compilador GHC. El artículo detalla tres contribuciones principales y varias mejoras secundarias que acercan Dependent Haskell a una realida
Principia Mathematica, la obra monumental de Alfred North Whitehead y Bertrand Russell publicada a partir de 1910 por la Cambridge University Press, es célebre por la extensión de sus demostraciones —se dice que emplea unas mil páginas en probar que 1+1=2— y por un nivel de detalle concebido para de
Un reciente intento de refutar la conjetura de Collatz, cuya presunta refutación fue verificada en el asistente de pruebas Lean y contrastada con el comprobador independiente Nanoda, resultó ser erróneo: la demostración aprovechaba un fallo en el núcleo de Lean y Nanoda tampoco detectó el problema.
Los verificadores de tipos no solo evitan errores de programación como sumar cadenas y enteros, sino que además sustentan los asistentes de demostración, lenguajes como Lean y Rocq que validan matemáticamente teoremas. La base de esa capacidad es la correspondencia de Curry-Howard, que establece una
Este artículo presenta una técnica para codificar tipos existenciales en Haskell que permite que aparezcan 'desnudos' en las signaturas de tipo, sin necesidad de envolverlos en un constructor GADT ni recurrir a la transformación CPS (estilo paso de continuación). La codificación se apoya en funcione
El vídeo del canal Logan Smith analiza Verse, el lenguaje de scripting que Epic Games está desarrollando para sustituir al sistema de Blueprints en Unreal Engine 6. El autor parte de una pregunta provocadora: ¿tiene sentido aprender un nuevo lenguaje de programación en plena era de la inteligencia a
En la era de la generación de código asistida por inteligencia artificial, se ha extendido la percepción de que el dominio profundo de los lenguajes de programación ha quedado obsoleto. ¿Para qué invertir años en entender sus matices si una IA puede producir código en cualquier lenguaje bajo demanda
Counterexamples in Type Systems es una obra de referencia compilada por Stephen Dolan —con colaboraciones reconocidas de Andrej Bauer, Leo White y Jeremy Yallop— que reúne treinta y un contraejemplos cuidadosamente seleccionados para ilustrar los puntos delicados, las trampas y las excepciones de lo
Este artículo explica, desde cero y con ejemplos, cómo funciona la inferencia de tipos para los registros anónimos, una pieza que el autor considera clave y todavía недостаточно aprovechada en los lenguajes estáticamente tipados. Un registro anónimo es aquel que no necesita una declaración de tipo p
Los registros anónimos —estructuras de datos con campos identificados por nombre que no requieren una declaración previa de tipo— son habituales en lenguajes dinámicos como JavaScript (objetos), Python (diccionarios), Ruby (hashes) o Nix (attribute sets), y también aparecen en el formato JSON. Sin e
¿Cómo se explica un concepto avanzado de informática a un niño de seis años? Este ensayo, escrito en primera persona por un académico vinculado a la programación funcional, narra una conversación espontánea con su hijo menor mientras leía la tesis de habilitación de Janis Voigtländer sobre teoremas
GHC, el compilador de Haskell, incluye una extensión llamada ApplicativeDo que traduce bloques do-notation en operaciones aplicativas (<*>) cuando no existen dependencias entre instrucciones, habilitando paralelismo automático. Sin embargo, el algoritmo que produce la planificación óptima de esas op
Este artículo técnico explora una peculiaridad en el sistema de tipos de Rust y cómo un intento de emular tipos de orden superior (HKTs) llevó a un error de desbordamiento en la evaluación de requisitos de traits, causando que el compilador fallara. El autor, en su intento de crear un lenguaje de sc