Как я могу кодировать и применять законные переходы состояния FSM с системой типов?

Предположим, что у меня есть тип Thing с свойством состояния A | B | C,
и переходы законного состояния A->B, A->C, C->A.

Я мог бы написать:

transitionToA :: Thing -> Maybe Thing

который возвратил бы Nothing, если Thing находился в состоянии, которое не может перейти на A.

Но я бы хотел определить свой тип и функции перехода таким образом, чтобы переходы можно было вызывать только для соответствующих типов.

Опция заключается в создании отдельных типов AThing BThing CThing, но в сложных случаях это не выглядит удобным.

Другой подход заключается в кодировании каждого состояния в виде собственного типа:

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

и

transitionCToA :: C Thing -> A Thing

Это кажется мне более чистым. Но мне пришло в голову, что A, B, C являются функторами, где все функции Things могут отображаться, кроме функций перехода.

С классами я мог бы создать somthing как:

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

Что кажется еще более чистым.

Существуют ли другие предпочтительные подходы, которые будут работать в Haskell и PureScript?

Ответы

Ответ 1

Здесь довольно простой способ использования параметра типа (потенциально phantom) для отслеживания состояния a Thing:

{-# 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 -}

Ответ 2

Вы можете использовать класс типа (доступен в PureScript) вместе с phantom типами, как предложил Джон, но используя класс типа в качестве окончательной кодировки типа путей:

data A -- States at the type level
data B
data C

class Path p where
  ab :: p A B -- One-step paths
  ac :: p A C
  ca :: p C A
  trans :: forall a b c. p c b -> p b a -> p c a -- Joining paths
  refl :: forall a. p a a

Теперь вы можете создать тип допустимых путей:

type ValidPath a b = forall p. (Path p) => p a b

roundTrip :: ValidPath A A
roundTrip = trans ca ac

Контуры могут создаваться только с использованием одноэтапных путей, которые вы предоставляете.

Вы можете писать экземпляры для использования ваших путей, но, что важно, любой экземпляр должен уважать действительные переходы на уровне типа.

Например, здесь представлена ​​интерпретация, которая вычисляет длины путей:

newtype Length = Length Int

instance pathLength :: Path Length where
  ab = Length 1
  ac = Length 1
  ca = Length 1
  trans (Length n) (Length m) = Length (n + m)
  refl = Length 0

Ответ 3

Поскольку ваша цель - запретить разработчикам выполнять незаконные переходы, вы можете захотеть просмотреть типы phantom. phantom типы позволяют моделировать безопасные типы без использования более сложных функций системы типов; поэтому они переносимы на многие языки.

Здесь PureScript-кодирование вашей проблемы:

foreign import data A :: *
foreign import data B :: *
foreign import data C :: *

data Thing a = Thing

transitionToA :: Thing C -> Thing A

Phantom хорошо работают, чтобы моделировать допустимые переходы состояния, когда у вас есть свойство, чтобы два разных состояния не могли перейти в одно и то же состояние (если только все состояния не могут перейти в это состояние). Вы можете обойти это ограничение, используя классы типов (class CanTransitionToA a where trans :: Thing a -> Thing A), но на этом этапе вам следует исследовать другие подходы.

Ответ 4

Если вы хотите сохранить список переходов, чтобы вы могли его обработать позже, вы можете сделать что-то вроде этого:

{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds #-}

data State = A | B | C
data Edge (a :: State) (b :: State) where
    EdgeAB :: Edge A B
    EdgeAC :: Edge A C
    EdgeCA :: Edge C A

data Domino (f :: k -> k -> *) (a :: k) (b :: k)  where
    I :: Domino f a a
    (:>>:) :: f a b -> Domino f b c -> Domino f a c

infixr :>>:

example :: Domino Edge A B
example = EdgeAC :>>: EdgeCA :>>: EdgeAB :>>: I

Вы можете превратить это в экземпляр Path, написав функцию конкатенации для Domino:

{-# LANGUAGE FlexibleInstances #-}
instance Path (Domino Edge) where
    ab = EdgeAB :>>: I
    ac = EdgeAC :>>: I
    ca = EdgeCA :>>: I

    refl = I
    trans I es' = es'
    trans (e :>>: es) es' = e :>>: (es `trans` es')

На самом деле это заставляет меня задаться вопросом, имеет ли Hackage пакет, который определяет "индексированные моноиды":

class IMonoid (m :: k -> k -> *) where
    imempty :: m a a
    imappend :: m a b -> m b c -> m a c

instance IMonoid (Domino e) where
    imempty = I
    imappend I es' = es'
    imappend (e :>>: es) es' = e :>>: (es `imappend` es')