Use (:>) in favor of Cons

[kleinreact]

We currently offer the Cons constructor and the (:>) pattern synonym for vector construction. They slightly differ in their type signature and implementation, which can cause some code to work with one but not with the other and the other way around (cf. #2913).

While the pattern synonym was necessary in the past to work around some GHC issues, these original problems are not not present with modern GHCs any more. Hence, it is desirable to favor the direct usage of the data constructor over the pattern.

Note that there are some conditional cases, where the currently differing type signature of the pattern may lead to less need for type annotations or explicit pattern matching on the constructor. This can be considered a side effect of the particular setup of the signature, which comes at the price that some code, which would check by using the data constructor instead, won't check with the pattern on the other hand. However, just requiring a bit more of annotation is a reasonable invest, as it usually leads to cleaner code. Consider for example this test case, that needed to be fixed for this change, where the resulting code resolved to be even easier to read than before.

In particular, the PR introduces the following changes:

• It fixes the type signature of the pattern synonym to align with the one of the data constructor.
• It swaps the names of (:>) and Cons. The use of (:>) is more popular than Cons. Almost all our examples use it, which makes it to be favored in comparison to Cons.
• After the name swap, the pattern is the only remaining definition using the name Cons.
• The resulting Cons pattern synonym is marked as deprecated, which will lead to only a single operation in the future.

Still TODO:

• Write a changelog entry (see changelog/README.md)
• Check copyright notices are up to date in edited files

[martijnbastiaan]

One of the reasons we couldn't remove the pattern synonym last time is that lazy pattern matches didn't work on GADTs. Is that still the case?

Edit: if it is still the case, we could add an entry to the changelog saying users could use ViewPatterns to get the old behavior back. E.g., they would rewrite:

f ~(a :> _)

to

f (lazyV -> (a :> _))

[DigitalBrains1]

Will this be a squash merge? Could you squash all commits and give it a good commit message? GitHub doesn't allow us to review the merge itself for some unfathomable reason, so I like to see the final product during review.

[martijnbastiaan]

@kleinreact We talked about this a while ago, but I can't remember the conclusion. I think you said lazy patterns still work right? If so, is there anything blocking this PR that you know of?

[kleinreact]

Lazy pattern still can cause problems (cf #2913 (comment)), which is why I for example also needed to change the type signature in T1340 here. There's usually a a proper fix for these kind of issues, but it might cause some new type errors for code to arise, which just compiled fine before that change.

The problem here more are the plugins, which don't work equally well with the constraints being introduced. My hope was that we could improve the plugins in that regard first, such that our users won't observe any difference, but that's bit more work, unfortunately.

It's quite hard to estimate how much effect this particular change could have for our users.

I'm fine with just trying it out 😉.

[kleinreact]

So just to summarize my current understanding:

• Pattern matching on the currently used constructor Cons brings the constructor and the associated m ~ n + 1 constraint into scope (where m is the length of the vector and n is the length of the tail).
• Pattern matching via the (:>) pattern instead only brings some (new) m ~ n + 1 constraint into scope that, however, is not associated with the constructor.
• Lazy pattern matching won't bring the constructor into scope, which is why you get some m ~ n + 1 constraint with ~(x :> xs) but not with ~(Cons x xs).
• The m ~ n + 1 constraint associated with the constructor and the m ~ n + 1 constraint introduced by (:>) are handled differently. Either by the plugins or even GHC, as it was observed in (:>) vs. Cons #2913 (comment).

This PR associates the constructor m ~ n + 1 constraint with (:>), which is more desirable IMO. Whether a pattern for creating some new m ~ n + 1 constraint just for the lazy pattern match case is desirable or not may be a different question. I don't see any need for lazily matching, but that does not have to mean anything.

[martijnbastiaan]

Thanks for the write-up!

Lazy pattern still can cause problems (cf #2913 (comment)), which is why I for example also needed to change the type signature in T1340 here.

I've checked out your branch and tried to write a function that uses lazy pattern matches:

f0 :: Vec (n + 1) a -> Vec n a
f0 ~(x :> xs) = xs

but I get the error:

src/Clash/Sized/Vector.hs:185:6-12: error: [GHC-87005]
    • An existential or GADT data constructor cannot be used
        inside a lazy (~) pattern
    • In the pattern: x :> xs
      In the pattern: ~(x :> xs)
      In an equation for ‘f0’: f0 ~(x :> xs) = xs
    |
185 | f0 ~(x :> xs) = xs
    |      ^^^^^^^

I was under the impression that you wanted to completely remove the pattern synonym, which would make it impossible to use lazy pattern matches. Is that not the case? Edit: it seems like Cons in your branch also disallows lazy pattern matching, so I think it completely eliminates it :(.

The reason I'm hammering on this, is because if we completely remove the ability to do lazy pattern matches, we'd make it much more annoying to write circuits that "break the loop" so to speak, we'd break existing code bases, and our users would face issues like these.

[kleinreact]

I was under the impression that you wanted to completely remove the pattern synonym, which would make it impossible to use lazy pattern matches. Is that not the case?

Yes, the idea is to swap the names of (:>) and Cons and to discard Cons (the pattern synonym then) eventually.

Would missing support for lazy pattern matches be a big deal though? You still can just use head and tail instead, which are also evaluated lazily, while their usage is more explicit than the pattern synonym in terms of not introducing any new constraints.

My problem here is that the pattern does two things: (1) it rewrites the match into a view pattern over the head and tail and (2) it introduces a new constraint. (1) is fine, but (2) can cause trouble. Most use cases won't need a lazy match in the first place, so just matching on the constructor instead should be fine. In some cases you might need a lazy match, i.e., (1), but then you probably don't need (2). Hence, my recommendation is to explicitly use a view pattern with head and tail in these cases instead, to avoid the confusion caused by (2).

I think that the user needs to explicitly take care of these difference here, and really only use lazy matching, if required. Currently we introduce a potential problem with every use of :>, which, however, is not necessary in 99% of the cases.

[martijnbastiaan]

I don't see how head and tail would provide a clean transition, but we could introduce uncons. Then we would be able to write a changelog telling users to rewrite:

f ~(x :> xs)

into

f (uncons -> (x, xs))

It's still a bit more verbose, but:

1. I don't think it happens that often
2. The patch should always work?
3. We could even provide an upgrade tool through retrie

To be clear I just care about a clean, simple upgrade path for our users. There are big code bases out there. Minor changes like these just another thing on the pile of things they need to do in order to bump Clash..

[kleinreact]

I'm fine with the introduction of uncons, as it makes it explicit that the user want's to use a lazy match, like ~(x :> xs) is syntactically visible in the code, but does not suffer from the lazy pattern GADT error.

[martijnbastiaan]

In any case, I'm excited to ditch the pattern synonyms! It's always been a wart, so thanks!

[christiaanb]

The fact that we have to tell users to use lazy patterns for certain situations is already annoying enough, adding an extra step for Vec seems like going in the wrong direction when it comes to learnability and useability for the majority of our (potential) users.

I.e. my assumption is that more users will have to use a lazy pattern match for Vec than there are users who will need to write recursive functions over the structure of Vec; most of our users will get by with the existing higher-order functions.

So the status quo, where it is easy to have a lazy match on :>, is the global optimum in the design space in my opinion.

[martijnbastiaan]

I can totally see that @christiaanb. While I do think it's a wart, it's not truly a user-facing wart. Most people can go years without realizing :> is a pattern synonym..

[DigitalBrains1]

write recursive functions over the structure of Vec

Such constructions also have a nasty habit for working for vectors up to and including length 21, but not above, without raising -fclash-spec-limit. I suppose you hit the limit sooner with a bit more complex code, and such constructions are costly to normalise during HDL generation as well. I feel recursing over Vec is a feature that people should not rely on, and we should steer our users towards higher-order functions. I also think we already do this, btw.

Of course, if it works for a particular person, I won't stop them, absolutely not. It's just not what I'd recommend people use.

And thus, I'm also not very concerned with something that is already fraught with details to be a bit cumbersome to use regarding constructors and pattern synonyms.