I recently got more into software correctness, and...

# getting-started

[ursus]

I recently got more into software correctness, and all this talk about invariants, and types being the best way to enforce

if so. what you think then about NonEmptyString, PositiveInt, NonEmptyList etc? i,e, specifically very general/non domain specific.

Overkill?

[Youssef Shoaib [MOD]]

They tend to work really nicely IMO. We have NonEmptyList in #C5UPMM0A0
There's many many articles I can cite here, but I really like Oleg Kiselyov's blog, specifically his article on basically this topic. Be warned, he writes in OCaml and Haskell, but all the ideas can be translated over into Kotlin with some effort.
The general pattern in Kotlin is having `value class`es that expose their innards `internal`ly only. This allows for functions that have unsafe implementations in the same module, but establish a safe contract for outside users. For instance, a NonEmptyList can be implemented as a List under the hood, but creating such a list is only done thru factory functions that guarantee the non-emptiness somehow.
From a correctness standpoint, all you have to do then is verify that the implementation within your module is correct (I.e. that the invariants you want indeed hold), then you guarantee it for everyone else

[ursus]

I see, what I have questions about is should those constraint types implement interfaces/operators etc, to not be annoying

say in the list case, should NonEmptyList implement List ?

Also, say NonZeroInt for a calculator Calculator.divide(a: Int, b: NonZeroInt)
does this make sense to you as well? It looks nice to me, but won't people be more annoyed with creating the NonZeroInt "instance"?

About the internal stuff, how would you have the NonZeroInt shaped? value class NonZeroInt(val value: Int) , is it worthwhile to not expose the value: Int? (and also should it implement arithmetic?)

[Youssef Shoaib [MOD]]

NonEmptyList should implement List yes, as should NonEmptyString implement CharSequence
I think NonZeroInt is unlikely to be helpful, but maybe you can make it work. You can always have some safe division that returns Int? (Rich errors can make this Int | DivisionByZero).
Re internal stuff: just make the constructors internal. That's the main trick really. Exposing the underlying value is usually fine, unless you wanna hide it because e.g. it's useless (for instance, Result from the stdlib has `Any?`as its underlying type because it holds a union of T and Failure. This union is not useful to users in its current form)

It should probably implement arithmetic yes. Kotlin gives you a lot of power in implementing the arithmetic operators however you want, so you can easily make it work in a type safe manner (e.g. operator fun NonZeroInt.plus(other: UInt): NonZeroInt is safe). A lot of the design work for these types goes into exactly what operators and other such functions to support and expose, since some of these operators may need to use the constructor directly. Usually, I'd also expose a toNonZeroIntOrNull() type of function so outside consumers can !! their way out, with the calls still being safe in the sense that your NonZeroInt is truly never zero

[ursus]

why do you want to make constructors internal? because you dont want to throw? (via say init { require(..) }

[ursus]

What about something domain specific, where the neat NonEmptyList doesnt fit, say chat has 1..5 participants

so, for example

value class ChatParticipants(
   val participants: List<User>
) {
   init {
      require(<http://participants.si|participants.si>ze in 1..5)
   }
}

now, at first glance whats annoying is the doubling of the name (participants.participants.forEach) at callsites looks kinda dumb

and also I dont think implementing List here is worth it

wdy think? or is this a bad type?

[Marat Akhin]

Some design space exploration for these could be also found here: https://github.com/Kotlin/KEEP/blob/main/notes/0006-refinement-types.md

[efemoney]

participants.value / participants.list / participants.users ...

[Youssef Shoaib [MOD]]

You can have a throwing constructor like that, but I tend to avoid it. For one, you'd be duplicating the validation effort between the constructor and any "smart constructor". For another, exceptions just aren't the nicest thing to use in Kotlin. Sometimes your data representation might be very weird and might involve generics in a magical way (prime example is Result), meaning that no `require`s can really save you, and the caller might be confused.

For participants, I wouldn't mind making it extend List. Do remember that you can just write your own forEach as well.

[min]

@ursus Logic doesn't belong in constructors.

class ChatParticipants private constructor(
    val participants: List<User>,
) {
    companion object {
        fun new(participants: List<User>): ChatParticipants? {
            return when (participants.size) {
                in 1..5 -> ChatParticipants(participants)
                else -> null
            }
        }
    }
}

Always control the instantiation of your types. Although if somebody else has access to the participants: List<User> as a MutableList<User>, the invariant can still be broken.

val users = mutableListOf<User>()
populate(users)

val participants = ChatParticipants.new(users) ?: return
users.add(newUser()) // ⚠️

You may choose to clone the list in new if you’re fine with the performance cost.

[Youssef Shoaib [MOD]]

You can use ImmutableList from kotlinx.collections.immutable if you really wanna ensure that

Also, I'd go with companion object { operator fun invoke(...) } or a top-level function with the same name as the class to simulate a constructor better (a pattern called "smart constructor")

[min]

@Youssef Shoaib [MOD] I’ll have to check out ImmutableList! That sounds awesome. Personally I wouldn’t employ the invoke syntax sugar though. I like to be explicit about the factory not being a constructor language item, but to each their own.

[ursus]

@Marat Akhin the point of refinement types vs a value class with require in construtor is what exactly? that the enforcement could be at comp time?

[Youssef Shoaib [MOD]]

@ursus The design notes define 2 potential avenues: refinement classes and refinement subtypes. Enforcement at comp time applies to both I believ, and it's basically the extent of what refinement classes would provide.
Refinement subtypes are more interesting IMO since they're "subtypes" of their original type, so they expose all the operations and such.

[ursus]

that would be super nice to have

that could also implicitly emulate dependant types, no? Array<Int, 3>

[ursus]

btw did you all know swift is adding dependant types? atleast what I call dependant types = value type parameters