如何在 GADT 中表示此 FSM

Posted 2023-03-15

【中文标题】如何在 GADT 中表示此 FSM

【英文标题】：How to represent this FSM in GADT

【发布时间】：2022-01-06 00:02:43

【问题描述】：

我正在观看 this 视频并了解了 Scala 中的 GADT。

我能够代表下面的状态机

这是我的代码

type Idle
type Moving

enum Direction:
  case East, West, North, South
import Direction.*

enum Command[From, To]:
  case Turn(direction: Direction) extends Command[Idle, Idle]
  case Start extends Command[Idle, Moving]
  case Stop extends Command[Moving, Idle]
  case Chain[A, B, C](command1: Command[A, B], command2: Command[B, C])
      extends Command[A, C]

import Command.*

extension [A, B, C](command1: Command[A, B])
  infix def ~>(command2: Command[B, C]): Command[A, C] =
    Chain(command1, command2)

现在我想改变一个细节。我想在Idle 和Moving 时赋予Turn 的能力。在Turn 命令之后，我希望机器保留它所处的任何状态。例如，如果机器正在移动并且需要转弯，我希望状态机保留该信息。

例如 Start ~> Turn(West) 应该是 Command[Idle,Moving] & Start ~> Stop ~> Turn(West) 应该是 Command[Idle,Idle]

【参考方案1】：

我通过在Turn 命令 中添加类型参数来解决它