问是否使用细化进行重试？
EN

Stack Overflow用户

提问于 2017-08-29 18:43:35

回答 1查看 96关注 0票数 1

使用细化，我尝试定义f

import eu.timepit.refined._
import eu.timepit.refined.api.Refined
import eu.timepit.refined.auto._
import eu.timepit.refined.numeric._

// if action 'succeeds', return 'good'; otherwise re-try, subtracting count by 1
scala> def f[A](action: => A, success: A => Boolean, count: Int Refined Positive): String = 
     |   if( success(action) ) "good" else f(action, success, count - 1)
<console>:32: error: compile-time refinement only works with literals
         if( success(action) ) "good" else f(action, success, count - 1)
                                                                    ^

由于这不起作用，我求助于：

def fEither[A](action: => A, success: A => Boolean, count: Either[String, Int Refined Positive]): String = { 
  println(count)

  if( success(action) ) "good" 
  else {
    count match {
      case Right(c) => fEither(action, success, refineV[Positive](c - 1))
      case Left(_)  => "bad"
    }
  }
}

scala> fEither[Int](42, _ => false, Right( refineMV[Positive]( 2 ) ) )
Right(2)
Right(1)
Left(Predicate failed: (0 > 0).)
res2: String = bad

理想情况下，我希望将此Idris程序转换为Scala：

f : (action : a) -> (success: a -> Bool) -> (n : Nat) -> String
f action success (S n) = if (success action) then "good" else f action success n
f _       _      Z     = "bad"

*scratch> f 42 (const False) 2
"bad" : String
*scratch> f 42 (const False) 0
"bad" : String

但我不确定在Nat功能上是否有任何模式匹配。

scala

refined

回答 1

Stack Overflow用户

发布于 2017-08-29 19:05:28

您要使用的细化是NonNegative，因此0是一个有效值。
Idris代码本质上区分n - 1是否仍然是一个自然数，因此您可以使用运行时版本的Idris直接进行区分

def f[A](action: => A, success: A => Boolean, count: Int Refined NonNegative): String =
  refineV[NonNegative](count - 1) match {
    case Right(n) => if (success(action)) "good" else f(action, success, n)
    case Left(_)  => "bad"
  }

备注:您可能需要多个参数列表b/c Scala可能无法在调用点正确推断A的类型

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/45937064

复制

相似问题

问是否使用细化进行重试？
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问是否使用细化进行重试？EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问是否使用细化进行重试？
EN