Another question but this time about Arrow Analysi...

# arrow-meta

[bloder]

Another question but this time about Arrow Analysis, I'm trying to run in compile time a pre condition with collections, but I'm getting an error, I'm just trying to copy / paste the documentation example:

fun average(xs: List<Int>): Int {
  pre(xs.isNotEmpty()) { "list not empty" }
  TODO()
}

val x = average(listOf(1))

pre-condition `list not empty` is not satisfied in `average(listOf(1))`
  -> unsatisfiable constraint: `listOf(1).isNotEmpty`

The curious thing here is, pre / pos conditions with primitive values (like PositiveInt sample) works but not with collections, I've already tried to create value classes wrappers, Laws, but only works with primitive types, not collections... Am I missing anything? Current using Kotlin 1.6.10 and arrow analysis 2.0-SNAPSHOT

[raulraja]

are you adding the laws module to your plugin which includes the laws for the std lib and collections?

[raulraja]

but yeah, that should have worked

[raulraja]

I was trying to refer to some docs but looks like the latest deployment broke the arrow meta site

[bloder]

Only added the analysis class path and its plugin, Is there any place in arrow meta that this laws module is refered?

[raulraja]

https://github.com/arrow-kt/arrow-meta/blob/5e0c834a4f9e0d7a0956b8f996b77377de283410/plugins/analysis/example/build.gradle.kts#L16

[raulraja]

there is an example that manually applies the plugin

[bloder]

Yeah I saw this one, I've tried to copy / paste all collection laws to my project but still not working, investigating what I am doing wrong, once I have at least in my project all collection laws it should work, isn't? Or to check a isNotEmpty predicate I need to define laws from other std lib type?

[raulraja]

I’m not positive but will discuss with Alejandro in the next few days

[raulraja]

you wouldn’t need to paste the laws, just include them in the classpath depending on them

[raulraja]

they are also published

[bloder]

Got it! I'll try to test it in arrow meta sample internals

[bloder]

Hi @raulraja, srry bring this thread up again, I got some time to try to investigate isNotEmpty problem, I didn't find out why its axiom is not being declared properly but I found other axioms that is not being declared to smt solver by plugin internal laws like List<E>#isEmpty and mapOf() , then if u try to declare pre conditions like this:

fun <K, V> Map<K, V>.x(): Int {
  pre(isEmpty()) { "map is not empty" }
  return 1
}

val y = mapOf<Int, Int>().x()

and this:

fun <E> List<E>.x(): Int {
  pre(isEmpty()) { "list is not empty" }
  return 1
}

val y = listOf<Int>().x()

U'll get errors. U guys accepting contributions? I can open a PR

[raulraja]

Hi @bloder, yeah definitely open to contributions!,I haven’t had a chance to talk to Alejandro yet but hopefully we can discuss this next week.

[bloder]

perfect my friend! thanks!