Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to mark unreachable cases in pattern matching

Tags:

haskell

What is the standard way to "mark" unreachable cases in pattern-matching expression? For example, with Aeson, I have Value and need to unpack it. I do it with pattern matching and I know that it's Object and it's not Array, String, Number, etc, because I created it. So, I will have case like _ -> something. What must be something? I mean standard Haskell, not LiquidHaskell approaches :) Is it something like error "Internal error" or something else?

like image 360
RandomB Avatar asked Mar 27 '18 14:03

RandomB


1 Answers

Having impossible constructors is a common occurrence in Haskell and can/is handled one of two ways depending on the situation and the style. Many developers, especially those who favor a Haskell 98 style of code, will simply indicate the impossible cases via an error:

data SumType1 = ConstrA | ConstrB | ConstrC

anyConstr :: SumType1 -> Int
anyConstr ConstrA = 1
anyConstr ConstrB = 2
anyConstr ConstrC = 3

onlyConstrA :: SumType1 -> Int
onlyConstrA ConstrA = 1
onlyConstrA _ = error "Impossible: internal error, passed wrong constructor."

However, this is both unsatisfying and requiring the developer to ensure safety when the compiler is capable and much more reliable. The common solution is to use a type that can only represent ConstrA. You could have the SumType1 be a sum of two types one of which has a field that is "ConstrAType" but that sort of refactoring can be really draining. Sometimes I prefer a GADT solution:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data SumTag = A | Anything
data SumType (a :: SumTag) where
     ConstrA :: SumType A
     ConstrB :: SumType Anything
     ConstrC :: SumType Anything

doAnything :: SumType a -> Int
doAnything ConstrA = 1
doAnything ConstrB = 2
doAnything ConstrC = 3

onlyConstrA :: SumType A -> Int
onlyConstrA ConstrA = 1

Now the function onlyConstrA has a type that clearly shows (when considered in conjunction with the data declaration) it can only be applied to the ConstrA constructor. At the same time we haven't lost any power, for example doAnything doesn't need to consider a hairy bisection of the original SumType1 into various types - the constructors are all from the same original type.

like image 160
Thomas M. DuBuisson Avatar answered Nov 10 '22 21:11

Thomas M. DuBuisson