使用类型对任意约束进行建模以进行编译时检查

发布于 2024-10-30 12:47:15 字数 2907 浏览 3 评论 0原文

鉴于 Scala 的强大类型系统,我有一个雄心勃勃的项目,现在我即将放弃它,因为工作量与有用性的比率似乎太高了。

基本上我有一些图形元素(GE),它们对应于以给定计算速率执行的声音过程。图形元素由形成其输入的其他图形元素组成。现在,输入速率存在相当任意的约束。在源语言(SuperCollider)中,速率在运行时检查,这自然是因为它是动态类型语言。我想看看是否可以在编译时强制执行检查。

一些约束相当简单,可以用“arg1 的速率必须至少与 arg2 的速率一样高”的形式来表达。但其他的则变得复杂,例如

“如果 arg0 的速率是‘需求’,则 args1 的速率必须是‘需求’或‘标量’或等于封闭的 GE 速率”。

问题是:我应该放弃这个吗?以下是运行时检查的外观:

sealed trait Rate
case object demand  extends Rate
case object audio   extends Rate
case object control extends Rate
case object scalar  extends Rate

trait GE { def rate: Rate }

// an example GE:
case class Duty(rate: Rate, in0: GE, in1: GE) extends GE {
  def checkRates(): Unit =
    require(in0.rate != demand || (in1.rate != demand &&
            in1.rate != scalar && in1.rate != rate))
}

相比之下,使用速率类型参数时的外观:

sealed trait Rate
trait audio   extends Rate
trait demand  extends Rate
trait control extends Rate
trait scalar  extends Rate

trait GE[R <: Rate]

object Duty {
  trait LowPri {
    implicit def con1[R, T]: RateCons[R, audio  , T] = new ConImpl[R, audio  , T]
    implicit def con2[R, T]: RateCons[R, control, T] = new ConImpl[R, control, T]
    implicit def con3[R, T]: RateCons[R, scalar , T] = new ConImpl[R, scalar , T]

    implicit def con4[R, T]: RateCons[R, demand , demand] = 
      new ConImpl[R, demand, demand]

    implicit def con5[R, T]: RateCons[R, demand , scalar] = 
      new ConImpl[R, demand, scalar]
  }
  object RateCons extends LowPri {
    implicit def con6[R]: RateCons[R, demand, R] = new ConImpl[R, demand, R]
  }
  private class ConImpl[ R, S, T ] extends RateCons R, S, T ]
  sealed trait RateCons[ R, S, T ]

  def ar[S <: Rate, T <: Rate](in0: GE[S], in1: GE[T])(
    implicit cons: RateCons[audio, S, T]) = apply[audio, S, T](in0, in1)

  def kr[S <: Rate, T <: Rate](in0: GE[S], in1: GE[T])( 
    implicit cons: RateCons[control, S, T]) = apply[control, S, T](in0, in1)
}
case class Duty[R <: Rate, S <: Rate, T <: Rate](in0: GE[S], in1: GE[T])(
  implicit con: Duty.RateCons[R, S, T]) extends GE[R]

测试:

def allowed(a: GE[demand], b: GE[audio], c: GE[control], d: GE[scalar]): Unit = {
  Duty.ar(b, c)
  Duty.kr(b, c)
  Duty.ar(b, a)
  Duty.ar(b, d)
  Duty.ar(a, b)
  Duty.kr(a, c)
}

def forbidden(a: GE[demand], b: GE[audio], c: GE[control], d: GE[scalar]): Unit = {
  Duty.kr(a, b)
  Duty.ar(a, c)
}

一条值得追求的路径?除了代码膨胀之外,还有另外三件事反对它:

  • 可能有几十个 GE 需要自定义约束
  • 组合 GE 变得越来越困难: 代码可能需要传递数十个类型参数
  • 转换可能会变得困难,例如想象一个 List[GE[_<:Rate]].map( ??? )。我的意思是 Duty.RateCons 如何转换为 TDuty.RateCons (其中 TDuty 是不同的 GE)。我

已经在这个项目上投入了相当多的时间,所以我不愿意轻易放弃。所以...说服我我在这里做了一些有用的事情,或者告诉我我应该回到动态检查的版本。

Given the strong type system of Scala, I had an ambitious project which I'm about to abandon now because the effort to usefulness ratio seems to be too high.

