如何使用类型系统编码和执行合法的FSM状态转换？ [英] How can I encode and enforce legal FSM state transitions with a type system?

问题描述

假设我有一个 Thing 类型的状态属性 A | B | C ，

和合法状态转换是 A-> B，A-> C，C-> A

我可以这样写：

transitionToA :: Thing - >如果 Thing

会返回 Nothing / code>处于无法转换为 A 的状态。

但我想定义我的类型和转换函数，以便只能在适当的类型上调用转换。

一个选项是创建单独的类型 AThing BThing CThing ，但在复杂情况下似乎不可维护。

另一种方法是将每个状态编码为自己的类型：

  data A = A Thing 
 data B = B Thing 
 data C = C Thing 
  

和

transitionCToA :: C Thing - >一件事

这对我来说似乎更清洁。但是在我看来，A，B，C是函子，除了过渡函数外，所有的东西函数都可以被映射。

使用类型类我可以创建如下类：

  class ToA t其中
 toA :: t  - >一件事
  

这看起来更干净。

是否有其他首选的方法可以在Haskell和PureScript中工作？

解决方案这是一个非常简单的方法，它使用（可能是幻影）类型参数来跟踪哪个状态

  { - ＃LANGUAGE DataKinds，KindSignatures＃ - } 
  -  - 注意：不导出Thing 
模块的构造函数Thing（Thing，transAB，transAC，transCA）其中
 
 data State = A | B | C 
数据Thing（s :: State）= { -  elided;甚至可以成为一个数据族 - } 
 
 transAB :: Thing A  - >事情B 
 transAC ::事情A  - >事情C 
 transCA ::事情C  - >事情A 
 
 transAB = { -  elided  - } 
 transAC = { -  elided  - } 
 transCA = { -  elided  - } 
  

Suppose I have a type Thing with a state property A | B | C,
and legal state transitions are A->B, A->C, C->A.

I could write:

transitionToA :: Thing -> Maybe Thing

which would return Nothing if Thing was in a state which cannot transition to A.

But I'd like to define my type, and the transition functions in such a way that transitions can only be called on appropriate types.

An option is to create separate types AThing BThing CThing but that doesn't seem maintainable in complex cases.

Another approach is to encode each state as it's own type:

data A = A Thing
data B = B Thing
data C = C Thing

and

transitionCToA :: C Thing -> A Thing

This seems cleaner to me. But it occurred to me that A,B,C are then functors where all of Things functions could be mapped except the transition functions.

With typeclasses I could create somthing like:

class ToA t where  
    toA :: t -> A Thing

Which seems cleaner still.

Are there other preferred approaches that would work in Haskell and PureScript?

解决方案

Here's a fairly simple way that uses a (potentially phantom) type parameter to track which state a Thing is in:

{-# LANGUAGE DataKinds, KindSignatures #-}
-- note: not exporting the constructors of Thing
module Thing (Thing, transAB, transAC, transCA) where

data State = A | B | C
data Thing (s :: State) = {- elided; can even be a data family instead -}

transAB :: Thing A -> Thing B
transAC :: Thing A -> Thing C
transCA :: Thing C -> Thing A

transAB = {- elided -}
transAC = {- elided -}
transCA = {- elided -}

这篇关于如何使用类型系统编码和执行合法的FSM状态转换？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！