De qué se trata
Somos un grupo apasionado de desarrolladores que se reúnen regularmente para explorar y aprender sobre los principios de la programación funcional. Desde las bases de la inmutabilidad y las funciones de orden superior hasta los conceptos más avanzados como los mónadas, nuestro objetivo es profundizar en el mundo de la programación funcional y aplicar estos conocimientos en nuestros proyectos del mundo real. Si te interesa descubrir nuevas formas de escribir código limpio, elegante y robusto, únete a nosotros en nuestras reuniones llenas de aprendizaje, discusiones animadas y networking entre programadores de Madrid. ¡Te esperamos!
Próximos eventos (1)
Ver todo- The Mastermind behind Refinement TypesDevo, Madrid
Cerramos la temporada de charlas en FP Madrid de la mano de Juanjo Madrigal (Devo) y Jorge Luis Mayoral (Playtomic), en la que nos hablarán de tipos refinados. Damos las gracias a Devo por acoger a nuestra comunidad en sus instalaciones.
⚠️ ¡La charla se impartirá en español! (This talk will be held in spanish!) 🇪🇸
The Mastermind behind Refinement Types
Should your function only admit positive integers? Does it always return non-empty lists?
Refinement types are wonderful: beyond typing, you can annotate the behaviour of your function values. It's a great ally for the correctness of a program, but there is fine print: obviously the wonder is not to do a check at runtime, but at compile time, and that may not be trivial.
What we need is a brain, a mastermind that takes all the conditions and validates our program. And for it to work, this mastermind has to cleverly combine many ingredients: dependent types, logic, polymorphism... a very interesting mess.
In this talk we want to present, in an intuitive way and through examples, these masterminds, the SMT (Satisfiability Modulo Theories) solvers, and the applications to the semantic enrichment of many programming languages, as is the case of Z3 solver with Liquid Haskell, and compare the approach of refinement types with that of dependent types, as happens with Idris, Agda or Lean.