Basically I have some graph elements (GE) and they correspond to sound processes which are carried out at a given calculation rate. Graph elements are composed from other graph elements forming their inputs. Now there are rather arbitrary constraints on the inputs' rates. In the source language (SuperCollider) the rates are checked at runtime, naturally because it's a dynamically typed language. I wanted to see if I can enforce the check at compile time.

Some constraints are fairly simply and can be expressed in the forms of "rate of arg1 must be at least as high as rate of arg2". But others get intricate, e.g.

"if arg0's rate is 'demand', args1's rate must be either 'demand' or 'scalar' or equal to the enclosing GE's rate".

The question is: Should I give up on this? Here is how it looks with runtime check:

sealed trait Rate
case object demand  extends Rate
case object audio   extends Rate
case object control extends Rate
case object scalar  extends Rate

trait GE { def rate: Rate }

// an example GE:
case class Duty(rate: Rate, in0: GE, in1: GE) extends GE {
  def checkRates(): Unit =
    require(in0.rate != demand || (in1.rate != demand &&
            in1.rate != scalar && in1.rate != rate))
}

And in constrast how it could look with type parameters for the rates:

sealed trait Rate
trait audio   extends Rate
trait demand  extends Rate
trait control extends Rate
trait scalar  extends Rate

trait GE[R <: Rate]

object Duty {
  trait LowPri {
    implicit def con1[R, T]: RateCons[R, audio  , T] = new ConImpl[R, audio  , T]
    implicit def con2[R, T]: RateCons[R, control, T] = new ConImpl[R, control, T]
    implicit def con3[R, T]: RateCons[R, scalar , T] = new ConImpl[R, scalar , T]

    implicit def con4[R, T]: RateCons[R, demand , demand] = 
      new ConImpl[R, demand, demand]

    implicit def con5[R, T]: RateCons[R, demand , scalar] = 
      new ConImpl[R, demand, scalar]
  }
  object RateCons extends LowPri {
    implicit def con6[R]: RateCons[R, demand, R] = new ConImpl[R, demand, R]
  }
  private class ConImpl[ R, S, T ] extends RateCons R, S, T ]
  sealed trait RateCons[ R, S, T ]

  def ar[S <: Rate, T <: Rate](in0: GE[S], in1: GE[T])(
    implicit cons: RateCons[audio, S, T]) = apply[audio, S, T](in0, in1)

  def kr[S <: Rate, T <: Rate](in0: GE[S], in1: GE[T])( 
    implicit cons: RateCons[control, S, T]) = apply[control, S, T](in0, in1)
}
case class Duty[R <: Rate, S <: Rate, T <: Rate](in0: GE[S], in1: GE[T])(
  implicit con: Duty.RateCons[R, S, T]) extends GE[R]

Tests:

def allowed(a: GE[demand], b: GE[audio], c: GE[control], d: GE[scalar]): Unit = {
  Duty.ar(b, c)
  Duty.kr(b, c)
  Duty.ar(b, a)
  Duty.ar(b, d)
  Duty.ar(a, b)
  Duty.kr(a, c)
}

def forbidden(a: GE[demand], b: GE[audio], c: GE[control], d: GE[scalar]): Unit = {
  Duty.kr(a, b)
  Duty.ar(a, c)
}

A path worth pursuing? Three more things that speak against it, apart from the code bloat:

  • There are probably a couple of dozen GEs which would need custom constraints
  • Composing GEs becomes increasingly difficult: code might need to pass around dozens of type parameters
  • Transformations might become difficult, e.g. imagine a List[GE[_<:Rate]].map( ??? ). I mean how would Duty.RateCons translate to TDuty.RateCons (where TDuty is a different GE)...

I had invested quite a bit of time in this project already, that's why I'm reluctant to give up so easily. So... convince me that I'm doing something useful here, or tell me that I should go back to the dynamically checked version.

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(1

御守 2024-11-06 12:47:15

正如 Jesper Nordenberg 所提到的,要做的事情是定义一组封闭的类型以及对这些类型的相等操作。如果您确实重新审视这个问题,那么最好提供一个如何解决该问题的示例。此外,提问者所需的类型级编程示例也是可取的。

了解更多此处以及此处

As mentioned by Jesper Nordenberg, the thing to do is define a closed set of types and an equality operation over those types. If you do revisit this problem, an example of how you solved it would be desirable. Also, an example of type-level programming of the sort required by the questioner is desirable.

Read more here and here.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文