路径依赖类型：Idris到Scala

2023年6月29日 225次阅读

我从Idris到
Scala的
Type-Driven Development with Idris写了一个例子：

伊德里斯(取自伊德里斯的TDD)

data PowerSource = Petrol | Pedal

data Vehicle : PowerSource -> Type where
           Bicycle : Vehicle Pedal
           Car : (fuel : Nat) -> Vehicle Petrol
           Bus : (fuel : Nat) -> Vehicle Petrol

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200

斯卡拉

scala> sealed trait PowerSource 
defined trait PowerSource

scala> case object Petrol extends PowerSource
defined object Petrol

scala> case object Pedal extends PowerSource
defined object Pedal

scala> sealed abstract class Vehicle {
     |   type A <: PowerSource
     | }
defined class Vehicle

scala> case object Bicycle extends Vehicle {
     |   type A = Pedal.type
     | }

scala> case class Bus(fuel: Int) extends Vehicle {
     |   type A = Petrol.type
     | }
defined class Bus

scala> case class Car(fuel: Int) extends Vehicle {
     |   type A = Petrol.type
     | }

但是,我在尝试实施加油时遇到了麻烦：

scala> def refuel[P <: Petrol.type](vehicle: Vehicle {type A = P} ): Vehicle = vehicle match {
     |   case Car(_) => Car(100)
     |   case Bus(_) => Bus(100)
     | }
<console>:20: warning: unreachable code
         case Bus(_) => Bus(100)
                           ^
refuel: [P <: Petrol.type](vehicle: Vehicle{type A = P})Vehicle

scala> refuel(Car(100))
res6: Vehicle = Car(100)

scala> refuel(Bus(5))
res7: Vehicle = Bus(100)

scala> refuel(Bicycle)
<console>:22: error: inferred type arguments [Bicycle.A] do not conform to method refuel's type parameter bounds [P <: Petrol.type]
       refuel(Bicycle)
       ^
<console>:22: error: type mismatch;
 found   : Bicycle.type
 required: Vehicle{type A = P}
       refuel(Bicycle)
              ^

请批评/纠正我的方法,并帮助我在Scala加油.

最佳答案 无法访问的代码警告似乎是虚假的：如果它不是你能够强制一个总线到一个汽车(这是不健全的)并导致ClassCastExeception ……似乎是不可能的.

虚假警告是一个scalac bug. Scala问题跟踪器中存在相关错误,但这似乎是一个不同的变体……您应该报告它.

点赞