Haskell: Why does pattern matching work for types without equality instances?

Question

I was wondering how the pattern matching in Haskell works. I am aware of this thread , but did not quite understand the answers in it.

• The answers claim that types map to boolean expressions, but how is this possible?
• Another (==) thing I got is pattern matching, more general than (==) and Eq implemented using pattern matching.

Can you tell me why match and match3 work even if I omit deriving (Eq) in the following code snippet (it is clear why match2 does not work)?

 data MyType = TypeA | TypeB deriving (Eq) match :: MyType -> String match TypeA = "this is type A" match TypeB = "this is type B" match2 :: MyType -> String match2 a | a == TypeA = "this is type A matched by equality" | a == TypeB = "this is type B matched by equality" | otherwise = "this is neither type A nor type B" match3 :: MyType -> String match3 a = case a of TypeA -> "this is type A matched by case expression" TypeB -> "this is type B matched by case expression" main :: IO () main = do (print . match) TypeA (print . match) TypeB (print . match2) TypeA (print . match2) TypeB (print . match3) TypeA (print . match3) TypeB 

Answer 1

I just want to note that data types and pattern matching (to a first approximation) are just useful, but redundant language features that can be implemented exclusively using lambda calculus. If you understand how to implement them in lambda calculus, you can understand why they do not need Eq to implement pattern matching.

The implementation of data types in lambda calculus is known as the “church coding” of them (after Alonzo Church , who demonstrated how to do this). The functions encoded by the Church are also known as the Continuation Style.

It is called a “continuation transfer style,” because instead of providing a value, you provide a function that will handle the value. So, for example, instead of giving the user Int , I could instead give him a value of the following type:

 type IndirectInt = forall x . (Int -> x) -> x 

The above type is "isomorphic" Int . Isomorphic is just a fancy way of saying that we can convert any IndirectInt to Int :

 fw :: IndirectInt -> Int fw indirect = indirect id 

... and we can convert any Int to IndirectInt :

 bw :: Int -> IndirectInt bw int = \f -> f int 

... such that:

 fw . bw = id -- Exercise: Prove this bw . fw = id -- Exercise: Prove this 

Using the continuation transfer style, we can convert any data type to the term lambda calculus. Let's start with a simple type like:

 data Either ab = Left a | Right b 

In the style of passing continuation, it will become:

 type IndirectEither ab = forall x . (Either ab -> x) -> x 

But Alonzo Church was smart and noticed that for any type with multiple constructors, we can simply provide a separate function for each constructor. Thus, in the case of the above type, instead of providing a function of type (Either ab → x) , we can instead provide two separate functions, one for a and one for b , and that would be just as good:

 type IndirectEither ab = forall x . (a -> x) -> (b -> x) -> x -- Exercise: Prove that this definition is isomorphic to the previous one 

What about a type of type Bool where the constructors have no arguments? Well, Bool is isomorphic to Either()() (Exercise: prove it), so we can just encode it as:

 type IndirectBool = forall x . (() -> x) -> (() -> x) -> x 

And () → x just isomorphic to x (Exercise: Prove it), so we can rewrite it as follows:

 type IndirectBool = forall x . x -> x -> x 

There are only two functions that can have the above type:

 true :: a -> a -> a true a _ = a false :: a -> a -> a false _ a = a 

Due to isomorphism, we can guarantee that all church encodings will have as many implementations as there were possible values ​​of the original data type. Therefore, it is no coincidence that IndirectBool has exactly two functions, exactly the same as exactly two constructors in Bool .

But how do we compare patterns on our IndirectBool ? For example, with a regular Bool we could simply write:

 expression1 :: a expression2 :: a case someBool of True -> expression1 False -> expression2 

Well, with our IndirectBool it already comes with tools to deconstruct itself. We would just write:

 myIndirectBool expression1 expression2 

Note that if myIndirectBool is true , it will select the first expression, and if it is false it will select the second expression, as if we somehow matched its value pattern.

Let's try to do the same with IndirectEither . Using regular Either , we would write:

 f :: a -> c g :: b -> c case someEither of Left a -> fa Right b -> gb 

With IndirectEither we simply write:

 someIndirectEither fg 

In short, when we write types in the style of passing a continuation, the continuations are similar to the case statements of the case construct, so all we do is pass each individual case statement as arguments to the function.

For this reason, you do not need to make any sense in Eq to match the type pattern. In the lambda calculus, the type decides what it is "equal to" by simply determining which argument it chooses from the ones given to it.

