我试图理解 index-core
中的索引单子(monad)风格。我陷入了一个悖论,就是在我构建了几个例子之前我无法理解原理,而我在理解原理之前我无法构建例子。
我正在尝试构建一个索引状态单子(monad)。到目前为止,我的直觉告诉我应该是这样的
type a :* b = forall i. (a i, b i)
newtype IState f a i = IState { runIState :: f i -> (a :* f) }
并且我可以通过设置
f = Identity
来恢复“受限”状态 monad并选择 a
适本地:type IState' s s' a = IState Identity (a := s') s
但我感觉有点失落。有人可以确认我在正确的路线上吗?
我正在使用 a similar question on the indexed continuation monad作为指南,但我认为它还不够接近。
最佳答案
我们可以从索引 Cont
复制 Gabriel 的论点。答案链接。如果标准索引状态单子(monad)是
State s s' a = s -> (a, s')
然后我们分阶段概括它。首先使用
Identity
反射(reflect)具体类型s
和 s'
作为索引类型空间中的纤维 Identity
.State s s' a = s -> (a, s')
~ Identity s -> (a, Identity s')
然后通过推广值类型
a
到索引类型以及“目标”索引,类型 s'
. ~ Identity s -> (a , Identity s')
~ Identity s -> (a s', Identity s')
然后通过使用存在类型删除目标索引。我们稍后会恢复它。
data a :* b = forall i . P (a i) (b i)
Identity s -> (a s', Identity s')
~ Identity s -> P a Identity
最后,我们会注意到
Identity
是状态空间的索引类型,a
值空间的索引类型,所以我们可以写成 IState
作为newtype IState s -- indexed state space
a -- indexed value space
i -- index
= IState { runIState :: s i -> a :* s }
-- State { runState :: s -> (a, s) } for comparison
为什么使用存在量化的对而不是普遍量化的对?第一个插入来自与
a
关联的索引这一事实。在 IState
中积极发生虽然它在 ICont
中出现了负面影响.第二个提示来自写作 returnI
.如果我们使用普遍量化的版本并尝试写returnI
newtype IState' s a i = IState' { runIState' :: s i -> (forall i . (a i, s i)) }
returnI :: a i -> IState' s a i
returnI a = IState' (\si -> (?forget a, ?forget si))
我们需要这个
forget
忘记有关索引的所有信息的函数。但是,如果我们改为使用存在量化对,则取决于该返回对的构造函数,即
IState
的实现者。值,选择索引。这让我们可以实例化 IFunctor
和 IMonad
instance IFunctor (IState s) where
-- fmapI :: (a :-> b) -> IState s a :-> IState s b
fmapI phi (IState go) = IState $ \si ->
case go si of
P ax sx -> P (phi ax) sx
instance IMonad (IState s) where
-- returnI :: a :-> IState s a
return ai = IState (\si -> P ai si)
-- bindI :: (a :-> IState s b) -> (IState s a :-> IState s b)
bindI f m = IState $ \s ->
case runIState m s of
P ax sx -> runIState (f ax) sx
使用这个存在对的唯一缺点是它......实际上很难使用。例如,我们真的希望能够使用“pointed”索引类型构造函数
(:=)
为了修复已知索引并从存在对中投影出来。one :: (a := i :* b) -> a
two :: (a := i :* b) -> b i
不幸的是,即使我们知道存在主义是什么,Haskell 也不够聪明,无法强制存在主义,所以这些预测中的第二个有一个令人讨厌的实现
one :: (a := i :* b) -> a
one (P (V a) _) = a
two :: (a := i :* b) -> b i
two (P _ s) = unsafeCoerce s
最后,证据就在布丁中。我们可以使用
IState
实现我们习惯看到的有状态效果的标准补充。-- Higher order unit type
data U1 a = U1
put :: s i -> IState s U1 j
put s = IState (\_ -> P U1 s)
get :: IState s s i
get = IState (\s -> P s s)
并使用它们来实现一些通用的高阶组合器,例如修改(这需要一个显式的类型签名,但您可以通过一些想法手动从实现中计算它)
modify :: (s :-> s) -> IState s U1 i
modify f = get ?>= put . f
然而,除此之外,我们还有其他表示组合子的方法,这些组合子由于受到
(:=)
的限制而对索引更加明确。 .这对于传递有关索引的更多信息很有用。put' :: s i1 -> IState s (() := i1) i
put' s = IState (\_ -> P (V ()) s)
get' :: IState s (s i := i) i
get' = IState (\s -> P (V s) s)
modify' :: (s -> s) -> IState (s := j) (() := j) i
modify' f = get >>= put' . V . f
modify'' :: (s i -> s k) -> IState s (() := k) i
modify'' f = get' >>= put' . f
最后,我们可以使用所有这些来实现一个示例。例如,我们可以在文件句柄状态上构建索引类型,但这并不是非常有用。
data Open
data Closed
data Any a
data St where
So :: Int -> St Open
Sc :: St Closed
Sa :: a -> St (Any a)
getAny :: St (Any a) -> a
getAny (Sa a) = a
然后我们可以构建
open :: String -> File Closed Open ()
open name = put' (SOpen $ getHandle name) where
getHandle = length
close :: File Open Closed ()
close = put' SClosed
getHandle :: File Open Open Int
getHandle = do
SOpen i <- get'
return i
putA :: a -> File x (Any a) ()
putA a = put' (SAny a)
在哪里
open "foo" >> close -- typechecks
open "foo" >> close >> close -- fails
open "foo" >> getHandler >> close -- typechecks
open "foo" >> close >> getHandler -- fails
和类似的东西
> one $ runIState (do putA 4
sa <- get'
return (getAny sa)) Sc
4
> one $ runIState (do putA ()
sa <- get'
return (getAny sa)) Sc
()
> one $ runIState (do putA 4
putA ()
sa <- get'
return (getAny sa)) Sc
()
所有的工作。
关于haskell - 如何实现 index-core 风格的索引状态单子(monad)?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/23887237/