The Mastermind behind Refinement Types by Jorge Mayoral & Juanjo Madrigal
Lambda World 25
•
35m
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.
Up Next in Lambda World 25
-
Sketching streams with aquascape by Z...
Functional streams are a vital tool in any ecosystem. They can simplify the code for webservers, event loops, and data-intensive applications. But they are notoriously difficult to understand. In this talk, we'll explore a mental model of stream execution in fs2, a functional stream processing li...
-
From Exception Hell to Typed Bliss: R...
Error handling often turns into a production nightmare: monitoring alerts triggered by invalid user input, critical issues lost in log noise, and users abandoning forms after fixing one error at a time. Meanwhile, teams debate whether functional programming solutions are worth the steep learning ...
-
Starship Enterprise: Functional Progr...
Practicing functional programming inside a Fortune 100 enterprise can feel like flying the Starship Enterprise through asteroid fields of legacy code and bureaucracy. This talk shares hard-earned lessons from the Information Engineering team at JPMorganChase, which runs a production Scala codebas...
