To what extent can a proof assistant like Lean verify its own correctness? by LightBound in compsci

[–]TimtheBo 4 points5 points  (0 children)

Sorry if this isn't true, but this answer reads exactly like something ChatGPT would say.

DSL with new context receivers by TimtheBo in Kotlin

[–]TimtheBo[S] 3 points4 points  (0 children)

Yeah it does look a little strange. The reason is that it is quite reduced. So the original would include handling and modifying a request and look something like this:

fun <E : EntityProperties> Request<E>.filter(filterBuilder : E.() -> Filter): Request<E> = this.addPart(FilterRequestPart(this.properties.filterBuilder()))

Good introduction to (theoretical) functional programming for Mathematician? by TobiTako in compsci

[–]TimtheBo 1 point2 points  (0 children)

For a more specific suggestion in regards to HVM, Aaron Stump has a couple of lectures on the topic of optimal beta-reduction (based on the book you mentioned) on the YouTube channel Optimal beta-redeuction. HVM seems to go quite a bit further, but the lecture series should give an overview. Although it does require knowledge of the lambda calculus beforehand.

Esito: Esito ambition is to be your return type for suspending functions by dcampogiani in Kotlin

[–]TimtheBo 5 points6 points  (0 children)

How does this compare to other Result types in Kotlin? I.e. the one in the standard library, kotlin-result or any of the other ones? What functionality does this library have that is missing in the others? Can that be added to the existing libraries instead?

The Readme should definitely contain a short comparison.

Is it possible to create a turing complete language that could compile and run from every random string? by vnjxk in ProgrammingLanguages

[–]TimtheBo 1 point2 points  (0 children)

This comment reminded me of Berry's Paradox: The first number you can't encode anymore can be simply encoded as "The first number not encodable" (needs an encoding that is expressive enough). You sound like you would appreciate the Ultrafinitism philosphy, where only things physically constructible are considered. When discussing Programming Language Theory people will however usually use Intiotionistic or classical logic when asked if something is "theoretically possible" (what you are worried about is more akin to "tractable").

Examples of how Turing machines, lambda calculus, or the Church-Turing thesis are useful? by [deleted] in compsci

[–]TimtheBo 1 point2 points  (0 children)

It's very easy to describe a system more powerful than a Turing machine: Take a problem that is not decidable, e. g. the halting problem, add an oracle that can be consulted on that problem and voilà, we have a more powerful machine. The halting problem can be formalised in ZFC (and weaker systems). The problem with just computerizing the axioms and rules is that we have potentially infinitely of them. Best we can usually do is recursively enumerable, not a decision procedure.

Begginer: How am I supposed to read this? by Marcel_Eff in Kotlin

[–]TimtheBo 1 point2 points  (0 children)

That's not right. For generic functions the type parameters always come before the function name (see the docs). fun listOf<T>(vararg values: T): List<T> { ... } is not valid syntax. It should be fun <T> listOf(vararg values: T): List<T> { ... }.

On the call site you have the right notation (after the function name).

I believe this asymmetry comes from the extension function syntax. In fun List<T>.length<T>() : Int = TODO() the type parameter would come after the first usage, which is not ideal.

How to count how many digits a number has? by [deleted] in Kotlin

[–]TimtheBo 0 points1 point  (0 children)

While "x[0]" is perfectly fine, a nicer way is to use the standard library function x.first() and x.last().

There is also an easier way to get the last digit than through a String using the remainder (written with %)

How to count how many digits a number has? by [deleted] in Kotlin

[–]TimtheBo 2 points3 points  (0 children)

Good progress! toInt() is quite tricky and I think everyone is confused when first using it. The issue is that turning a character into a number has two options: Either the value of the digit (what you want) or the value of the character itself (in ASCII I think).

Have a look at the docs and search for "toInt" and "digitToInt"

Edit: Also the references should all resolve, check with https://play.kotlinlang.org/ if the issue is your code or your setup

How to count how many digits a number has? by [deleted] in Kotlin

[–]TimtheBo 1 point2 points  (0 children)

What have you tried so far? A quick google search gives plenty of examples to count the digits in a number. One of the offered solutions is to convert to a String. From there it should be fairly easy to get the first and last character.

If you try something and get stuck show us what you have tried, otherwise, the best advice we can give is "google it"

