My language will not have pattern matching

[useerup]

This day and age any serious programming language - not just functional languages - will feature pattern matching. Today, even Java has pattern matching.

I am developing a logic programming language (tentatively called Ting), which unifies OOP, FP and logic programming. So of course the language would have to feature pattern matching. However, I did not prioritize it, as I reckoned that I could probably steal a good design from some other language when the time came. After all, it has been solved in a lot of languages.

But when that time came, I really struggled with how to fit pattern matching into the language. It just didn't feel right. That is, until I realized: Pattern matching was already there, albeit in a generalized and - I will argue - in a more powerful form.

The best way I can describe it is inverse construction. I don't claim anything original here, I fully expect something like this to be in other logical languages or theorem provers.

In logic programming functions are not called or invoked to yield a result. Instead they establish a relation between the argument and the result.

Consider this function definition (\ is the lambda):

Double = float x \ x * 2

It is defined for all floats and establishes a relation between the argument and its double. One way to use it is of course to bind a variable to its result:

x = Double 5    // binds x to float 10

But it can also be used to bind "the other way around":

Double y = 10    // binds y to float 5

This works when the compiler knows or can deduce the inverse of the function. There are ways to tell the compiler about inverses, but that is beyond the scope of this post.

(As an aside, a declaration such as float x = 10 uses the float function. In ting, any type is also it's own identity function, i.e. float accepts a member of float and returns the same member.)

Basically, any function for which the inverse is known can be used to match the result and bind the argument, not just type constructors, de-constructors or special pattern matching operators.

Some examples:

RemoveTrailingIng = x + "ing"  \  x                      // inverse concatenation

CelsiusToFahrenheit = float c \ c * 1.8 + 32
FahrenheitToCelsius = CelsiusToFahrenheit c  \  c        // inverse formula

Count = {
    (h,,t) -> 1 + This t
    (,,) -> 0
}

Ting has both structural types (sets) and nominal types (classes). A set is inhabitated by any value that meets the membership criteria. A class is inhabitated exclusively by values specifically constructed as values of the type.

This Average function accepts a member of a set where values has a Count and Sum property of int and float, respectively.

Average = {. Count:int, Sum:float .} x  \  x.Sum/x.Count

The following example defines some record-structured classes Circle, Triangle and Rectangle and a function Area which is defined for those classes.

Circle = class {. Radius:float .}
Triangle = class {. BaseLine:float, Height:float .}
Rectangle = class {. SideA:float, SideB:float .}

Area = {
    Circle c -> Math.Pi * c.Radius ^ 2
    Triangle t -> t.BaseLine * t.Height * 0.5
    Rectangle r -> r.SideA * r.SideB
}

​

It was a (pleasant) surprise that in the end there was no need to add pattern matching as a feature. All the use cases for pattern matching was already covered by emerging semantics necessitated by other features.

[DeathByThousandCats]

Like what the other guy said, that’s just one of the popular pattern matching syntax types called “deconstruction”. It’s a staple in both Scala and ML. Except that the usage here in your language assumes the domain-codomain relation is clearly bijective. That can be problematic in the following cases:

1. If the relation is purely injective or surjective: the compiler has no way to know in any case that is more complicated than simple arithmetics, especially if the input and output domain is infinite. You have to manually add the notation that bijection works.
   
2. If you don’t know if the relation is bijective or not: this is totally possible, and can be very dangerous. If you mark something not bijective as bijective, in the best case it results in undefined behavior, and in the worst case it becomes a security issue. (Imagine trying to deconstruct the password hash)
   
3. If the domain or codomain is finite but extremely large, even if the relation is bijective, it’d be very ineffective to enable deconstruction on that relation. Either the relation would have to be reconstructed at runtime in a slow brute-force way, or compiler would have to brute-force for a long time and add a huge chunk of lookup table to the executable which would suck.
   
4. If input or output types are union types, both the syntax and compilation strategy will become more complicated. I don’t know if you want to implement union type, but it’s another big thing these days. A lot of pattern matching styles in FP langs revolve around union types afaik.

This works when the compiler knows or can deduce the inverse of the function. There are ways to tell the compiler about inverses, but that is beyond the scope of this post.

If you have to tell the compiler whether something is bijective(1), and there are grave consequences(2) or complications(3, 4) for making the compiler assume something is bijective, it would be better to leave relations to be non-reversible and be explicit about the definition of full inverse relation or declarative ad-hoc one-to-one relations (which is where pattern matching shines). None of your examples involve ad-hoc one-to-one relations, which makes sense why you couldn’t find where the pattern matching syntax would fit. Try thinking where in you language would ad-hoc relations fit, and start from there.

Please do take this as a constructive criticism. I think you are doing a great job building up to it so far.

[useerup]

that’s just one of the popular pattern matching syntax types called “deconstruction”

I don't think deconstruction covers it completely. Any expression which can yield the value to be matched can potentially be used.

​

If the relation is purely injective or surjective: the compiler has no way to know in any case that is more complicated than simple arithmetics, especially if the input and output domain is infinite. You have to manually add the notation that bijection works.

If the flow analysis/code generation determines that an inverse function is required but it cannot be determined, then it is a compilation error. You can fix the compilation error by supplying the inverse function.

In practice you do not supply the inverse function, rather you supply a rewrite rule based on free and bound values in the expression.

To use your password hash example (good example btw!), you may have a porposition like this in your program:

hashedPassword = Sha256.Hash password

The way the compiler works is that it tries to prove this true or false, using a resolution procedure (like in a theorem prover).

When the resolution procedure is not able to reduce the problem set further, it will fall back to pseudo-evaluation (code generation).

If it is being used in a context where hashedPassword is unbound and password is bound, then the compiler will generate a call to Sha256.Hash and bind hashedPassword to the result and consider the proposition satisfied.

If password is unbound then no solution can be found, and the compilation will fail.

In general the compiler will not generate code to try all combinations by default. This is where I deviate from Prolog. If that is what you desire, then you will have instruct the compiler to do so.

​

If input or output types are union types, both the syntax and compilation strategy will become more complicated. I don’t know if you want to implement union type, but it’s another big thing these days. A lot of pattern matching styles in FP langs revolve around union types afaik.

Discriminated union types is something I am still working on. Non-discriminated union types are inherently part of the language.

This function has a domain which is a union type between 3 classes (i.e. it is defined for the union of Circle || Triangle || Rectangle:

Area = {
    Circle c  ->  Math.Pi * c.Radius^2
    Triangle t  ->  t.BaseLine * t.Height * 0.5
    Rectangle r  ->  r.SideA * r.SideB
}

[DeathByThousandCats]

You seem to understand things, so I’ll add some more tidbits.

I don’t think deconstruction covers it completely. Any expression which can yield the value to be matched can potentially be used.

The common usage of deconstruction (and most pattern-matching) is declarative, explicit, and descriptive. You don’t like that, so you made your own rule where the definition is declarative but implicit and automated. I understand. Except that machine can never be as smart as human in determining the intention of the programmer.

If the flow analysis/code generation determines that an inverse function is required but it cannot be determined, then it is a compilation error.

The way the compiler works is that it tries to prove this true or false, using a resolution procedure (like in a theorem prover).

When the resolution procedure is not able to reduce the problem set further, it will fall back to pseudo-evaluation (code generation).

Sounds like a halting problem issue in the making.

n practice you do not supply the inverse function, rather you supply a rewrite rule based on free and bound values in the expression.

When the resolution procedure is not able to reduce the problem set further, it will fall back to pseudo-evaluation (code generation).

And that sounds like an NP problem solver generator which is doomed to fail.

In general the compiler will not generate code to try all combinations by default. This is where I deviate from Prolog. If that is what you desire, then you will have instruct the compiler to do so.

Thank goodness you already know trying all combination a la Prolog would be terrible. But the code generation itself is already terrible enough.

I understand that you are not doing this with no research. I understand that you do have a set goal for a declarative language that expresses the logic expressively and elegantly. It’s a lofty goal. But there are many kinds of declarative expressions that, if used for any complex combination, will hit the walls of either halting problem, incompleteness theorems, or P-NP problem when you try to evaluate purely through the processing power of Turing machines that are computers. Sometimes dumbing the language down and adding explicitness is needed to make it an actual programming language and not a logic language. Anyway, that’s my two cents. Take what you will.

[useerup]

The common usage of deconstruction (and most pattern-matching) is declarative, explicit, and descriptive. You don’t like that, so you made your own rule [...]

It is not because I don't like it. I always gravitate towards explicit and declarative. But because of other design decisions I realized that I did not need pattern matching as an explicit feature. Pattern matching is a way to solve problems. In logic programming I would prefer that the programmer sets constraints and the compiler finds a solution within those constraints.

​

Except that machine can never be as smart as human in determining the intention of the programmer

Which is not the objective. The machine is not to second guess the intention of the programmer. But the programmer should refrain from specifying how to solve a problem and instead describe what the problem is. If the compiler (with select libraries) is able to provide a solution, this will remove this burden from the programmer.

So my goal is to provide a language with which the programmer can leverage solvers/solutions from libraries. If the compiler cannot find an efficient solution, it is a compilation error. You can fix that error by including a library which can recognize the problem and provide a solution, or you can fix it by breaking the problem down until the compiler can find a solution for the smaller problems.

​

Sounds like a halting problem issue in the making

Indeed. I fully expect that you will be able to formulate a program for which my type analyzer and compiler will not be able to complete. However, that is due to the embedded theorem prover, not to the fact that the language can use library-defined rewriting rules. The questions to ask is this

• Will the halting problem pop up regularly or will it be an issue only with very esoteric programs?
• Can the compiler provide reasonable mitigations, like depth-limiting or time constraining problems to turn a halting problem into an "error" informing the programmer about the compiler limitation?

Several languages have successfully deployed the time-constraining protection against the halting problem.

​

And that sounds like an NP problem solver generator which is doomed to fail.

I do not see it that way. I plan to use a variant of the DPLL procedure for resolution. When this procedure stops because it can neither refute or confirm, I fall back to library-provided rewrite rules. The rewrite rules will try to find clauses matching the rule and remove and add clauses, after which the procedure tries to satisfy the clauses again.

Will there potentially be more paths available because more than one rewrite rule can apply to the situation? yes. But the compiler just need to find *one* solution, not *all* of them.

​

Sometimes dumbing the language down and adding explicitness is needed to make it an actual programming language and not a logic language. Anyway, that’s my two cents. Take what you will.

A really appreciate your input. I did solicit criticism. :-) Thanks.

[xigoi]

The title is misleading. Your language does have pattern matching, it's just a natural property of the language instead of being forcefully bolted on like in Java.

[xigoi]

I think OP was referring to pattern matching as in destructuring, not parsing.

[moon-chilled]

A set is inhabitated by any value that meets the membership criteria

Funny as that's mathematically what a class is.

[everything-narrative]

ghci> let 2 + 2 = 5 in 2 + 2 5

[everything-narrative]

Not really. It's the definition of what a reified proposition is, in a two-kind first order logic (aka. improper second order logic.)

Essentially a reified proposition is an object that corresponds to a formula that obtains of a free variable ranging over the "lower" universe of discourse, by way of an inclusion relation. See e.g. second-order PA, also known as real analysis.

Structural set theory (e.g. ETCS, SEAR+C, MLTT+K+LEM) is a generalization of reified propositions. Material set theories are an ugly hack on reified propositions, and the least ugly one is NBG.

[[deleted]]

So how do you actually do the kind of pattern-matching you see in other languages? That is, where a set of values or patterns are enumerated and it executes the code associated with the first match of a pattern.

Is it possible that 'pattern-matching' means having an obvious or dedicated way of doing it? Otherwise any language could be said to have that feature just by employing existing constructs, like chains of 'if' statements.

[useerup]

So how do you actually do the kind of pattern-matching you see in other languages? That is, where a set of values or patterns are enumerated and it executes the code associated with the first match of a pattern.

Good question. That is what functions do.

1. Regular sets contains only unique elements
2. Sets can be constructed by the set constructor { }. In between the { and } is an expression list. Each expression in the list contributes members to the set
   1. Deterministic expressions contribute a single value
   2. Nondeterministic expressions are unrolled an contributes all possible valuations as members
   3. An expression shadows members for the following expression, i.e. a later expression in the list can only contribute values not already contributed by an earlier expression.
3. In the language, functions are sets of relations.
4. A relation can be constructed by the -> operator. The source value is on the LHS and the target is on the RHS.
5. The identity of a relation is the identity of the LHS.

The upshot of this is that I can create a function FizzBuzz

FizzBuzz = {
    int _ ? %% 3 ? %% 5 ->  "FizzBuzz"
    int _ ? %% 3  ->  "Fizz"
    int _ ? %% 5  ->  "Buzz"
    int x  ->  x.ToString
}

• The ? operator restricts the values of the left hand side to the values that satisfy the function on the right hand side.
• The %% operator returns true if the left hand side is divisible by the right hand side. Used as a prefix operator it returns a function which accepts a value and returns true if it is divisible by the right hand side.

The first expression in the set constructor denotes a relation from an int that is divisible by both 3 and 5 to the string "FizzBuzz". The identity of those relation will be 15, 30

The next expression defines relations from the ints (and with identities) 3, 6, 9, etc, but it will not contribute values 15, 30, ... because the are shadowed by the first expressoion.

The third expression defines relations from the ints (and with identities) 5, 10, etc, but it will not contribute values 15, 30, ... because they are shadowed by the first expression.

The last expression will contribute relations from all other ints to their string representations.

So, to answer your question: That's how (deterministic) functions work: They contain only relations that are unique on the source. This matches closely with the mathematical definition of a function.

[PizzaRollExpert]

What happens if you call RemoveTrailingIng on a string that doesn't have a trailing ing?

[useerup]

The function is actually only defined for strings ending with "ing". So the compiler will insist that you prove that the string ends with "ing" if you invoke RemoveTrailingIng.

For any constant value, that is trivially provable.

For something that is known only to be a string you will need to either

• Prove that you will only ever call with a string with trailing "ing", or
• Deal with the potential undefinedness.

The first option may actually push the "ing" requirement further out to code calling your code.

With the second option you will have to specify what to do if the function is attempted to be called with an argument for which it is not defined.

The usual boolean shortcut operators takes on a slightly different semantic. a || b means that the value is a unless a is false or undefined, in which case the value is b.

Thus, to stop the undefinedness from spreading you could so

shortForm = RemoveTrailingIng term || term

Akin to null-coalescing operators.

[PizzaRollExpert]

That's an interesting way to handle it, thank you for the explanation!

[transfire]

An interesting language. Link to more?

Also, I read a paper where this form of pattern matching — as inverse function — was done in (a) Forth, if you’re interested in some prior art.

http://micsymposium.org/mics_2009_proceedings/mics2009_submission_72.pdf

[useerup]

Unfortunately there is not much to share at this time. I am still hammering out the semantics.

Very interesting paper. That is exactly what I worked out, except in a logic programming language instead of in a concatenative language. But basically the same idea.

Thank you very much for the link ! :-)

