Incomplete Pattern-matching in Haskell

Posted on August 3, 2018 by Marko Dimjašević

From Haskell’s safe-exceptions library: “[I]ncomplete pattern matches can generate impure exceptions.” This makes me think of Agda, its totality and absence of exceptions.