核心风格索引状态monad？
我试图理解索引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和选择a适当的：
type IState' s s' a = IState Identity (a := s') s
但我感觉很失落。 有人可以确认我在正确的路线吗？
我在索引连续monad上使用了一个类似的问题作为指导，但我认为它不够接近。
我们可以从被索引的Cont回答中复制Gabriel的观点。 如果标准索引状态monad是
State s s' a = s -> (a, s')
那么我们分阶段推广它。 首先通过使用Identity将索引类型空间Identity的具体类型s和s'反映为纤维。
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
使用这个存在对的唯一缺点是它很难实际使用。 例如，我们真的希望能够使用“指向”索引类型构造函数(:=)来修复已知索引和项目中的存在对。
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
()
所有的工作。
链接地址: http://www.djcxy.com/p/79275.html