Introduce dan-level rank assessments (and Kata)

[DonaldKellett]

I noticed that this has been suggested multiple times before (and closed multiple times for various reasons) but I think it is finally time to consider this for real.

What I understood/considered from previous issues on this Topic

Previously, certain users advocated for opening up dan-level Kata due to the sheer difficulty of certain algorithmic Kata (e.g. toBrainfuck transpiler) which are believed to be more difficult than typical 1 kyu algorithmic Kata. Such issues were closed since the previously active Codewars administrator Jake Hoffner wanted to make dan levels distinct from kyu levels by introducing project-level Kata among other things (please do correct me if I am wrong).

What prompted me to re-open this Feature Request? How is the current situation different from previous situations?

With the swift (and sudden!) support of dedicated proof-assistant languages such as Idris and Agda, there has been a surge in theorem-proving Kata recently. While it was possible to prove very simple and straightforward statements such as A + B = B + A in Haskell using an array of GHC extensions back when Idris/Agda were not supported, the introduction of the aforementioned languages made it feasible to author theorem-proving Kata of all levels of difficulty ranging from less trivial arithmetic proofs such as 1 + 2 + ... + n = n * (n + 1) / 2 to properties of lists and list operations and even research-level academic topics such as Cubical Type Theory (which I have absolutely no idea what it is about).

There has been a debate as to how such theorem proving Kata should be ranked. Obviously, proving even the simplest of theorems such as "flipping a binary tree twice gives back the original tree" is in no way 7-8 kyu as some have suggested since a Codewarrior who has only began learning the syntax and semantics of Idris/Agda would seriously struggle to understand deep concepts such as Curry-Howard isomorphism, let alone apply said concepts in the form of machine-checked proofs. This means that even the simplest of proofs (maybe except absurdly simple proofs such as n + 0 = n for all natural numbers n which is currently offered as an 8 kyu Agda Kata) are currently ranked starting from 4 kyu upwards.

What this means is that since even the simplest of proofs are ranked 4 kyu or above (and ought to be!), slightly less straightforward proofs requiring a bit more insight and intuition are easily ranked as 2 kyu or even 1 kyu. However, it is totally possible to author rather complex proofs on obscure academic theories such as Cubical Type Theory (a few kata on the topic which can be found in @ice1000 's authored Kata list) or properties of mathematical entities involving extremely abstract concepts such as the injectivity of the type constructor Maybe (which is totally different from proving the injectivity of an ordinary function). Such Kata are yet an entire level above those "less straightforward" proofs (e.g. List concatenation is injective? Prove it! currently ranked at 1 kyu) but under the current ranking scheme, they would all be ranked as 1 kyu at the very most. This would lead to a whole bunch of 1 kyu theorem-proving Kata of vastly differing difficulties (ranging from "quite difficult" to "insanely difficult") which could discourage Codewarriors from authoring and/or solving the more difficult ones.

The proposed solution is to open up dan-level Kata and rank assessments, at least up to and including 2 dan. Even higher dan-ranks may need to be opened up in the near future as ever more complex and abstract theorem-proving Kata are authored.

Supporting comments demonstrating the need to open up dan-level Kata ASAP

@ice1000 recently left a comment on the Maybe Injective Kata stating that it should honestly be ranked 1 dan:

---

Specifically, I would like to hear the opinions of the following people on this specific Issue:

• @ice1000
• @lwoo1999
• @kazk

Others are free to chime in as well 😄

[Voileexperiments]

Completely disagree. Let me quote my stance from gitter again:

> just because nobody on CW except a few understands proof assistant languages yet doesn't mean you're all gonna rank it blue or purple
> the same thing happened to Haskell katas too, all of them went purple when they really shouldn't
> so I'm gonna say the same old thing again and tell you all to git gud

---

There has been a debate as to how such theorem proving Kata should be ranked. Obviously, proving even the simplest of theorems such as "flipping a binary tree twice gives back the original tree" is in no way 7-8 kyu as some have suggested since a Codewarrior who has only began learning the syntax and semantics of Idris/Agda would seriously struggle to understand deep concepts such as Curry-Howard isomorphism, let alone apply said concepts in the form of machine-checked proofs. This means that even the simplest of proofs (maybe except absurdly simple proofs such as n + 0 = n for all natural numbers n which is currently offered as an 8 kyu Agda Kata) are currently ranked starting from 4 kyu upwards.

since even the simplest of proofs are ranked 4 kyu or above (and ought to be!),

That's just completely absurd. Just because someone can't handle proof assistant languages or that proof assistant languages are hard to get started (unlike, say, Python) doesn't mean it should be ranked blue. By the same logic everything should be ranked 8 dan because for complete newbies, they all look like that.

If you think about it, it has always been like this: back in 13-14 pretty much every power user is like a noob, and problems that would be yellow or blue nowadays would be blue or purple back then just because users aren't good enough. Did anyone argue otherwise that they're overranked? Anyone?

and even research-level academic topics such as Cubical Type Theory (which I have absolutely no idea what it is about)

Then... go read the papers? You're talking like you can write code in any language without reading any documentation about your language or the domain you're writing code for. That's called spoon-feeding. It's completely optional.

CW gets katas with topics of increasing span over time, and it will only get wider. It's up to you who should catch up to the meta, not instead sitting inside your comfort zone and thinking why isn't everything 8 dan already.

This would lead to a whole bunch of 1 kyu theorem-proving Kata of vastly differing difficulties (ranging from "quite difficult" to "insanely difficult") which could discourage Codewarriors from authoring and/or solving the more difficult ones.

Easy. Just deflate the ranking to make it more realistic. That's the thing we've been advocating for instead of opening dan ranking katas. I'm not sure where you get the latter from.

If you don't want ridiculous ranking on new katas, you gotta re-adjust the old ones, and it's not our fault that it's unavailable at the moment.

---

By the way, are you aware of a feature called "My Languages"? If you're only familiar with a few languages, there are no reasons to show katas of all languages, and then try tackling them anyway without avail. You're not supposed to be able to solve all katas (even if you want to ;-)). Perhaps you need to rethink about your abilities and stop thinking you're like a certain someone with name starting with a V? 😉