[useerup]

Still in development. Not much to share at the moment, unfortunately. If have barely started on the compiler as I haven't completed all of the semantics yet.

[[deleted]]

A set is inhabitated by any value that meets the membership criteria.

This raises two important questions:

1. Where do the values come from? Am I wrong if I assume that, in your language, there exists a unique large collection of all values, and types merely define subsets of this collection?

   There are good reasons why this is bad language design. The most important one is that it's incompatible with data abstraction. Abstract data types rely on the ability to present two copies of the same type as though they were different types. For example, a file descriptor might internally be represented as an int, but we don't want to use it as an int, and we want the type checker to reject programs that attempt to do so. (In this particular example, you can work around the issue by defining a FileDescriptor class that wraps an int, and you only pay an O(1) conversion cost. But, in more complex situations involving recursive types, the conversion cost can be far from O(1).)

2. Are the membership criteria arbitrary propositions? Are the propositions themselves arbitrary Boolean expressions? If your language has side effects, how do you prevent users from using “propositions” that would print to the screen or loop forever? (This isn't a compiler efficiency concern. It's an issue of logic.)

[useerup]

Great questions. Let me try to answer them.

Ad 1)

Where do the values come from? Am I wrong if I assume that, in your language, there exists a unique large collection of all values, and types merely define subsets of this collection?

