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

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.

Referencias básicas:

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.

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).

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.