Scalaの依存型refinedをList型の変数に適用すると「リテラル値でない」エラーになる => refineVで解決！

###直面した問題

- リテラル値__*List(1,2)*__を格納（名前束縛）した変数__*ints*__で、値制約を付けたListオブジェクトをval宣言すると、エラーになる。

```Scala:REPL(Terminal)
scala> type TwoInts = List[Int] Refined Size[W.`2`.T]
type TwoInts

scala> val ints = List(1,2)
val ints: List[Int] = List(1, 2)


scala> val ints2: TwoInts = ints
                            ^
       error: type mismatch;
        found   : List[Int]
        required: TwoInts
           (which expands to)  eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[Int(2)]]

scala>
```

- リテラル値__*List(1,2)*__で、値制約を付けたListオブジェクトをval宣言しても、エラーになる。


```Scala:REPL(Terminal)
scala> val ints2: TwoInts = List(1,2)
                                ^
       error: type mismatch;
        found   : List[Int]
        required: TwoInts
           (which expands to)  eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[Int(2)]]

```

> Frank Thomas @fthomas 8月 31 2017 07:29 UTC
>@coltfred Size needs to take another predicate like Equal or Greater as argument. So if you >define TwoInts as List[Int] Refined Size[Equal[W.`2`.T]] it should work as expected. Here are >some examples from the tests

###エラー

```Scala:REPL(Terminal)
scala> type TwoInts = List[Int] Refined Size[Equal[W.`2`.T]]
type TwoInts

scala> val ints3: TwoInts = List(1,2)
                                ^
       error: compile-time refinement only works with literals

scala> ints
val res6: List[Int] = List(1, 2)

scala> val ints3: TwoInts = ints
                            ^
       error: compile-time refinement only works with literals

scala> val ints3: TwoInts = `List(1,2)`
                            ^
       error: not found: value List(1,2)

scala> val ints3: TwoInts = List(1, 2)
                                ^
       error: compile-time refinement only works with literals

```

###以下で成功する

- コンテナ型（List型やArray型、Set型）が要素数を5つかどうかを型検査

>```Scala:
>val v1 = List(1, 2, 3, 4, 5)
>refineV[Size[Equal[5]]](v1) 
>```


```Scala:REPL(Terminal)
scala> val v1 = List(1, 2, 3, 4, 5)
val v1: List[Int] = List(1, 2, 3, 4, 5)

scala> v1
val res7: List[Int] = List(1, 2, 3, 4, 5)
```

- 要素数５のList[Int]型インスタンス v1を用意する
- コンパイルが成功する（型検査合格）

```Scala:REPL(Terminal)
scala> refineV[Size[Equal[5]]](v1) 
val res8: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]]] = Right(List(1, 2, 3, 4, 5))

scala> 
```

- 変数に格納することもできる（変数*temp*への名前束縛）

```Scala:REPL(Terminal)
scala> val v1 = List(1, 2, 3, 4, 5)
val v1: List[Int] = List(1, 2, 3, 4, 5)

scala> refineV[Size[Equal[5]]](v1)
val res68: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]]] = Right(List(1, 2, 3, 4, 5))

scala> val temp = refineV[Size[Equal[5]]](v1)
val temp: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]]] = Right(List(1, 2, 3, 4, 5))

scala> temp
val res69: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]]] = Right(List(1, 2, 3, 4, 5))

scala>  
```

- tempの中身はEither型。
- Rightに、式__*List*の評価結果__が格納されているかを確認する

```Scala:REPL(Terminal)
scala> temp.isRight
val res80: Boolean = true

scala> temp.isLeft
val res81: Boolean = false

scala>
```

- 格納されていた。中身を取り出す。

```Scala:REPL(Terminal)
cala> temp.right
warning: 1 deprecation (since 2.13.0); for details, enable `:setting -deprecation` or `:replay -deprecation`
val res73: scala.util.Either.RightProjection[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]]] = RightProjection(Right(List(1, 2, 3, 4, 5)))

scala> temp.right.get
warning: 2 deprecations (since 2.13.0); for details, enable `:setting -deprecation` or `:replay -deprecation`
val res74: eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]] = List(1, 2, 3, 4, 5)

scala> val result = temp.right.get
warning: 2 deprecations (since 2.13.0); for details, enable `:setting -deprecation` or `:replay -deprecation`
val result: eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]] = List(1, 2, 3, 4, 5)

scala> result
val res75: eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]] = List(1, 2, 3, 4, 5)

scala> println(result)
List(1, 2, 3, 4, 5)

scala> println(temp)
Right(List(1, 2, 3, 4, 5))

scala>
```

- 型検査の述語制約を、「要素数が3であること」に変更する
- __*failed: Predicate failed: (5 == 3).*__と表示される。
- コンパイルが失敗する（型検査失格）