Therefore, if I am true , I will prove that I am "equal" to true , always choosing my first argument. If I am false , I prove that I am "equal" to false , always choosing the second argument. In short, the constructor "equality" comes down to "positional equality", which is always defined in the lambda calculus, and if we can distinguish one parameter as the "first" and the other as the "second", then all we need to have skill is " compare "constructors.

Answer 2

First of all, match and match3 are actually exactly the same (ignoring different lines): pattern matching in functions is disaggregated in case.

Further, pattern matching works on constructors, not arbitrary values. Pattern matching is built into the language and is independent of Boolean expressions — it simply acts directly on the constructors. This is most obvious with more complex matches, which include some suitable terms:

 f :: MyType -> Int f (A a) = a + 1 f (B ab) = a + b 

How would you rewrite these patterns in boolean expressions? You cannot (without knowing anything about MyType ).

Instead, pattern matching is done only by the constructor. Each template must be led by a constructor - you cannot write a template, for example f (abc) in Haskell. Then, when the function receives the value, it can look at the constructor of the values ​​and immediately go to the corresponding cases. This is how it should work for more complex templates (for example, A a ), as well as the way it works for simple templates that you used.

Since pattern matching only works when moving to the appropriate constructor, it does not depend on Eq . Not only do you not need to have an Eq instance for pattern matching, but having one also does not affect the behavior of the pattern. For example, try the following:

 data MyType = TypeA | TypeB | TypeC instance Eq MyType where TypeA == TypeA = True TypeB == TypeC = True TypeC == TypeB = True _ == _ = False match :: MyType → String match TypeA = "this is type A" match TypeB = "this is type B" match TypeC = "this is type C" match2 :: MyType → String match2 a | a == TypeA = "this is type A matched by equality" | a == TypeC = "this is type B matched by equality" | a == TypeB = "this is type C matched by equality" | otherwise = "this is neither type A nor type B" 

Now you have defined such equality that TypeB is equal to TypeC , but not to yourself. (In real life, you have to make sure that equality behaves rationally and matches the reflective property, but this is an example of a toy.) Now, if you use pattern matching, TypeB still matches TypeB and TypeC matches TypeC , but if you use safety expressions TypeB really matches TypeC and TypeC TypeB . TypeA does not change between the two.

Also, notice how the Eq instance was defined using pattern matching. When you use the deriving clause, it is defined in the same way with the code generated at compile time. Thus, pattern matching is more fundamental than Eq - it is part of the language where Eq is part of the standard library.

In conclusion: pattern matching is built into the language and works by comparing the constructor, and then recursively matching the rest of the value. Equality is usually implemented in terms of pattern matching and compares an integer value, not just the constructor.

Answer 3

What you are missing is that constructors in Haskell can have arguments. Tags like "yourself" are comparable on an equal footing (at least inside, behind the scenes), but full values ​​are only comparable if the constituent arguments are also comparable.

So, if you have a type type

 data Maybe a = Nothing | Just a 

then even if you can check whether the tag is of the type “Nothing” or “Just” (that is, matching the pattern with the possible value) in the general case, you cannot compare the full one, perhaps if the value is of the type “a” that is held by Just also turns out to be comparable.

 --note that your first and third examples are --just syntactic sugar for each other... matchMaybe mb = case mb of Nothing -> "Got a Nothing" Just _ -> "Got a Just but ignored its value" 

Now it should also be clear why you cannot write a match2 variant for Maybes. What would you use to test equality in the case of Just?

 matchMaybe_2 mb | mb == Nothing = "Got a Nothing" | mb == Just {- ??? -} = "This case is impossible to write like this" 

Answer 4

As I think of this, pattern matching is basically bitwise equality. It is based on types, and not on some abstract meaning of value.

Keep in mind, however, that you must say Int as

 data Int = ... | -2 :: Int | -1 :: Int | 0 :: Int | 1 :: Int | 2 :: Int | ... 

Thus, each integer has a different type.

This is why you can match Int with text 2 .

Eq goes a little further, it allows you to set things equal, which may not be bitwise.

For example, you might have a binary tree that stores sorted items. Say the following:

  AA / \ / \ BCBD \ \ DC 

It can be considered equal on Eq because they contain the same elements, but you cannot verify equality here using pattern matching.

But in the case of numbers, bitwise equality basically coincides with logical equality (with the possible exception of positive and negative floating point 0.0 ), therefore, here Eq and pattern matching are largely equivalent.

---

For the C ++ analogy, think of Eq as operator== and matching the pattern as memcmp . You can compare many types for equality simply using memcmp , but some you cannot, if they can have different representations for "equal" values.