I am looking into arrow analysis and it talks a bi...

# arrow

[Ties]

I am looking into arrow analysis and it talks a bit about require being invariant, and pre/post conditions being something different.

fun increment(x: Int): Int {
    pre(x > 0) { "value must be positive" }
    return x + 1
}

fun increment2(x: Int): Int {
    require(x > 0) { "value must be positive" }
    return x + 1
}

But here both seem to work the same, and if I look into the code I see pre() is just calling require.
If I then look at the examples in the documentation (https://arrow-kt.io/docs/meta/analysis/types/)class

Positive(val value: Int) {
  init { require(value > 0) }
}

and 

class Positive(val value: Int) {
  init { 
    pre(value > 0) { "value must be positive" }
    post({ this.value > 0 }) { "value is positive" }
  }
}

could the second example also be written

class Positive(val value: Int) {
  init { 
    require(value > 0) { "value must be positive" }
    post({ this.value > 0 }) { "value is positive" }
  }
}

and it being the same thing? or is there a difference between pre and require?

[raulraja]

hi @Ties no difference, require is an existing function from the std lib we support to declare pre conditions. Pre conditions are a type of invariant.

[Ties]

thanks for your quick reply! Is there any special reason for pre to exist then? (apart from it being more readable in combination with post ) (no judgement btw, trying to understand)

[raulraja]

invariant from the point of view they provide a fact about the state of a value at a given point. As far as I understand it pre, post , invariant and require they all declare invariants about values at some point. pre and require are used as pre conditions of arguments, post for resulting values of calls and invariant in loops. @Alejandro Serrano Mena may be able to provide more context if there are any more detailed differences. In terms of pre and require they are the same. pre was added historically before require and maybe it can be considered for removal going forward.

[Ties]

Thank you 🙂 that explains it quite well (invariance was also a new term for me before reading the documentation, but I think I get it now)