```Scala:REPL(Terminal)
scala> refineV[Size[Equal[3]]](v1) 
val res15: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[3]]]] = Left(Predicate taking size(List(1, 2, 3, 4, 5)) = 5 failed: Predicate failed: (5 == 3).)

scala> 
```

- 型検査の述語制約を、「要素数が2であること」に変更する
- __*failed: Predicate failed: (5 == 2).*__と表示される。
- コンパイルが失敗する（型検査失格）

```Scala:REPL(Terminal)
scala> refineV[Size[Equal[2]]](v1)
val res16: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[2]]]] = Left(Predicate taking size(List(1, 2, 3, 4, 5)) = 5 failed: Predicate failed: (5 == 2).)

scala> 
```

__*Size[Equal[5]]](v1)*__の述語__*Equals*__を外すとコンパイルエラーになる。

```Scala:REPL(Terminal)
scala> refineV[Size[5]](v1)
                       ^
       error: could not find implicit value for parameter v: eu.timepit.refined.api.Validate[List[Int],eu.timepit.refined.collection.Size[5]]

scala> 
```

###RefineVではなく、Refinedで用意されている述語一覧

https://github.com/fthomas/refined#documentation

>```text:
>collection
>
>Contains[U]: checks if an Iterable contains a value equal to U
>Count[PA, PC]: counts the number of elements in an Iterable which satisfy the predicate PA and >passes the result to the predicate PC
>Empty: checks if an Iterable is empty
>NonEmpty: checks if an Iterable is not empty
>Forall[P]: checks if the predicate P holds for all elements of an Iterable
>Exists[P]: checks if the predicate P holds for some elements of an Iterable
>Head[P]: checks if the predicate P holds for the first element of an Iterable
>Index[N, P]: checks if the predicate P holds for the element at index N of a sequence
>Init[P]: checks if the predicate P holds for all but the last element of an Iterable
>Last[P]: checks if the predicate P holds for the last element of an Iterable
>Tail[P]: checks if the predicate P holds for all but the first element of an Iterable
>Size[P]: checks if the size of an Iterable satisfies the predicate P
>MinSize[N]: checks if the size of an Iterable is greater than or equal to N
>MaxSize[N]: checks if the size of an Iterable is less than or equal to N
>```


###RefineVで、コンテナ型オブジェクトに対するHeadを試してみる

- v1オブジェクトは、Int型「１」で始まるList[Int]である。
- refineV[Head[Equal[1]]](v1)だけ成立する。

```Scala:REPL(Terminal)
scala> v1
val res17: List[Int] = List(1, 2, 3, 4, 5)

scala> refineV[Head[Equal[3]]](v1)
val res14: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Head[eu.timepit.refined.generic.Equal[3]]]] = Left(Predicate taking head(List(1, 2, 3, 4, 5)) = 1 failed: Predicate failed: (1 == 3).)

scala> refineV[Head[Equal[2]]](v1)
val res21: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Head[eu.timepit.refined.generic.Equal[2]]]] = Left(Predicate taking head(List(1, 2, 3, 4, 5)) = 1 failed: Predicate failed: (1 == 2).)

scala> refineV[Head[Equal[1]]](v1)
val res22: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Head[eu.timepit.refined.generic.Equal[1]]]] = Right(List(1, 2, 3, 4, 5))

scala> 
```
- Forallで、Listの要素すべてについて、指定した述語制約が充足されるかを検査する

```Scala:REPL(Terminal)
scala> refineV[Forall[Equal[-10]]](v1)
val res28: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Forall[eu.timepit.refined.generic.Equal[-10]]]] = Left(Predicate failed: ((1 == -10) && (2 == -10) && (3 == -10) && (4 == -10) && (5 == -10)).)

scala> refineV[Forall[Positive]](v1)
val res29: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Forall[eu.timepit.refined.numeric.Positive]]] = Right(List(1, 2, 3, 4, 5))

scala> refineV[Forall[Negative]](v1)
val res30: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Forall[eu.timepit.refined.numeric.Negative]]] = Left(Predicate failed: ((1 < 0) && (2 < 0) && (3 < 0) && (4 < 0) && (5 < 0)).)

scala> 
```

以下は、充足しない場合に、__*did not fail.*__と出力される？？

```Scala:REPL(Terminal)
scala> refineV[Exists[Equal[100]]](v1)
val res24: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Exists[eu.timepit.refined.generic.Equal[100]]]] = Left(Predicate (!(1 == 100) && !(2 == 100) && !(3 == 100) && !(4 == 100) && !(5 == 100)) did not fail.)

scala> refineV[Exists[Equal[1]]](v1)
val res25: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Exists[eu.timepit.refined.generic.Equal[1]]]] = Right(List(1, 2, 3, 4, 5))

scala> refineV[Exists[Equal[-10]]](v1)
val res26: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Exists[eu.timepit.refined.generic.Equal[-10]]]] = Left(Predicate (!(1 == -10) && !(2 == -10) && !(3 == -10) && !(4 == -10) && !(5 == -10)) did not fail.)

scala> refineV[Exists[-10]](v1)
                           ^
       error: could not find implicit value for parameter v: eu.timepit.refined.api.Validate[List[Int],eu.timepit.refined.collection.Exists[-10]]

```

