Use value-level terminology on type-level

[cvogt]

I think it would be great if we could use the same language at the type-level like at the value level. At least as close as possible. E.g.

Instead of

val x: Int Refined Greater[W.`5`.T]

val x: Int > W.`5`.T

This is syntactically possible, see e.g. https://github.com/cvogt/scala-extensions/blob/master/src/test/scala/constraint/boolean.scala

The question is what the best implementation for this would be in refined. I think concerns would be performance and impact on type error messages.

Alternative 1

type >[L,R] = L Refined Greater[R]

Does this impact error messages, do they dealias?

Alternative 2 Making Refined non-final and probably co-variant and

class >[L,R](val get: L) extends Refined[L,Greater[R]](get)

Does this prevent value classes?

Alternative 3 Not having a Refined super type, but individual types for each constraint.

class >[L,R](val get: L) extends AnyVal

Does this make things harder anywhere?

[dwijnand]

1. Type aliases are problematic, see #105
2. You can't extend value classes
3. Probably means duplication and possibly unification problems, but I'm not sure.

[lastland]

I'm definitely in favor of a simpler type level declaration, but wouldn't using the same symbols at both type level and value level kind of confusing? For example:

val x: Int > W.`5`.T = 6
val y: Int == W.`3`.T = 3

[soronpo]

Since singleton-ops uses same type aliases, and there are use-cases to use both libraries together, I'm not in favor of this suggestion. At least not as part of the default of refined import statement. Maybe something like import refined.standard_symbol_aliases._ will be OK.

[cvogt]

At the risk of overgeneralizing, I am under the impression some people like using different terminology for the same things in a different context and this might apply here. Here the contexts are value level expressions vs type level constraints.

Other examples where I have seen this are: Writing html templates? Let's name all the same things differently than in ordinary code. Writing type-level code? Let's use aliases instead of the operators we use in ordinary code. Writing server-side database queries? No need to call things the same as in client-side Scala code. Writing html style instruction? Let's use an entirely different language.

I am not saying this is wrong. I don't think people would advocate for it for no reason. My best hypothesis is that this helps some people with the context switch between the different things the code is for and sometimes allows specializing the language for the context.

Personally however, I find it harder to re-learn and remember names, syntax (or even concepts) for the same things depending on the context I am in. I'd prefer in refined to look at the syntactic context for knowing when I am in type-level position or value level position. So I am advocating for syntactical and terminological re-use for eased learning and eased remembering.

I actually see some curious similarity with discussions pro/con functional abstractions and pro/con type-inference. The more you generalize, e.g. by using .map for any Monad, not just List, the more you remove specific information from the code, which could have helped people understand what the code is about, but at the same time prevents re-use and grows the size of our language (counting number of library methods). Similarly with type-inference the sometimes helpful context of what type identifiers have is removed from the code at the favor of faster editing and easier overall comprehension.

So IMHO the question comes down to, do we want to generalize the syntax to be shared with value level Scala code for easier learnability and rememberability or do we instead prefer to keep it different to give more hints to the context when reading the code rather than having to scan forward or backwards for the next : or =.