gpt4 book ai didi

haskell - 如何以类型编码可能的状态转换?

转载 作者:行者123 更新时间:2023-12-04 07:33:55 26 4
gpt4 key购买 nike

我试图在 Haskell 中复制这段 Idris 代码,它通过类型强制执行正确的操作顺序:

 data DoorState = DoorClosed | DoorOpen
data DoorCmd : Type ->
DoorState ->
DoorState ->
Type where
Open : DoorCmd () DoorClosed DoorOpen
Close : DoorCmd () DoorOpen DoorClosed
RingBell : DoorCmd () DoorClosed DoorClosed
Pure : ty -> DoorCmd ty state state
(>>=) : DoorCmd a state1 state2 ->
(a -> DoorCmd b state2 state3) ->
DoorCmd b state1 state3

感谢 (>>=) 的重载运算符,可以编写一元代码,例如:
do Ring 
Open
Close

但编译器拒绝不正确的转换,例如:
do Ring
Open
Ring
Open

我试图在下面的 Haskell 片段中遵循这种模式:
 data DoorState = Closed | Opened

data DoorCommand (begin :: DoorState) (end :: DoorState) a where
Open :: DoorCommand 'Closed 'Opened ()
Close :: DoorCommand 'Opened 'Closed ()
Ring :: DoorCommand 'Closed 'Closed ()

Pure :: x -> DoorCommand b e x
Bind :: DoorCommand b e x -> (x -> DoorCommand e f y) -> DoorCommand b f y

instance Functor (DoorCommand b e) where
f `fmap` c = Bind c (\ x -> Pure (f x))

-- instance Applicative (DoorCommand b e) where
-- pure = Pure
-- f <*> x = Bind f (\ f' -> Bind x (\ x' -> Pure (f' x')))

-- instance Monad (DoorCommand b e) where
-- return = Pure
-- (>>=) = Bind

但这当然失败了: ApplicativeMonad实例无法正确定义,因为它们需要两个不同的实例来正确排序操作。构造函数 Bind可用于强制执行正确的排序,但我无法设法使用“更好”的 do-notation。

我如何编写此代码才能使用 do-notation,例如防止 Command 的无效序列年代?

最佳答案

你要找的确实是Atkey的parameterised monad ,现在通常称为索引单子(monad)。

class IFunctor f where
imap :: (a -> b) -> f i j a -> f i j b
class IFunctor m => IMonad m where
ireturn :: a -> m i i a
(>>>=) :: m i j a -> (a -> m j k b) -> m i k b
IMonad是类单子(monad)的东西 m :: k -> k -> * -> *描述通过属于类型 k 的类型的有向图的路径. >>>=绑定(bind)从 i 获取类型级状态的计算至 j进入一个从 j 获取的计算至 k ,从 i 返回更大的计算至 k . ireturn允许您将纯值提升为不改变类型级状态的单子(monad)计算。

我将使用索引的自由 monad 来捕获这种请求-响应操作的结构,主要是因为我不想弄清楚如何编写 IMonad我自己的类型的实例:
data IFree f i j a where
IReturn :: a -> IFree f i i a
IFree :: f i j (IFree f j k a) -> IFree f i k a

instance IFunctor f => IFunctor (IFree f) where
imap f (IReturn x) = IReturn (f x)
imap f (IFree ff) = IFree $ imap (imap f) ff
instance IFunctor f => IMonad (IFree f) where
ireturn = IReturn
IReturn x >>>= f = f x
IFree ff >>>= f = IFree $ imap (>>>= f) ff

我们可以建立您的 Door monad 从以下仿函数中免费获得:
data DoorState = Opened | 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

instance IFunctor DoorF where
imap f (Open x) = Open (f x)
imap f (Close x) = Close (f x)
imap f (Ring x) = Ring (f x)

type Door = IFree DoorF

open :: Door Closed Opened ()
open = IFree (Open (IReturn ()))
close :: Door Opened Closed ()
close = IFree (Close (IReturn ()))
ring :: Door Closed Closed ()
ring = IFree (Ring (IReturn ()))

您可以 open一扇门,这会导致当前关闭的门打开, close当前打开的门,或 ring门铃一直关着,大概是因为屋子里的人不想见你。

最后, RebindableSyntax语言扩展意味着我们可以替换标准 Monad类与我们自己的自定义 IMonad .
(>>=) = (>>>=)
m >> n = m >>>= const n
return = ireturn
fail = undefined

door :: Door Open Open ()
door = do
close
ring
open

但是我注意到你并没有真正使用你的 monad 的绑定(bind)结构。没有你的积木 Open , CloseRing返回一个值。所以我认为你真正需要的是以下更简单的类型对齐列表类型:
data Path g i j where
Nil :: Path g i i
Cons :: g i j -> Path g j k -> Path g i k

在操作上, Path :: (k -> k -> *) -> k -> k -> *就像一个链表,但它有一些额外的类型级结构,再次描述了通过有向图的路径,其节点位于 k .列表的元素是边 g . Nil说你总能找到一个节点的路径 i对自己和 Cons提醒我们,千里之行始于一步:如果你有优势 ij以及来自 j 的路径至 k ,您可以将它们组合成一条来自 i 的路径至 k .它被称为类型对齐列表,因为一个元素的结束类型必须与下一个元素的起始类型匹配。

在 Curry-Howard Street 的另一边,如果 g是二元逻辑关系,则 Path g构造它的自反传递闭包。或者,明确地说, Path g是图的自由范畴中的态射类型 g .在自由类别中组合态射只是(翻转)附加类型对齐列表。
instance Category (Path g) where
id = Nil
xs . Nil = xs
xs . Cons y ys = Cons y (xs . ys)

然后我们可以写 Door根据 Path :
data DoorAction i j where
Open :: DoorAction Closed Opened
Close :: DoorAction Opened Closed
Ring :: DoorAction Closed Closed

type Door = Path DoorAction

open :: Door Closed Opened
open = Cons Open Nil
close :: Door Opened Closed
close = Cons Close Nil
ring :: Door Closed Closed
ring = Cons Ring Nil

door :: Door Open Open
door = open . ring . close

你没有得到 do表示法(尽管我认为 RebindableSyntax 确实允许您重载列表文字),但是使用 (.) 构建计算看起来像纯函数的排序,我认为无论如何你都在做一个很好的类比。对我来说,使用索引单子(monad)需要额外的脑力——一种稀有而珍贵的自然资源。当更简单的结构可以做到时,最好避免单子(monad)的复杂性。

关于haskell - 如何以类型编码可能的状态转换?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/40197310/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com