Please log in to watch this conference skillscast.
Haskell is known for its strong static typing but there are even stronger typing disciplines! Refinement types are types 'annotated' with 'predicates'. Dependent types allow terms to appear in types. Both of these disciplines allow the programmer to be more specific. A classic example is defining a type of lists of length 'n'. Both of these disciplines allow the programmer to prove that some function is valid on all possible inputs, a much stronger proof of correctness than a battery of tests. How are these two disciplines different? How do they work? How can you experiment with them? I'll answer these questions and demonstrate with examples in A Brief Introduction to Refinement Types and Dependent Types.
You can also view the slides from this talk here.
YOU MAY ALSO LIKE:
- Haskell Fundamentals (2-Day Course) with Alejandro Serrano (Online Course on 8th - 9th March 2021)
- Haskell Fundamentals (4-Day Course) with Alejandro Serrano (Online Course on 19th - 22nd April 2021)
- Haskell eXchange 2021 (Online Conference on 16th - 17th November 2021)
- Theorems for Free (SkillsCast recorded in November 2020)
- Comparing Strict and Lazy (SkillsCast recorded in November 2020)
Stronger Types! : A Brief Introduction to Refinement Types and Dependent Types (Lightning Talk)
Eric Bond a software engineer and functional programming consultant at 47 Degrees in Seattle by day.. type theorist and proof engineer by night. He spends his free time reading papers in formal verification and categorical semantics. Scala pays the bills but his heart belongs to Agda, Haskell, and Coq.