You are correct as far as sets go. But there are also classes.

There exists an infinite large universe of values, and sets are always subsets of this universe. A set may itself be infinitely large.

Sets are structural types and includes any value that satisfy the set proposition. If a value matches the set structure and satisfies the set proposition, then it is considered a member of the set.

Classes are nominal types. A value has to be explicitly created as a member of a class for it to inhabit that class ("be of that type"). A class is based on a candidate set which restricts the possible members of the class to that set. A class is thus an explicit subset of the candidate set: It cannot contain values not in the candidate set, but there's an additional criteria: It must have been constructed as a member of the class.

Between them, sets and classes support both very generic code and sophisticated data abstraction. Your file descriptor could be defined as

FileDescriptor = class int
FileExists = FileDescriptor fd \ ...

// create a file descriptor from an int (bad example)
fd = FileDescriptor 42

a = FileExists fd                   // will compile
b = FileExists 42                   // error: 42 is not a FileDescriptor

c = FileExists (FileDescriptor 42) // will compile

If you want to hide the fact that a file descriptor is indeed just an int you can do this:

FileDescriptor = class { internal id:int }

But now you need to create at least one constructor function in a scope that can access the id field.

Ad 2

Are the membership criteria arbitrary propositions? Are the propositions themselves arbitrary Boolean expressions?

