4

I'm experimenting the refined type feature of scala provided in one of its library:

https://github.com/fthomas/refined

The following code represents a simple case:

  import eu.timepit.refined.auto._
  import shapeless.{Witness => W}

    type Vec5 = List[Int] Refined Size[Equal[W.`5`.T]]

    val v1: Vec5 = List(1, 2, 3, 4, 5)

    val v2: Vec5 = List(1 to 5: _*)

When attempting to compile it I got the following error:


[Error] /home/peng/git/scalaspike/common/src/test/scala/com/tribbloids/spike/refined_spike/Example.scala:32: compile-time refinement only works with literals
[Error] /home/peng/git/scalaspike/common/src/test/scala/com/tribbloids/spike/refined_spike/Example.scala:34: compile-time refinement only works with literals
[Error] /home/peng/git/scalaspike/common/src/test/scala/com/tribbloids/spike/singleton_ops_spike/Example.scala:32: Cannot prove requirement Require[...]
three errors found

It should be noted that both v1 & v2 can be easily evaluated at compile time and inlined, however scala compiler seems to refuse to do that, and for List type there seems to have no way to suggest this.

So how could this feature be useful?

Dmytro Mitin
  • 48,194
  • 3
  • 28
  • 66
tribbloid
  • 4,026
  • 14
  • 64
  • 103

2 Answers2

8

Judging by tests the Size[Equals[X]] compile-time lifting is only implemented in macros for String literals.

And BTW, this makes sense, because author would have to evaluate the code at compile time - List(1,2,3,4,5) might look easy, but Set(1,1,2,2,3,3) would require some evaluation, and what if the code to evaluate was List(1,1,2,2,3,3).distinct - it also could be resolved in compile time but you have to set line somewhere unless you want to risk arbitrary code execution. And even in simpler cases the ADT to analyze could be hairy and error prone. Sure, it would be possible to add some "obvious special cases" but personally, I prefer that the library's author focuses on something more useful instead.

Mateusz Kubuszok
  • 24,995
  • 4
  • 42
  • 64
  • 1
    This is why I'm asking if scala has a keyword to declare a literal for List type. In most modern compiler architecture there is no clear boundary between compile time and runtime. – tribbloid May 24 '20 at 20:05
  • Scala has literals only for: `String`s, symbols, `null` and some primitives, see: https://www.scala-lang.org/files/archive/spec/2.13/01-lexical-syntax.html#literals – Mateusz Kubuszok May 24 '20 at 20:20
  • I see, wow that seems like quite a distance to full dependent type. I'll see if I can find other bypasses – tribbloid May 24 '20 at 21:39
  • Well, Scala never claimed that it had full dependent types. It implemented a subset, path dependent types, and improved the idea in Dotty, but full dependent types are never a goal. Still it works out most of the time, check Miles Sabin post: https://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types – Mateusz Kubuszok May 24 '20 at 21:58
5

The thing is that eu.timepit.refined macros work for literals, BigDecimal, BigInt

https://github.com/fthomas/refined/blob/master/modules/core/shared/src/main/scala/eu/timepit/refined/macros/RefineMacro.scala#L14-L23

def impl[F[_, _], T: c.WeakTypeTag, P: c.WeakTypeTag](t: c.Expr[T])(
    rt: c.Expr[RefType[F]],
    v: c.Expr[Validate[T, P]]
): c.Expr[F[T, P]] = {
  val tValue: T = t.tree match {
    case Literal(Constant(value)) => value.asInstanceOf[T]
    case BigDecimalMatcher(value) => value.asInstanceOf[T]
    case BigIntMatcher(value)     => value.asInstanceOf[T]
    case _                        => abort(Resources.refineNonCompileTimeConstant)
  }

List(1, 2, 3, 4, 5) is not a literal.

For not literal values like List(1, 2, 3, 4, 5) there is refineV working at runtime

val v1 = List(1, 2, 3, 4, 5)
val v2 = List(1, 2, 3, 4, 5, 6)
refineV[Size[Equal[5]]](v1) 
// Right(List(1, 2, 3, 4, 5))
refineV[Size[Equal[5]]](v2) 
// Left(Predicate taking size(List(1, 2, 3, 4, 5, 6)) = 6 failed: Predicate failed: (6 == 5).)

Fortunately you can run refineV at compile time

object myAuto {
  implicit def compileTimeRefineV[T, P](t: T): T Refined P = 
    macro compileTimeRefineVImpl[T, P]

  def compileTimeRefineVImpl[T: c.WeakTypeTag, 
                             P: c.WeakTypeTag](c: blackbox.Context)(t: c.Tree): c.Tree = {
    import c.universe._
    val pTyp = weakTypeOf[P]
    val tTyp = weakTypeOf[T]
    c.eval(c.Expr[Either[String, T Refined P]](c.untypecheck(
      q"_root_.eu.timepit.refined.`package`.refineV[$pTyp].apply[$tTyp]($t)"
    ))).fold(
      c.abort(c.enclosingPosition, _),
      _ => q"$t.asInstanceOf[_root_.eu.timepit.refined.api.Refined[$tTyp, $pTyp]]"
    )
  }
}

import myAuto._ // don't import eu.timepit.refined.auto._
type Vec5 = List[Int] Refined Size[Equal[5]]
val v1: Vec5 = List(1, 2, 3, 4, 5) // compiles
// val v2: Vec5 = List(1, 2, 3, 4, 5, 6) 
  // Error: Predicate taking size(List(1, 2, 3, 4, 5, 6)) = 6 failed: Predicate failed: (6 == 5).

If you just need statically-sized collection you can use shapeless.Sized

https://github.com/milessabin/shapeless/wiki/Feature-overview:-shapeless-2.0.0#collections-with-statically-known-sizes

Dmytro Mitin
  • 48,194
  • 3
  • 28
  • 66
  • Thanks a lot, the answer apparently was written in scala 2.13, I'll try to reproduce it in 2.12. – tribbloid May 24 '20 at 19:53
  • The reason I prefer to avoid Shapeless.Sized is that it uses Nat type which relies on church encoding, which is not efficient – tribbloid May 24 '20 at 19:55
  • @tribbloid In 2.12. you just need to replace type `5` with ``W.`5`.T`` (`import eu.timepit.refined.W`). Everything else should work. – Dmytro Mitin May 26 '20 at 13:24
  • 1
    @tribbloid I [asked](https://gitter.im/fthomas/refined?at=5eca59944412600ccd64654f) **fthomas** aka [Frank S. Thomas](https://stackoverflow.com/users/460387/frank-s-thomas) at gitter: *"wouldn't it be a good idea to implement implicit conversions not only for literals?"*. His [answer](https://gitter.im/fthomas/refined?at=5ed63c999da05a060a47c69e): *"If we allow refining arbitrary values at compile-time, we would allow running arbitrary code at compile-time. If the expression passed to `refineV` has side-effects, we would run them at compile-time."* – Dmytro Mitin Jun 02 '20 at 12:02