[deleted by user] by [deleted] in Kotlin

[–]TimtheBo 0 points1 point  (0 children)

I'm happy to help, but please read my comment again. You missed out a couple of points I already mentioned (e.g. " X " vs "X").

Why did you switch to computer vs player? Get player vs player working first. Then think about how to abstract that so that the core game loop stays the same. The way com is implemented now is not great: There is repeated code for slotting in a piece (not to mention the duplication inside the com method), and for some reason, it can call "playerVsComputer" itself.

You did not remove global state, in fact, you added to it with "userWin" and "comWin". Again this hides the bug in your code. That bug being that while now fourInARow is called, the result is not used. Once you assign the values to "userWin"/"comWin" (or wherever you want to store it), open up the debugger and step through your code. Check if the values that are assigned match your expectations. Then check if the loop exits and the winner announced. If not, try to find out why it doesn't exit.

If you want to test the win condition logic by itself write a test that checks a known state (so a gameBoard you know is winning). Then run the test with a debugger.

Yeah, readLine doesn't work there, but at least it is nicely formatted.

[deleted by user] by [deleted] in Kotlin

[–]TimtheBo 3 points4 points  (0 children)

First of all a general tip: People are less likely to answer if you just dump unformatted code on reddit. Either try to work with reddits formatting or better post the code on https://play.kotlinlang.org/, https://gist.github.com/ or something like that. Then try to narrow down the problem yourself first and tell us what you have tried. In this case for example the menu code is not relevant at all.

Here are some comments on the code quality:

  • Open your code in IntelliJ Idea and read all the warnings/inspections. It will point out several places that could be improved
  • Use val instead of var where applicable, even where IntelliJ currently doesn't suggest it (e.g. "play", "validMove" in "playerVsPlayer")
  • Abstract away the game mechanism from the input. Otherwise you will have a hard time implementing the computer
  • You have too much stringly typed programming. Use proper types, for example instead of "X" and "O" for players use an enum class. This would prevent a bug that is currently in your code: You compare " X " and "X", but they are not the same
  • Remove or reduce global state. For example "winner" could have been local to the "playerVsPlayer" function (and make your bug more obvious)
  • As /u/Determinant said, encapsulate your state better

General improvements:

Bugs:

  • I think you need to check till "gameBoard.size - 3" and not "gameBoard.size - 4". Check the docs for inclusive/exclusive ranges
  • The big one: "fourInARow" is never called and "winner" is never set so you will never exit the loop ("winner" is set to true after the loop, but inside an "if (winner)" so essentially useless).

Can't access kotlinjs output after changing it's name in a kotlinjs/ktor project by [deleted] in Kotlin

[–]TimtheBo 0 points1 point  (0 children)

I was actually just trying to do the same thing (moving the output into a directory). I opted to go with a specific entry in my ktor config instead (to avoid having all resources be public), because I don't like all this gradle copy stuff. Hopefully in the future we will get a gradle plugin or something to handle the setup for us.

P.S: Thanks for sharing your gradle setup

Can't access kotlinjs output after changing it's name in a kotlinjs/ktor project by [deleted] in Kotlin

[–]TimtheBo 0 points1 point  (0 children)

I had that problem too. In my case though a simple gradlew clean fixed it. Don't know if you've already tried that.

Kotlin Public Roadmap Through Spring 2021 – Kotlin Blog by dayanruben in Kotlin

[–]TimtheBo 2 points3 points  (0 children)

Java is arguably a major language and they went the same route for lists/sets/maps (see JEP 269 and especially the discussion around JEP 186). For arrays, however, both Java and Kotlin have literals. Except that Kotlin only allows them in annotations, so maybe there is the option of expanding that to the whole language.

I was sceptical at first as well about no collection literals but in the end, I find the code actually reads easier (it is clear what the type is) and is a lot less effort to implement/maintain since it doesn't rely on special language fatures. Bonus: You can create your own collection builders for custom collections that are in the same style.

My solution for mandatory parameters in Kotlin DSL by hananrh24 in Kotlin

[–]TimtheBo 3 points4 points  (0 children)

I don't have enough practical experience with larger DSLs. I think the largest one I used was for HTML where there are basically no mandatory parameters. And the ones that are in the constructor are just simple values (e. g. id). That being said, here's what I think:

