LoginSignup
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 3 years have passed since last update.

@electronics_diy721(elec tron)

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

Last updated at Posted at 2021-11-07

直面した問題

  • リテラル値__List(1,2)を格納（名前束縛）した変数ints__で、値制約を付けたListオブジェクトをval宣言すると、エラーになる。
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宣言しても、エラーになる。
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

エラー

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つかどうかを型検査
val v1 = List(1, 2, 3, 4, 5)
refineV[Size[Equal[5]]](v1)
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を用意する
  • コンパイルが成功する（型検査合格）
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への名前束縛）
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の評価結果__が格納されているかを確認する
REPL(Terminal)
scala> temp.isRight
val res80: Boolean = true

scala> temp.isLeft
val res81: Boolean = false

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).__と表示される。
  • コンパイルが失敗する（型検査失格）
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).__と表示される。
  • コンパイルが失敗する（型検査失格）
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__を外すとコンパイルエラーになる。

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で用意されている述語一覧

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]である。
  • refineVHead[Equal[1]]だけ成立する。
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の要素すべてについて、指定した述語制約が充足されるかを検査する
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.__と出力される？？

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に投稿された質問

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

（ 省略 ）

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

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宣言すると、エラーになる。
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宣言しても、エラーになる。
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

エラー

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でも、以下は失敗した

  • 型に名前をつけるのは失敗
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>
  • クラス定義のコンストラクタの型シグネチャ煮付けるのも失敗
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で連結するのは失敗
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>
  • これは問題なく動く
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))
  • 要素数を数値リテラルではなく、加算計算式で与えると、認識されない。
sbtConsole
scala> refineV[Size[Equal[2+3]]](v1)
                           ^
       error: not found: type +

scala> refineV[Size[Equal[(2+3)]]](v1)
                            ^
       error: not found: type +
  • 無名関数を入れてもダメ
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>
  • 数値を束縛した変数を与えてもダメ
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でやってみたかったのだが・・・。

もうちょっとユースケースが分かりやすい例にベクタ型などもあります。 リスト型のようですが、 Vect n a と型引数にその長さ n を保持できます。

例えばそのベクタを結合する関数 ++ は以下のような型をしています。

(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem

長さ m のベクタと長さ n のベクタを結合すると長さ m + n のベクタになるというシンプルですが強力な表明が書けます。

あるいは要素 n 個を取り出す関数 take は以下のような型をしています。

take : (n : Nat) -> Vect (n + m) elem -> Vect n elem

n 個取り出すからには n 個以上のベクタを渡さないといけないんですね

実行環境

build.sbt
scalaVersion := "2.13.6"
libraryDependencies += "eu.timepit" %% "refined" % "0.9.27"
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>
1
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?