2014
Este es el sitio web del Espacio sobre temas de programación funcional, un encuentro informal que se organiza en el Departamento de Computación de la Facultad de Ciencias Exactas y Naturales de la Universidad de Buenos Aires, destinado a profundizar y fomentar el interés en temas relacionados con la programación funcional en un sentido amplio.
Durante el segundo semestre de 2014, el espacio estará proyectado como un grupo de lectura del libro Homotopy Type Theory (HoTT).
El programa Univalent Foundations es una iniciativa de un grupo de investigadores reconocidos en varias áreas (teoría de tipos, álgebra homotópica, categorías), basada en una interpretación homotópica de una variante de la teoría de tipos de Martin-Löf. Propone fundamentos para la matemática basados en la correspondencia entre proposiciones y tipos.
Organizadores - contacto
Federico Lebrón - (flip (++) . ('@' :)) "dc.uba.ar" "flebron"
Luis Scoccola - minombre.miapellido@gmail.com
Pablo Barenbaum - (λ x y. y@x) gmail.com foones
Videos grabados y procesados por Federico Lebrón y Manuel Ferrería.
Lista de correo: https://groups.google.com/d/forum/funcionaldc
Encuentros pasados
Homotopy Type Theory (cap. 3)
Jueves 30 de octubre.
Resolución de ejercicios del libro y otros. Tipos contráctiles, truncación de tipos. Definición de conjunto y, más generalmente, n-tipo.
Homotopy Type Theory (consolidación cap. 1)
Jueves 25 de septiembre.
Repaso del capítulo 1. Discusión de un ejemplo particular de la técnica de coding-decoding (demostración de ~par(1)). Codificación de deducción natural con proof terms.
Homotopy Type Theory (§§ 2.1–2.3)
Expositor: Pablo Barenbaum
Jueves 18 de septiembre.
Estructura de weak ∞-groupoid: composición e inversa de caminos. Teorema de Eckmann-Hilton. Funciones son funtores. Operador de transporte.
Homotopy Type Theory (§§ 1.7–1.12 + introducción cap. 2)
Expositor: Luis Scoccola
Jueves 4 de septiembre.
Proposiciones como tipos. Igualdad proposicional. Inducción sobre caminos e inducción "basada" sobre caminos (based path induction). Resolución de algunos ejercicios: 1.10 (función de Ackermann), 1.13 (¬¬(p v ¬p)). Introducción informal a la interpretación de la igualdad proposicional como caminos con estructura de weak ∞-groupoid. Pentágono de Mac Lane.
Homotopy Type Theory (§§ 1.1–1.7)
Expositor: Pablo Barenbaum
Jueves 21 de agosto.
Cuestiones básicas sobre la teoría de tipos de HoTT. Juicios y proposiciones. Igualdad definicional y proposicional. Universos y familias. Reglas de formación, introducción, eliminación y cómputo: funciones dependientes, productos, pares dependientes, coproductos.
- Slides
Cómo funciona un asistente de demostración
Pablo Barenbaum
Jueves 3 de julio.
Charla conjunta con el ciclo de charlas UbaCs del Departamento de Matemática.
Los asistentes de demostración ayudan a verificar formalmente la corrección de definiciones, teoremas y sus demostraciones. Hay decenas de asistentes, basados en distintos fundamentos (Coq, Isabelle, HOL Light, PVS, ACL2, Mizar, Metamath, Agda, etc.). En esta charla se hizo una introducción rudimentaria a Coq, un asistente basado en teoría de tipos.
- Transparencias de la charla
- Video de la charla
- Archivos usados para la presentación:
- Basico1.v - ejemplo básico en Set
- Basico2.v - ejemplo básico en Prop
- Naturales.v - definición de proposición inductiva
- Sigma.v - pares dependientes
- Relaciones.v - ejercicio con relaciones
- Induccion.v - length (xs ++ ys) = length xs + length ys
- Cayley.v - teorema de Cayley
- Basico1.v - ejemplo básico en Set
Theorems for free
Federico Lebrón
Jueves 19 de junio.
El tipo de una expresión provee mucha información sobre su valor. Por ejemplo, la única función posible de tipo a → a es la identidad. En esta charla se presentó el artículo Theorems for free de Philip Wadler, donde para cada tipo polimórfico se deriva un teorema que cumplen todas las expresiones de ese tipo.
Zippers y derivadas de tipos
Pablo Barenbaum
Jueves 5 de junio.
Introducción a la noción de isomorfismo de tipos. Análisis de la estructura de datos conocida como zipper, utilizada para "iterar" y "modificar" estructuras de datos de manera puramente funcional. Relación entre el tipo de los zippers y la derivada formal de un tipo.
- Transparencias de la charla
- Video de la charla
Referencias básicas:
- Conor McBride, The Derivative of a Regular Type is its Type of One-Hole Contexts
- Gérard Huet, The Zipper
Estructuras de datos funcionales
Juan Pablo Darago
Jueves 22 de mayo.
Colas puramente funcionales en O(1) amortizado y peor caso. Análisis de complejidad amortizada usando técnicas del físico y del banquero. Implementación de streams usando memoización. Evaluación lazy como requisito para lograr estructuras de datos persistentes eficientes. Vectores persistentes de Clojure (hashed array mapped tries). Finger trees.
Referencia elemental: Purely Functional Data Structures de Okasaki.
- Transparencias de la charla
- Video de la charla
Tipos dependientes en Haskell y Agda
Federico Lebrón
Jueves 8 de mayo.
Presentación de la noción de tipos dependientes en Haskell y Agda. Se ilustraron maneras interesantes de aprovechar el sistema de tipos para garantizar invariantes complejos estáticamente (en tiempo de compilación). Ejemplo interesante: tipo de datos para árboles que sólo admite instancias balanceadas (p.ej. que cumplan el invariante de un AVL).
- Transparencias de la charla
- Video de la charla
- VIdeo alternativo de la charla (grabado por Manuel Ferreria)
Continuaciones y call/cc
Pablo Barenbaum
Jueves 24 de abril.
Introducción a las continuaciones first-class y el operador de control call/cc. Codificación de estructuras de control basadas en el manejo de continuaciones: excepciones, iteradores, co-rutinas. Dos maneras de implementar call/cc: reificación de la pila de llamadas y conversión a Continuation-Passing Style.
- Transparencias de la charla
- Video de la charla
- Evaluador del cálculo-λ con let, letrec, referencias, call/cc
Funtores y mónadas
Federico Lebrón
Jueves 3 de abril.
Introducción a algunos conceptos modernos de programación funcional desde una perspectiva teórica: funtores, mónadas y funtores aplicativos. La charla se basó en las primeras secciones de la Typeclassopedia de Brent Yorgey.
- Transparencias de la charla
- Video de la charla
- Parser del cálculo-λ usando parser combinators
Introducción al cálculo lambda sin tipos
Pablo Barenbaum
Jueves 20 de marzo.
Términos, alfa equivalencia, beta conversión. Codificación de tipos de datos y funciones recursivas usando únicamente lambdas.
- Transparencias de la charla
- Video de la charla
- Intérprete gráfico del cálculo-λ