Added subtypes for Inference

[umbreak]

Fixes #454

Here I've tried to have Inference as a trait and added 2 subtypes

• InferAlways
• InferWhen

With that we can directly have a safe conversion whenever an InferAlways is presen

[umbreak]

It is failing cause I added subtypes for Inference and it says Binary compatibility check failed (this mima plugin).

@fthomas I would appreciate some feedback on the approach I took, and whether you'd like to see some changes or It doesn't make sense at all the pull request.

[fthomas]

What is the purpose of T? I see that it is used in adapt but can't we just use Inference there? Subtypes should be able to override adapt with a more concrete type (eg. override def adapt[P2, C2](adaptedShow: String): InferAlways[P2, C2] = ...).

[umbreak]

I kept it there in case we wanted to use Dependent types for something like; def something[C,P](f: Inference[C,P]): f.T[C,P] = f...
However in the end I didn't find a way to use it for the implicit conversion. So if that's unnecessary any longer I can do it as suggested

[fthomas]

The Inference instances that depend on other Inference instances are now duplicated. One version for InferAlways and one version for InferWhen. I would prefer if we could achieve the same functionality without duplicating these instances. Maybe we could use the type member T on Inference for this:

implicit def modusTollens[A, B](implicit p1: Inference[A, B]): p1.T[Not[B], Not[A]] =
  p1.adapt("modusTollens(%s)")

?

[fthomas]

Forget that, my last suggestion does not work for

implicit def hypotheticalSyllogismAlways[A, B, C](implicit p1: A ==> B, p2: B ==> C): A ==> C =
  Inference.combine(p1, p2, "hypotheticalSyllogism(%s, %s)")

[umbreak]

Yes your suggestion is exactly what I was trying to achieve by adding the T abstract type however I also realized it doesn't work for all cases

[fthomas]

I've thought about this a bit more and I think I made a mistake in the design of Inference that we now have to pay the price for. The mistake is the isValid: Boolean field which allows invalid Inference instances. Predicates in the library are static and have no runtime component, so in principle we should be able to tell if A ==> B at compile time. This is also true for e.g. Greater[10] ==> Greater[5] because 10 and 5 are compile time constants but since I had no generic way to require that the first number is greater than the second, I introduced the isValid field that could be instantiated with 10 > 5 to know if the Inference is valid. If singleton-ops would have been available at the time Inference was added we probably could have defined the above instance as implicit def greaterInference[A, B](implicit ev: A > B): Greater[A] ==> Greater[B] = ??? which would guarantee that A is greater than B so that this instance is always valid and we wouldn't be able to construct invalid instances.

[fthomas]

The more I think about this issue, the more I become convinced that we should remove isValid from Inference. Pros for removing that field:

• ==> becomes similar to =:= and <:< from the standard library. If we have an instance A ==> B we can safely convert F[T, A] to F[T, B]. Similar, if we have X =:= Y we know the types are equal and we can convert X to Y.
• There is no need for an Inference macro anymore. autoInfer can become a simple function and all the gotchas regarding that macro would be gone.
• The purpose of ==> becomes clearer. If the compiler finds an instance A ==> B we know that the predicate A implies B. Now we only know that A might imply B but to be sure we need to look at a boolean field.

Arguments against removing that field:

• Instances for e.g. Greater[N] ==> Greater[M] would either require singleton-ops or be implemented via a macro. But these macros can be implemented without using the fragile eval which is currently used in the Inference macro.
• This would break source and binary compatibility.

[umbreak]

I agree. It became also clear to me when attempting to fix this issue that it would be better to have Inference as always valid and consequently macro would not be needed.

It seems feasible to do, having the disadvantage of breaking binary compatibility

[fthomas]

Ok, let's do this. I hope that instances for Greater[N] ==> Greater[M] won't be too hard to write.