##参考にしたサイト
###stack overflowに投稿された質問

https://stackoverflow.com/questions/61979101/scala-how-to-force-converting-a-statement-to-literal

>The following code represents a simple case:
>
>```Scala:
>  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:
>
>```Scala:
>[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
>
> （ 省略 ）

###stack overflowに投稿された回答

> 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
>
>```Scala:
>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).)
>```

##Refinedを使うとコンパイルエラーになる
###エラー

- リテラル値__* List(1,2)*__を格納（名前束縛）した変数__*ints*__で、値制約を付けたListオブジェクトをval宣言すると、エラーになる。

```Scala:REPL(Terminal)
scala> type TwoInts = List[Int] Refined Size[W.`2`.T]
type TwoInts

scala> val ints = List(1,2)
val ints: List[Int] = List(1, 2)


scala> val ints2: TwoInts = ints
                            ^
       error: type mismatch;
        found   : List[Int]
        required: TwoInts
           (which expands to)  eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[Int(2)]]

scala>
```

- リテラル値__* List(1,2)*__で、値制約を付けたListオブジェクトをval宣言しても、エラーになる。


```Scala:REPL(Terminal)
scala> val ints2: TwoInts = List(1,2)
                                ^
       error: type mismatch;
        found   : List[Int]
        required: TwoInts
           (which expands to)  eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[Int(2)]]

```

> Frank Thomas @fthomas 8月 31 2017 07:29 UTC
>@coltfred Size needs to take another predicate like Equal or Greater as argument. So if you >define TwoInts as List[Int] Refined Size[Equal[W.`2`.T]] it should work as expected. Here are >some examples from the tests

###エラー

```Scala:REPL(Terminal)
scala> type TwoInts = List[Int] Refined Size[Equal[W.`2`.T]]
type TwoInts

scala> val ints3: TwoInts = List(1,2)
                                ^
       error: compile-time refinement only works with literals

scala> ints
val res6: List[Int] = List(1, 2)

scala> val ints3: TwoInts = ints
                            ^
       error: compile-time refinement only works with literals

scala> val ints3: TwoInts = `List(1,2)`
                            ^
       error: not found: value List(1,2)

scala> val ints3: TwoInts = List(1, 2)
                                ^
       error: compile-time refinement only works with literals

```

###RefineVでも、以下は失敗した


- 型に名前をつけるのは失敗

```Scala:REPL(Terminal)
scala> type Vec5 = List[Int] refineV[Size[Equal[5]]]
                                    ^
       error: identifier expected but '[' found.

scala> type Vec5 = refineV[Size[Equal[5]]]
                   ^
       error: not found: type refineV

scala> 
```

- クラス定義のコンストラクタの型シグネチャ煮付けるのも失敗

```Scala:REPL(Terminal)
scala> class ElementTwoList(data: List[Int] refineV[Size[Equal[5]]]) {
     |  val data_ = data
     |  def getData = data_
     |  println(data_)
     | }
                                                   ^
       error: identifier expected but '[' found.

scala>
``` 


- 他の型制約条件とANDで連結するのは失敗

```Scala:REPL(Terminal) 
scala> val a: List[Int] refineV[Head[Equal[2]]] And refineV[Size[Equal[5]]] = List(70000, 20, 100)
                               ^
       error: identifier expected but '[' found.
  
scala> val a: List[Int] refineV(Head[Equal[2]]) And refineV(Size[Equal[5]]) = List(70000, 20, 100)
                                                           ^
       error: ';' expected but '(' found.

scala> val a: refineV(Head[Equal[2]]) And refineV(Size[Equal[5]]) = List(70000, 20, 100)
                     ^
       error: ';' expected but '(' found.

scala> val a: Head[Equal[2]] And Size[Equal[5]] = List(2, 20, 100, 3, 435)
                                                      ^
       error: type mismatch;
        found   : List[Int]
        required: eu.timepit.refined.boolean.And[eu.timepit.refined.collection.Head[eu.timepit.refined.generic.Equal[2]],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]]

scala> val a: Head[Equal["a"]] And Size[Equal[5]] = List("a", "b", "c", "d", "e")
                                                        ^
       error: type mismatch;
        found   : List[String]
        required: eu.timepit.refined.boolean.And[eu.timepit.refined.collection.Head[eu.timepit.refined.generic.Equal["a"]],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]]

scala> 
```


- これは問題なく動く

```Scala:sbtConsole
scala> val v1 = List(1, 2, 3, 4, 5)
val v1: List[Int] = List(1, 2, 3, 4, 5)

scala> refineV[Size[Equal[5]]](v1)
val res0: Either[String,eu.timepit.refined.api.Refined[List[Int],eu.timepit.refined.collection.Size[eu.timepit.refined.generic.Equal[5]]]] = Right(List(1, 2, 3, 4, 5))
```

- 要素数を数値リテラルではなく、加算計算式で与えると、認識されない。

```Scala:sbtConsole
scala> refineV[Size[Equal[2+3]]](v1)
                           ^
       error: not found: type +

scala> refineV[Size[Equal[(2+3)]]](v1)
                            ^
       error: not found: type +

```

- 無名関数を入れてもダメ

```Scala:sbtConsole
scala> refineV[Size[Equal[(_ -> 2 + 3)]]](v1)
                                  ^
       error: not found: type +

scala> refineV[Size[Equal[((_ -> 2 + 3): Int => Int)]]](v1)
                                       ^
       error: ')' expected but ':' found.

scala> refineV[Size[Equal[((_) -> 2 + 3): Int => Int)]]](v1)
                                        ^
       error: ']' expected but ':' found.

scala> refineV[Size[Equal[(((_) -> 2 + 3): Int => Int)]]](v1)
                                         ^
       error: ')' expected but ':' found.

scala> refineV[Size[Equal[((_) -> 2 + 3)]]](v1)
                                    ^
       error: not found: type +

scala> refineV[Size[Equal[((_) -> 5)]]](v1)
                               ^
       error: not found: type ->

scala> 

```

- 数値を束縛した変数を与えてもダメ

```Scala:sbtConsole
scala> val length = 5
val length: Int = 5

scala> refineV[Size[Equal[length]]](v1)
                          ^
       error: not found: type length

scala> refineV[Size[Equal[W.`length`.T]]](v1)
                          ^
       error: Malformed literal length

scala> val x = 5
val x: Int = 5

scala> refineV[Size[Equal[W.`x`.T]]](v1)
                          ^
       error: Malformed literal x

scala> refineV[Size[Equal[x]]](v1)
                          ^
       error: not found: type x
       
```

__*Idris*__の依存型では、関数の型シグネチャで、返り値のデータ型（コンテナ型）の要素数が、２つの引数（コンテナ型）の要素数の和になるという制約を付加できる。

こうしたことをScalaでやってみたかったのだが・・・。

https://keens.github.io/blog/2020/11/30/idristtedonnagengo_/

> もうちょっとユースケースが分かりやすい例にベクタ型などもあります。 リスト型のようですが、 Vect n a と型引数にその長さ n を保持できます。
>
>例えばそのベクタを結合する関数 ++ は以下のような型をしています。
>
>```Idris:
>(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
>```
>
>長さ m のベクタと長さ n のベクタを結合すると長さ m + n のベクタになるというシンプルですが強力な表明が書けます。
>
>あるいは要素 n 個を取り出す関数 take は以下のような型をしています。
>
>```Idris:
>take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
>```
>
>n 個取り出すからには n 個以上のベクタを渡さないといけないんですね


##実行環境

```text:build.sbt
scalaVersion := "2.13.6"
libraryDependencies += "eu.timepit" %% "refined" % "0.9.27"
```


```Scala:sbtConsole
scala> import eu.timepit.refined._
import eu.timepit.refined._

scala> import eu.timepit.refined.api.Refined
import eu.timepit.refined.api.Refined

scala> import eu.timepit.refined.auto._
import eu.timepit.refined.auto._

scala> import eu.timepit.refined.collection._
import eu.timepit.refined.collection._

scala> import eu.timepit.refined.numeric._
import eu.timepit.refined.numeric._

scala> import eu.timepit.refined.string._
import eu.timepit.refined.string._

scala> import shapeless.{Witness => W}
import shapeless.{Witness=>W}

scala> import eu.timepit.refined.api.{Refined, Validate} 
import eu.timepit.refined.api.{Refined, Validate}

scala> import eu.timepit.refined.numeric.Interval
import eu.timepit.refined.numeric.Interval

scala> import eu.timepit.refined.api.{RefType, Refined}
import eu.timepit.refined.api.{RefType, Refined}

scala> import eu.timepit.refined.boolean._
import eu.timepit.refined.boolean._

scala> import eu.timepit.refined.char._
import eu.timepit.refined.char._

scala> import eu.timepit.refined.collection._
import eu.timepit.refined.collection._

scala> import eu.timepit.refined.generic._
import eu.timepit.refined.generic._

scala> import eu.timepit.refined.string._
import eu.timepit.refined.string._

scala> import shapeless.{ ::, HNil}
import shapeless.{$colon$colon, HNil}

scala> 
```