Weakening Type Systems for Faster Prototyping

Matthías Páll Gissurarson demonstrates how to temporarily weaken type systems during prototyping and use program synthesis to fix the code.

Matti is giving a virtual talk at the UCSC Languages, Systems, and Data (LSD) lab seminar! Intended mostly UCSC LSD grad+undergrad students and faculty, I'll be talking about some recent work and some work in progress. You'll find the abstract and a link to the most recent paper below! Abstract: Types and type systems are great to provide the compiler with a partial specification of our programs, but it can often be tricky to write code that matches said specification. In this talk, I will demonstrate how we can allow developers to opt-in to a weaker type system "just get it to compile", and what we can do to "fix" the code during compilation so that it matches the specification provided using synthesis and coercions, and hint to the developer what the issue is and how they might fix it. Be sure to check out my PLAS paper for further details! mpg.is/papers/gissurarson2020short-paper-weak.pdf The plugin itself: github.com/Tritlo/writ-plugin/ Also mentioned in the video: cse.chalmers.se/~russo/publications_files/pearl-russo.pdf