Another approach to Pattern Synonyms in Purescript

Making a Smart Constructor in Purescript is pretty easy.

One can simply make a function which mimicks the type signature of a constructor, and then it can be applied as a constructor.

This got me wondering why most functional languages, and purescript specifically can’t/won’t allow similar functionality for pattern matching?

What if destructors were just functions too, instead of this special construct that can only be used when pattern matching? What if, then as well, any function which fit this pattern could be used as a destructor? This could completely make redundant the addition of pattern synonyms, because all pattern-like functions would already be synonyms!

I’d love to get some feedback on whether the idea is a good one, and why this/other languages do/do not adopt this approach, since on my search I haven’t found any.

As for the encoding to be used for destructors, I personally prefer the Scott encoding based on simplicity, and how similar it looks to pattern matching already IMO. It would need to be extended, however, to allow for the naming of the variants in the pattern. However I believe this is easily achievable using Purescript’s records. Something like this.

If a data declaration were defined like this

data MyType a = A | B Int String | C a (MyType a)

The generated destructor’s signature could look like this

MyType' :: forall a b. { A :: b, B :: Int -> String -> b, C :: a -> (MyType a) -> b } -> b

And anyone willing to make a smart destructor would simply have to implement a function with a similarly constructed signature, and then it could be used within pattern matching naturally.

For example a smart destructor coded like this:

MySmartDestructorForEither' : :  forall a b c. { Left :: a -> c, Right :: b -> c } -> c

Could be used like this:

case myVal of
    Left a -> ?hole
    Right b -> ?hole

I’d love some feedback on the idea/proposal, and/or general thoughts on why this idea isn’t normally implemented, in Purescript or other Languages!

Can you walk me through how this would be used and give an example of a benefit it would have over pattern matching? I’m having trouble seeing the difference between this and pattern matching

The idea would be to make pattern matching first-class in the language, in the sense you could have “smart destructors” the same way you have “smart constructors”. Technically you can do this nowadays using this encoding, but it’s a fundamentally different syntax. The idea would be to make native pattern matching and this encoding one and the same.

For example a Queue is often implemented as a pair of lists, yet often it is useful to “uncons” from it, as if it were a regular list.

This can be accomplished with a function Queue a -> Maybe (Tuple a (Queue a)), whose result can then be pattern matched on.
This is then isomorphic to a function Queue a -> (forall b. (a -> Queue a -> b) -> b -> b), which allows you to directly “pattern match” on the cases by supplying continuations for each case.

However this cannot be exposed directly as pattern matching, since the uncons operation also performs internal operations apart from just destructing the arguments, as such this forms the closest thing to a “smart destructor” we have, but the syntax to use it is fundamentally different than that of pattern matching. This proposal would allow all such “smart destructors”, to be automatically used as patterns, allowing for multiple different “views” of the same datastructure.

Furthermore another example is regular pattern matching. The function that destructs a data structure is not directly exported by a data type, rather a constructor function is exported which “magically” can also destruct values using special syntax, and which cannot directly be passed around, rather needs to be recreated by making a lambda which pattern matches, and then pass that around.

This proposal would be to export destructors as their corresponding encodings, and to make all such encodings, smart or not, compatible with pattern matching.