[FArekkusu]

What this means is that since even the simplest of proofs are ranked 4 kyu or above (and ought to be!)

Sounds more like all the people who are into theorem-proving katas are overranking everything considerably as it has been done with some of the purple Haskell katas we have (there's an Idris kata currently in Beta which ZED.CWT completed by closing holes and ranked 7 kyu, and Donald solved by reimplementing the whole thing from scratch and ranked 1 kyu - wtf?). I'd asked about this on gitter some time ago, and I was told that these katas are blue/purple because it's indeed hard to programmatically prove mathematical theorems, but after seeing this post I'm only further convinced that this whole thing is a joke, and the ranking is 100% based on the fact that this whole theorem-proving topic is very niche, and very different from typical procedural tasks we deal with on CW everyday.

Codewarrior who has only began learning the syntax and semantics of Idris/Agda would seriously struggle to understand deep concepts such as Curry-Howard isomorphism, let alone apply said concepts in the form of machine-checked proofs

The fact that @DonaldKellett openly says this only proves the point that such katas are ranked not based on their difficulty in terms of language/concept but because "plebs are too stupid to solve it" (which is a bit of an exaggeration, but is it?).

slightly less straightforward proofs requiring a bit more insight and intuition are easily ranked as 2 kyu or even 1 kyu

Apparently, now, when somebody created an actually, truly, genuinely hard theorem-proving katas which does deserve to be ranked very high, it can only be approved at the same level as those "not so difficult things" because the very same theorem-proving community (including @DonaldKellett) has been misjudging the katas, and now their rankings are way off from reasonable. As it has been suggested by @Voileexperiments above, why do we have to open 1 dan - 8 dan ranking range when we could get rid of all those katas "approved as 1 kyu just for lulz" katas by turning them yellow/blue? It's been a week or so, and all the katas available in Idris/Agda at ranked at least 4 kyu - how on earth is this possible if all the people who do theorem-proving katas are constantly talking how "this kata was very easy" or "that kata was very easy"?

---

But hey, this is just my opinion. I don't know Idris/Agda, I'm not into theorem-proving, so I could still be wrong in the end...

[DonaldKellett]

there's an Idris kata currently in Beta which ZED.CWT completed by closing holes and ranked 7 kyu, and Donald solved by reimplementing the whole thing from scratch and ranked 1 kyu

I don't know Idris/Agda

Are you sure you know what you are talking about? "Reimplementing the whole thing from scratch" would imply that I reconstructed basic lemmas as n + m = m + n or n + 0 = n from basic principles before using them in my proof which I have not done. I have made good use of the standard library - the only thing I didn't use was the interactive theorem-proving capabilities of Idris (which IMO obscures the very nature of the proof one is constructing, e.g. @lwoo1999 once said something to the effect to "sometimes I prove theorems in Idris/Agda without knowing what I am actually proving").

I do agree that certain Kata (such as Haskell's "A + B = B + A") are overranked but surely not everything is overranked? Also, as I mentioned, wouldn't a high barrier of entry automatically warrant a somewhat higher rank (if not that high)?

[lwoo1999]

I don't think that's a problem for katas that's as difficult as n-dan will stay beta for a very long time.

[lwoo1999]

By the way, except the univalence axiom, the kata "maybe injective" doesn't involve complicated mathematical concepts. I can explain the idea in mathematics easily. It's agda's fault that the kata is so difficult.

[ice1000]

It's agda's fault that the kata is so difficult.

[ice1000]

I remain neutral. I'm already used to rank those dan-like Katas as 1kyu, but I feel like it's good if we can have some extra difficulty.

[Voileexperiments]

@DonaldKellett

as I mentioned, wouldn't a high barrier of entry automatically warrant a somewhat higher rank (if not that high)?

Have you realized that programming has a very high barrier of entry?

[kazk]

While I agree that ranks used on Codewars have various issues, I don't think adding few dan level will fix anything. I wish we had more flexible and systematic ways to describe the difficulty. Trying to fit challenges from different areas and different languages into a single scale doesn't work.

I also don't think "could discourage Codewarriors from authoring and/or solving the more difficult ones" will be an issue. I don't think most of us are doing for honor points. We simply like to solve/create interesting problems.

Like @Voileexperiments wrote, I'd also recommend deflating the ranks as we get more kata. This will at least provide meaningful scale within the category.

"The sum of an arithmetic progression" is approved with 2 kyu. My Idris experience is about few hours (mostly reading code and docs enough to add Idris support). I have no idea what I'm doing, but I can still get to the point where I can imagine solving it if I learned how to use the functions in the standard library. I can be obviously wrong, but it didn't feel like I needed advanced knowledge of the language.

Is it really 2 kyu? If it really is, I don't think adding 1 dan and 2 dan will be enough.
Would you consider yourself advanced in Idris? If not, then 2 kyu might be too high.

the only thing I didn't use was the interactive theorem-proving capabilities of Idris

Do people regularly write Idris code without it? Add definition, split cases, solve trivial holes, make lemma, inspect the type. Repeating these got me to the point where I need to rearrange the types. I couldn't do it because I don't know anything yet, but it seemed doable if I take the time.
I thought this was the intended workflow. I imagine Agda is similar (gave up for now since setting up Emacs was too time consuming :().

Also, as I mentioned, wouldn't a high barrier of entry automatically warrant a somewhat higher rank (if not that high)?

I don't think so.

[Voileexperiments]

The issue here in its general sense is that whenever something new and relatively niche is introduced, since almost nobody knows what they're doing, almost nobody knows what the difficulty scale should be either. The sample size is too small. Nowadays a BF interpreter kata would be at most 6 kyu. They were considered 2 kyu at the past because whenever you mention "language parser", people panic (even if it's as simple as HQ9+).

There are 2 things to address here:

1. We don't know what the actual difficulty is, yet. But that's expected, so it's better to be robust
2. If you don't know what you're doing (like I don't even write Idris/Agda without an IDE and it's hopeless), you tend to be inclined to overrank the kata. It's a poisonous line of thought. This is what the power users meant when they were saying "everything is 8 dan" and "you should git gud instead of overranking everything".

In a sense, I treat kata difficulty akin to junior math olympaid problems: what kind of knowledge do you need to know at the very least to tackle the kata? If you can only recognize a problem by its textbook form, you really need to git gud. Most solutions to actual problems come from novel use and combinations of many easy concepts together.

[hobovsky]

As a person who is not a mathematician, and knows nothing about theorem proving or AGDA, I feel fully qualified to voice my opinion :)

I am with Voile here - first thing we (CW community) need is possibility to re-adjust difficulty ratings. There were tons of scenarios when task is something like "fizzle a frobble" which is ranked as 2 kyu while it's terribly overranked and should be 4 kyu tops. Then someone creates a kata of "fuggle a fizz" which requires first step of fizzling a frobble, and it should be ranked as 2 or 3 kyu but noone will estimate it as such, because easier, introductory task is already 2 kyu, and this one is definitely harder. Now, it ends up ranked relatively higher as 1 kyu and instead of adjusting misjudged, easy kata, we get yet another overranked one. (Side note: I have an idea how to handle rank adjustment over time, but I am not sure whether it's the right place to share it).

