search

ashleygwilliams / breakfast-repo

a collection of videos, recordings, and podcasts to accompany our morning coffee
367 stars 10 forks source link

Refinement types for haskell #82

Open steveklabnik opened 8 years ago

steveklabnik commented 8 years ago

https://www.youtube.com/embed/vQrutfPAERQ?autoplay=1&feature=oembed&wmode=opaque

texastoland commented 8 years ago

I enjoyed this talk, but Gabe's post was much easier to understand. The gist is what if fancier types could save you from a whole new class of traditionally runtime errors, at compile time? The most common example is array out of bounds access, but it could keep you from reading into unsafe memory, dividing by zero, or even verify relationships between types like monad laws! This is another way Haskell (which doesn't even have null, for that kind of error) programs can "reason about" their execution, at the cost of verbosity. Refinement and dependent types lay the conceptual groundwork for proof languages like Agda, Idris, Coq, and JonPRL.