Ghost Hunting the Perfect API (with departed proofs)
Details
Join us for a virtual meetup with Anthony Sheldon! Anthony will be giving a talk about the ghosts of departed proofs—how spooky! See his abstract below.
NoRedInk is kindly hosting this virtual event! Software Engineer Katie Hughes will be joining us and can share details about NoRedInk, which is one of the SF companies that uses Haskell!
Zoom link: https://noredink.zoom.us/j/95024829806
Talk title: "Ghost Hunting the Perfect API (with departed proofs)"
Talk abstract:
Library authors are often faced with a design choice: should a function with preconditions be implemented as a partial function, or by returning a failure on incorrect usage? Neither option is ideal. Partial functions lead to frustrating run-time errors. Failure must be checked at the use-site, placing an unfair tax on the users who have ensured that the function’s preconditions were met. What if you could achieve many of the benefits of dependent and refinement types, whilst only requiring some minor and well understood extensions to haskell2010? TL;DR: You can use the same rank-2 types trick used in the ST monad to get the compiler to check a surprisingly wide range of API invariants and preconditions.
Agenda:
- 2:00pm: Welcome, sort out any technical difficulties
- 2:10pm: NoRedInk introduction
- 2:20pm: Ghost Hunting the Perfect API (with departed proofs)
For networking please join the #sfhaskell Slack channel here: https://www.sfbayareatech.xyz/
To ask questions during the meetup, please use the Zoom chat feature,
Link to the upcoming Scala meetup: https://www.meetup.com/reactive-systems/events/270368083/
UPDATE: Due to a scheduling conflict, we had to move the event from Thursday evening to Saturday afternoon. We apologize for any confusion!