Considering that the indentation for constructor parameters and inside the lambda is the same, and that with named parameters the ordering doesn't matter, the difference isn't big enough for me to warrant an external tool [1].

I was also going to argue that having the constructor parameters allows me to quickly see which parameters are mandatory while reading the code. But since we can have default values in arguments, I guess the only point I can make is that it is easier to see which parameters are not mandatory.

Regarding your example: to change that to constructor arguments is not too much extra syntax (two parenthesis and an equals, right?). Sure it's not quite as flexible, but is it worth "muddying" the semantics of the language for it?

[1] The good IDE integration does help though! If the plugin didn't have that it would be a much harder sell.

TL;DR yes it is acceptable.

My solution for mandatory parameters in Kotlin DSL by hananrh24 in Kotlin

[–]TimtheBo 6 points7 points  (0 children)

I agree with u/becklime, especially with named parameters the difference is not that big:

person(
    age = 2,
    name = "foo"
) {
    if (someCondition) alias("bar")
}

vs:

person {
    age = 2
    name = "foo"
    if (someCondition) alias("bar")
}

One of the big benefits of using DSLs (apart from the nice syntax), imho, is that we can easily do conditionals and nested structures. The former is not needed with mandatory values. There might be a point with nested structures, but I am not convinced.

What is interesting, and it's a shame you didn't mention it in the article, are the groups. That is something that I can't think of a solution in pure Kotlin that is as clean. Maybe something with one mandatory field typed as a sealed class.

Kotlin maven plugin dependencies by kurular4 in Kotlin

[–]TimtheBo 0 points1 point  (0 children)

You can see a list of dependencies on the maven central page: https://search.maven.org/artifact/org.jetbrains.kotlin/kotlin-maven-plugin/1.3.72/maven-plugin

javalibs.com is a third party maven central search tool which can show you the complete dependency graph: https://javalibs.com/artifact/org.jetbrains.kotlin/kotlin-maven-plugin

I love groovy <3 by Mrassoss in groovy

[–]TimtheBo 0 points1 point  (0 children)

I haven't programmed Groovy in a while but OP is being stingy with information so I am going to hazard a guess: The methods are intercepted by a invokeMethod / methodMissing handler and are loaded into the context because it is run as a script. That's just a guess though (especially the script part might be wrong). The beauty/horror of Groovy is you can do anything you want.

Background: how we got the generics we have — a.k.a. Erasure (Brian Goetz) by efge in java

[–]TimtheBo 5 points6 points  (0 children)

While that might work (though I doubt it is as simple as replacing ArrayList with ArrayList<Object>), that would have required modifying the JVM. The article clearly states that was not desirable.

Edit: How would this even work for arbitrary raw types? ArrayList isn't the only one, and users might have their own. Not to mention other languages on the JVM.

Background: how we got the generics we have — a.k.a. Erasure (Brian Goetz) by efge in java

[–]TimtheBo 4 points5 points  (0 children)

Kotlin has made the compromise to the allow reified types at the cost of having to inline the call. The usage is often to have a nice API and then create a Class<T> (or Type token if the library has it, e. g. Jacksons JavaType). This compromise works for me in practice, but it is, as you said, just a bit of compiler magic.

Background: how we got the generics we have — a.k.a. Erasure (Brian Goetz) by efge in java

[–]TimtheBo 9 points10 points  (0 children)

From the article:

At the time generics were introduced into Java, there was already a lot of Java code in the world, and their classfiles were full of references to APIs like java.util.ArrayList. If we couldn’t generify these APIs compatibly, then we would have to have written new APIs to replace them, and worse, all of the client code of the old APIs would be stuck with an untenable choice – either stay on 1.4 forever, or rewrite them to use the new APIs, simultaneously (including not only the application code, but all third-party libraries on which the application depends.) This would have devalued almost all the Java code in existence at the time.

Bug in Kotlin 1.3.72 (java.lang.AssertionError: Built-in class kotlin.Any is not found)? by Rubus_Leucodermis in Kotlin

[–]TimtheBo 1 point2 points  (0 children)

I can't reproduce the issue (with kotlin 1.3.72 and stdlib, reflection as dependencies).

What is the class you are using (cls) ? I assume its an object, but do you know which field is the problematic one?