Another thing is that I do not understand how "sum of arithmetic progression" kata is so difficult, while that's one of few proofs I know how to do (on paper) and I could not even finish 8 kyu a+0=a kata. Granted, the statement of the problem shown to me by my highschool teacher might be dumbed down to class' level, but still - I cannot understand how you can do academic- or research- level stuff while at the same time I was told one cannot easily do really basic proofs: real numbers too hard, geometry not possible/difficult to represent, so, what's possible at all? Are we stuck with Z and Succ n forever? I know nothing about proof assistants, Idris, AGDA, or even Haskell, but it seems to me that these katas are in the same category as Brainfuck katas: they cannot be compared to any other and need its own hierarchy of difficulties. If it is so, then do not compare them to other 1 kyu katas, just decide that a+0=a is 8 kyu, Fermat is 1 kyu, and just try to fit a new kata somewhere in between :)

But I know nothing about the topic, so I might be wrong.

[DonaldKellett]

Since the official Codewars stance regarding the ranking criteria for theorem-proving Kata has been made clear, I guess there isn't much more I have to say. I will re-adjust my rank assessments to Kata in said area from this moment onwards.

Speaking of which, the existing Haskell Kata on this topic are heavily overranked since they aren't actually that difficult once you know what you are doing even without the interactive theorem-proving capabilities of Idris/Agda. I will open a separate Issue addressing this.

---

Side note: I have an idea how to handle rank adjustment over time, but I am not sure whether it's the right place to share it

@hobovsky If you have an idea, feel free to share it (maybe on a separate Issue though) 😄