狀態機的索引單子

我決定嘗試使用索引單子來創建一個型別安全的狀態機。這意味著 Haskell 將拒絕編譯非法的狀態轉換。我的問題是。

1. 我創建了一個帶有操作的 Door 型別。不可能為它撰寫非法的狀態轉換，例如它不能為已經關閉的門呼叫 close。這段代碼作業正常，但我有一個問題：它可以更好嗎？也許它可以被增強，用有用的東西等擴展。
2. 我試圖創建一個基于索引的免費 monad 的 DSL，但我失敗了。有人能幫我嗎？

這是我的代碼：

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
import Control.Monad.Indexed
import Control.Monad.Indexed.Free
import Data.Coerce
import Language.Haskell.DoNotation
import Prelude hiding (Monad (..), pure)
import qualified Prelude (pure)

-- Handy Indexed container type borrowed from Sandy Maguire
newtype Indexed m i j a = Indexed { unsafeRunIndexed :: m a }
  deriving (Functor, Applicative, Monad)

instance Functor m => IxFunctor (Indexed m) where
  imap :: (a -> b) -> Indexed m i j a -> Indexed m i j b
  imap = fmap

instance Applicative m => IxPointed (Indexed m) where
  ireturn :: a -> Indexed m i i a
  ireturn = Prelude.pure

instance Applicative m => IxApplicative (Indexed m) where
  iap :: forall i j k a b. Indexed m i j (a -> b) -> Indexed m j k a -> Indexed m i k b
  iap = coerce $ (<*>) @m @a @b

instance Monad m => IxMonad (Indexed m) where
  ibind :: forall i j k a b. (a -> Indexed m j k b) -> Indexed m i j a -> Indexed m i k b
  ibind = coerce $ (=<<) @m @a @b

-- Door stuff
data DoorState = Opened | Closed deriving (Show, Eq, Ord)

newtype Door s (i :: DoorState) (j :: DoorState) a = Door
  { unsafeRunDoor :: Indexed IO i j a }
  deriving (IxFunctor, IxPointed, IxApplicative, IxMonad)

runDoor :: (forall s . Door s st1 st2 a) -> IO a
runDoor = coerce

class State (a :: DoorState) where
  state :: DoorState
instance State 'Opened where
  state = Opened
instance State 'Closed where
  state = Closed

stateM :: forall a m . (State a, Monad m) => m DoorState
stateM = return (state @a)

getState :: forall s st . State st => Door s st st DoorState
getState = coerce $ stateM @st @IO

openDoor :: Door s 'Closed 'Opened ()
openDoor = coerce $ putStrLn "open!"

closeDoor :: Door s 'Opened 'Closed ()
closeDoor = coerce $ putStrLn "close!"

ringBell :: Door s 'Closed 'Closed ()
ringBell = coerce $ putStrLn "ring!"
  
displayMessage :: String -> Door s st st ()
displayMessage = coerce . putStrLn

doorProgram :: Door s 'Closed 'Closed ()
doorProgram = do
  ringBell
  openDoor
  st <- getState
  displayMessage $ "State is: "    show st
  closeDoor

現在有問題的代碼：

• 預期種類 '* -> * -> * -> *'，但 'DoorF' 有種類 'DoorState -> DoorState -> * -> *'
• 在 'IxFree' 的第一個引數中，即 'DoorF'
• 在“IxFree DoorF”型別中
• 在“DoorDSL”的型別宣告中

任何想法如何為門創建免費的索引 monad DSL？

data DoorF (i :: DoorState) (j :: DoorState) next where
  Open    :: next -> DoorF 'Closed 'Opened next
  Close   :: next -> DoorF 'Opened 'Closed next
  Ring    :: next -> DoorF 'Closed 'Closed next
  Display :: String -> next -> DoorF st st next
  State   :: (DoorState -> next) -> DoorF st st next

instance Functor (DoorF i j) where
  fmap f (Open next) = Open (f next)
  fmap f (Close next) = Close (f next)
  fmap f (Ring next) = Ring (f next)
  fmap f (Display s next) = Display s (f next)
  fmap f (State nextF) = State (f . nextF)

instance IxFunctor DoorF where
  imap = fmap

type DoorDSL = IxFree DoorF

更新：Li-yao Xia 回答了我的問題。這是免費索引單子 DSL 的作業版本：

data Opened
data Closed

data DoorF i j next where
  Open    :: next -> DoorF Closed Opened next
  Close   :: next -> DoorF Opened Closed next
  Ring    :: next -> DoorF Closed Closed next
  Display :: String -> next -> DoorF st st next

instance Functor (DoorF i j) where
  fmap f (Open next) = Open (f next)
  fmap f (Close next) = Close (f next)
  fmap f (Ring next) = Ring (f next)
  fmap f (Display s next) = Display s (f next)

instance IxFunctor DoorF where
  imap = fmap

type DoorDSL = IxFree DoorF

open :: DoorDSL Closed Opened ()
open = Free (Open (Pure ()))

close :: DoorDSL Opened Closed ()
close = Free (Close (Pure ()))

ring :: DoorDSL Closed Closed ()
ring = Free (Ring (Pure ()))

display :: String -> DoorDSL st st ()
display msg = Free (Display msg (Pure ()))

uj5u.com熱心網友回復：

錯誤是因為IxFree當它可以被推廣時是單態的。該indexed-free庫應該被修補以使用PolyKinds.

同時，一種解決方法是DataKind將建構式宣告DoorState為它們自己的資料型別，而不是 ：

-- Promoted DoorState without DataKind
type DoorState' = Type
data Opened
data Closed

標籤：哈斯克尔 单子 自由单子

上一篇：GHC是否為`mapM_`生成優化代碼？

下一篇：從自定義資料型別中獲取值