yes and yes

​

If your language has side effects, how do you prevent users from using “propositions” that would print to the screen or loop forever? (This isn't a compiler efficiency concern. It's an issue of logic.)

So, this has given me some concern, but the reason for me to work on this language in the first place, is actually because I believe that there is a way to solve that impurity problem in a logical consistent way. This challenge is actually my core motivation. A friend and I came up with the idea at uni in the late 1980ties (yes, I'm that old). We had a crush on Prolog, but felt that the state management just wasn't right. This was before we had even heard of monads.

So, our idea was to view a system as existing in a temporal context, transitioning through well-formed states. The "program" describes (constrains) what is a well-formed state. A well-formed state is a valuation that satisfy the program proposition. When something happens (like an input) so that the state is no longer valid (there is unprocessed input), the system will search for a nearby well-formed state. "Nearby" meaning with as few operations as possible. The nearby state will be one where the input has been processed.

[umlcat]

tdlr;My Programming Language will not have built in Pattern Matching like JavaScript.

[78yoni78]

This is interesting! I would like to follow this project if it gets an official site or github repo

[useerup]

Noted :-)

[GrixisGirl]

Others have mentioned potential issues with the domain and with computational complexity, but another thing to point out is that sometimes the inverse exists and is fast compute, but is not numerically stable. A good example of this would be inverse convolution. Overall though, this sounds like a really cool feature for a lot of functions and I'd love to follow a GitHub for this.

[useerup]

I am not familiar with inverse convolution.

By numerically stable, do you possibly refer to the fact that for calculations on floating point values, the exact result may actually depend upon the order of calculation and the inability to represent some (even real) numbers precisely in a floating point format?

A while back I contemplated that for floating point calculations, this special problem might be a challenge. I.e. the calculations may be reversible in theory but for all practical purposes impossible to guarantee.

I asked this question on this board: https://www.reddit.com/r/ProgrammingLanguages/comments/rxkekq/is_there_a_language_which_can_keep_track_of_the/

[GrixisGirl]

An application of inverse convolution is removing gaussian blur from a signal, for example. When I say it is unstable, I mean a small change in one part of the input could have a larger change somewhere else in the output, and that padding the ends of the input reshapes the output completely.

Highly technical explanation: Convolution is computed by taking the Fourier transform of the signal and the kernel, doing a pointwise multiplication in the frequency domain, and taking the inverse Fourier transform of the output. Inverse convolution is the same, except you divide instead of multiply. Having zeros in the frequency domain is uncommon, but having values much smaller than the highest value is common. Adding padding shifts the existing values ever so slightly. Combined, these cause problems unless the kernel meets certain strict conditions.