Better infrastructure through types


  • Algebraic Data Types


    NOTE: This is an edit of an article I wrote for Functional Algebra in 2012.



  • The Unreasonable Effectiveness of Reasoning: Eliminating Bottom


    This article provides a simple code-level case study to understand how two functional programming libraries have made different trade-offs. We explore related API-level design choices in a neutral language (Scala) where we consider the ability of the consumer of the API to reason equationally about it. We demonstrate that focusing on eliminating bottom yields more reasonable (equationally) APIs.



  • Extending Syntax in Scala


    Yesterday I learned something really cool. In Idris I can just do this to extend the syntax:



  • Why Use Types?


    Types are one of the most mainstream and widespread applied formal methods in software engineering industry today. Yet I have met many accomplished and experienced practitioners in our field who do not know how to effectively use types, even in lanuages they can leverage well for this.