• ###### lationstcommented on "Sum of squares less than some number" haskell solution

I like that you used a list comprehension. I forget about those sometimes

• ###### ShreckYeresolved a suggestion on "Cardinality of N and N x N" kata

Thanks. I do think "Modular operations" is overranked. It takes sometime to get familiar with `Fin` and then work with its tricky definition, but the overall solution is usually not long: mine is about 40 lines and it's a lot simpler if you know the `mod` function as in andersk's solution. So I'd say it should be 2 kyu, for someone who knows `mod` maybe it should even be 3 kyu. The rank for "String formatting" is about right, it takes time to get used to defining functions that work on types and come with up that idea for the Kata as a learner.

• ###### monadiuscommented on "Cardinality of N and N x N" kata

Inconsistent ranking is a well known Codewars issue. The "Modular operations" kata is overranked. There is an ongoing work to adjust ranks of Agda kata.

In my opinion, this kata is between 1 and 2 kyu. I approved it as 2 kyu because it has a Coq translation. And it is simpler to write proofs in Coq.

Assuming that this kata is 1.5 kyu in Agda, I would like to know your rank suggestions for the "Modular operations" kata and the "String formatting" kata. Since you are learning Agda, your rank suggestions will be very valuable.

• ###### ShreckYecreated a suggestion for "Cardinality of N and N x N" kata

I am currently learning Agda. I completed the 1 kyu Kata "Modular operations on Finite data type" and then started to try this Kata becasue I haven't learned Cubical Agda but I learned about this in our math lessons so I thought this would be easier to start with. However, it took me a lot more time than expected.

I defined the Cantor pairing function and its inverse in the primitive with only addition, substraction, and recursion. Then proving the bijection using well-founded induction is a lot trouble and took a lot of time. I thought maybe I myself made the problem more complicated than it should be in this way, but I took a rough look at some other solutions and they all turned out to be just as lengthy.

So just a suggestion: maybe this Kata should be ranked 1 kyu instead of 2 kyu to be less misleading, considering that I spent much more time to complete this than a 1 kyu Kata, that all the solutions I see seem to quite lengthy, and that the total times this has been completed is actually less than 3 of the 4 currently existing 1 kyu Agda Katas. Or possibly in the other way, maybe "Modular operations on Finite data type" should be ranked down since I see some really short solutions there.

And a tip for those who think this should be easy like I did: it is not, especially if it's your first time to use well-founded induction! 😭

• ###### monadiusresolved an issue on "A bit of fun with proofs on inequalities" kata

The rank is adjusted

Fixed

• ###### XRFXLPcreated an issue for "One Line Task [Haskell]: Weak Primality Test" kata

GHC 8.8.4 (which is the default version)
Sample test returns:

``````IOException of type NoSuchThing
/home/codewarrior/solution.txt: openFile: does not exist (No such file or directory)
``````

But same runs in 8.2.2(sample and full) and 8.8.4(only full) fine.

• ###### ldcccommented on "L1: Set Alarm" haskell solution

that shocking me

• ###### Opabiniacommented on "One Line Task [Haskell]: 100 times..." kata

I absolutely hated doing that, but I'm really glad I did :)

• ###### Opabiniacommented on "One Line Task [Haskell]: 100 times..." kata

I thought that give up meant I was supposed to use fold!

Haha, now that really sent me barking down the wrong alley...

• ###### JohanWiltinkcommented on "Maximum Product " haskell solution

`<*>` is a better fit than `>>=` for `zipWith .. tail`. When fed an empty list, `zipWith (*) [] (tail [])` returns `[]` without evaluating `tail []`. `zipWith (*) (tail []) []` crashes. That's why you want the second list to be shorter, thus `<*>`.

In this case, `maximum []` will crash anyway, so it doesn't matter, you need a list of at least two elements to succeed at all.

.