Idris自动售货机

Question

伊德里斯(基于Idris的类型驱动开发)演示了如何使用Idris为自动售货机构建有限状态机。

请批评我的执行情况。我是新的依赖类型，所以我不确定依赖类型是否会增强这种实现。换句话说，如果路径依赖类型会显著改善FSM，那么我不确定如何改进。

module VendingMachine

-- Pounds is a form of currency/money
Pounds : Type
Pounds = Nat

-- the Machine dispenses/vends chocolate candy bars
Choc : Type
Choc = Nat

data Machine = Mach Pounds Choc

fill : Machine -> Nat -> Machine
fill (Mach ps bars) ns = Mach ps (bars + ns)

init : Machine
init = Mach 0 0

insertCoin : Machine -> Machine
insertCoin (Mach ps bars) = (Mach (ps + 1) bars)

vend : Machine -> Machine
vend (Mach Z bars)          = Mach Z bars
vend (Mach (S ps) (S bars)) = Mach ps bars

getChange : Machine -> Machine
getChange (Mach Z bars) = Mach Z bars
getChange (Mach n bars) = Mach 0 bars

Answer 1

我试着搜索和搜索关于如何解决这类问题的变体，所有的搜索都会出现由您发布的帖子或对原始文档和效果库的引用。换句话说，Idris语言没有多少在线文档可供使用，我有点不确定是否值得使用这种语言。不过，我可以对代码和状态机中的一般问题发表一点意见：

• 命名稍微不一致- For类型--我将使用Pounds和ChocolateBars (或Bars)，并在使用参数时使用相应的pounds和bars
• 使用(S pounds)或(pounds + 1)都要保持一致--试着坚持一个特定的表示法来表示递增的版本。Z或0的使用也是如此。保持一致。
• 一条巧克力的价格是多少？如果代码与vend相关的“S”"1磅“，那么使用getChange变体是没有意义的。这更像是一种removePounds方法。
• 国家并不是相互关联的，- I将定义更多的州，而行动显然是与各州相关联的。就目前情况而言，insertCoin、vend和可能的getChange操作之间没有联系。所有这些都可以按任意顺序执行，这取决于自动售货机中磅和棒的可用性。伪代码中的替代版本：
  • Empty - An空自动售货机，没有钱也没有酒吧
    • 操作：fill→状态：Idle：增加bars的数量

- `Idle` - A vending machine with no currently inserted money, but has bars  
    - action: `insertCoin` → state: `ReadyForVending`: changes the `coinInSlot` variable
    - action: `removePounds` → state: `Idle`: Clears the `pounds` variable

- `ReadyForVending` – With inserted money, and bars  
    - action: `vend` → state: `Idle`: Removes one `bars`, and clears `coinInSlot`
    - action: `returnCoin` →  state: `Idle`: Clear the `coinInSlot`

要实现这一点，除了coinInSlot和pounds之外，您还需要另一个状态变量，如bars。

• Machine vs Mach还不清楚--我不确定你是否对这些内容有很好的理解，至少名字有点让人困惑。我认为，与其使用奇怪的Mach额外表示法，不如使用元组或记录来描述内部状态，这也简化了下面的一些代码。
• 对状态机使用效果--我找到的状态机(- In 联机编译器 )--不支持效果，但是我发现的文档(和一些幻灯片/帖子/论文)表明，要正确实现状态机，您应该使用效果库(刽子手)，这在在线编译器中是不支持的。

我试着用http://www.tryidris.org的在线编译器编译一个新版本，但是错误很多，看起来有点不稳定。此外，当试图从OP获得有关您实际如何运行代码和预期输出的信息时，我没有得到多少响应。因此，我无法让您更好地实现Idris中的类型依赖状态机。