如何实现索引核心风格索引状态monad？ [英] How to implement index-core style indexed state monad?

问题描述

我试图了解 index-core中的索引monad 风格。我陷入了一个悖论，那就是在构造了一些例子之前，我无法理解这些原则，直到我理解了这些原则之后，我才能构建示例。

我试图构建一个索引状态monad。到目前为止，我的直觉告诉我应该是这样的： 一世。 （a i，b i）
newtype ISATE f a i = IState {runIState :: f i - > （a：* f）}

，我可以通过设置 f =身份并恰当地选择 a ：

  type IState's s'a = IState Identity（a：= s'）s 
  

但是我感觉很失落。有人可以确认我是正确的吗？

我正在使用 $ b对于实施索引核心风格索引延续monad>类似的索引延续单元格问题 $ b

解决方案

我们可以从链接的索引 Cont answer答复Gabriel的参数。如果标准索引状态monad是

  State s s'a = s  - > （a，s'）
  

然后我们分阶段推广它。首先使用 Identity 来反映具体类型 s 和 s'作为索引类型空间中的纤维标识。

 国家s'a = s  - > （a，s'）
〜身份s  - > （a，Identity s'）
  

然后通过泛化值类型 a 到索引类型以及目标索引，类型 s'。

 〜身份s  - > （a，身份s'）
〜身份s  - > （a's，Identity s'）
  

然后通过使用存在类型来擦除目标索引。我们会在稍后恢复。

 数据a：* b =全部i。 P（a i）（b i）
 
身份s  - > （a s'，身份s'）
〜身份s  - > P a Identity 
  

最后，我们会注意到 Identity 是状态空间的索引类型， a 是值空间的索引类型，所以我们可以写 IState as

  newtype IState s  - 索引状态空间
a  - 索引值空间
i  - 索引
 = IState {runIState :: si  - > a：* s} 
  -  State {runState :: s  - > （a，s）}用于比较
  

---

一个存在量化的对而不是一个普遍量化的一对？第一个推理来自与 a 相关的索引在 IState 中出现正值，而在 ICONT 。第二个提示来自 returnI 。如果我们使用通用量化版本并尝试编写 returnI

  newtype ISATE'sai = IState'{runIState':: si  - > （forall i。（a i，s i））} 
 
 returnI :: a i  - > ISATE'sai 
 returnI a = IState'（\si  - >（？forget a，？forget si））
  

我们需要有这个忘记函数，它会忘记所有关于索引的信息。

$ b $然而，如果我们使用存在量化的对，那么它取决于返回对的构造函数，即 IState 值的实现者来选择索引。这让我们实例化 IFunctor 和 IMonad

 实例IFunctor（IState s）其中
  -  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）其中
  -  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  - > 
案例runIState m s of 
 P ax sx  - > runIState（f ax）sx 
  

使用这个存在对的唯一缺点是它是..很难实际使用。例如，我们真的希望能够使用指向的索引类型构造函数（：=）来修复已知索引和项目的存在

  one ::（a：= i：* b） - > a 
 two ::（a：= i：* b） - > bi 
  

不幸的是，即使我们知道它是什么，Haskell也不够聪明以强制存在，所以这些预测的第二个有一个令人讨厌的实现

  one ::（a：= i：* b） - > a 
 one（P（V a）_）= a 
 
 two ::（a：= i：* b） - > bi 
 two（P _ s）= unsafeCoerce s 
  

---

最后，证明是在布丁中。我们可以使用 IState 来实现我们习惯看到的有状态效果的标准补充。

   - 高位单位类型
数据U1 a = U1 
 
 put :: si  - > IState s U1 j 
 put s = IState（\_-> P U1 s）
 
 get :: IState ssi 
 get = IState（\ s  - > P ss）
  

并用它们来实现一些通用的更高阶的组合器，例如modify（它需要一个明确的类型签名，但是你可以通过一些想法手动计算）

  modify ::（s： - > s ） - > IState s U1 i 
修改f = get？> = put。然而，除了这些之外，我们还有其他方式来表示组合子，这些组合子更加明确地说明了组合子通过（：=）限制索引。这可以用来传递更多关于索引的信息。
  put':: s i1  - > IState s（（）：= i1）i 
 put's = IState（\_-> P（V（））s）
 
 get':: IState s（si ：= i）i 
 get'= IState（\ s  - > P（V s）s）
 
 modify'::（s  - > s） - > IState（s：= j）（（）：= j）i 
修改'f = get>> = put'。 V。 f 
 
修改''::（s i  - > s k） - > IState s（（）：= k）i 
修改''f = get'>> = put'。 f 
  
最后，我们可以使用所有这些来实现一个示例。例如，我们可以通过文件句柄状态建立索引类型，而不是它非常有用。
  data打开
数据已关闭
数据任何
 
数据St其中
 So :: Int  - > St Open 
 Sc :: St Closed 
 Sa :: a  - > St（Any a）
 
 getAny :: St（Any a） - > a 
 getAny（Sa a）= a 
  
然后我们可以建立
  open :: String  - >文件关闭打开（）
 open name = put'（SOpen $ getHandle name）其中
 getHandle =长度
 
关闭::文件打开关闭（）
 close =把'SClosed 
 
 getHandle :: File Open Open Int 
 getHandle = do 
 SOpen i<  -  get'
 return i 
 
 putA :: a  - > File x（Any a）（）
 putA a = put'（SAny a）
  
  
 
 
 打开foo>> close  -  typechecks 
打开foo>>关闭>>关闭 - 失败
打开foo>> getHandler>> close  -  typechecks 
打开foo>>关闭>> getHandler  - 失败
  
以及像 
 
 
 >一个$ runIState（做putA 4 
 sa<  -  get'
 return（getAny sa））Sc 
 4 
>一个$ runIState（做putA（）
 sa<  -  get'
 return（getAny sa））Sc 
（）
>一个$ runIState（做putA 4 
 putA（）
 sa<  -  get'
 return（getAny sa））Sc 
（）
  
全部工作。
 
I'm trying to understand indexed monads in the index-core style.  I have become stuck in a paradox which is that I can't understand the principles until I have constructed a few examples, and I can't construct examples until I understand the principles.

I am trying to construct an indexed state monad.  So far my intuition tells me it should be something like this
type a :* b = forall i. (a i, b i)
newtype IState f a i = IState { runIState :: f i -> (a :* f) }
and that I can recover the "restricted" state monad by setting f = Identity and choosing a appropriately:
type IState' s s' a = IState Identity (a := s') s
But I'm feeling rather lost.  Can someone confirm that I'm on the right lines?

I'm using a similar question on the indexed continuation monad as a guide, but I don't think it's really close enough.
解决方案
We can replicate Gabriel's argument from the indexed Cont answer linked. If the standard index state monad is
State s s' a = s -> (a, s')
then we generalize it in stages. First by using Identity to reflect the concrete types s and s' as fibers in the indexed type space Identity. 
State s s' a = s          -> (a, s')
             ~ Identity s -> (a, Identity s')
then by generalizing the value type a to an indexed type as well over the "destination" index, the type s'.
             ~ Identity s -> (a   , Identity s')
             ~ Identity s -> (a s', Identity s')
and then by using an existential type to erase the destination index. We'll recover it later.
data a :* b = forall i . P (a i) (b i)

  Identity s -> (a s', Identity s') 
~ Identity s -> P a Identity
Finally, we'll note that Identity is the indexed type of the state space and a the indexed type of the value space, so we can write IState as
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




Why use an existentially quantified pair instead of a universally quantified one? A first nudge comes from the fact that the index associated with a is occurring positively in IState while it appeared negatively in ICont. A second hint comes from writing returnI. If we use the universally quantified version and try to write 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))
we would need to have this forget function which forgets all of the information about the index.

However, if we instead use the existentially quantified pair then it's up to the constructor of that returning pair, i.e. the implementor of the IState value, to pick the index. This lets us instantiate IFunctor and 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
The only downside to the use of this existential pair is that it's... pretty hard to actually use. For instance, we'd really like to be able to use the "pointed" indexed type constructor (:=) in order to fix a known index and project out of the existential pair.
one :: (a := i :* b) -> a
two :: (a := i :* b) -> b i
Unfortunately, Haskell isn't smart enough to coerce the existential even when we know what it it is, so the second of these projections has an unsavory implementation
one :: (a := i :* b) -> a
one (P (V a) _) = a

two :: (a := i :* b) -> b i
two (P _ s) = unsafeCoerce s




Finally, the proof is in the pudding. We can use IState to implement the standard complement of stateful effects we're used to seeing.
-- 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)
and use them to implement some general higher order combinators such as modify (which needs an explicit type signature, but you can compute that from the implementation manually with some thought)
modify :: (s :-> s) -> IState s U1 i
modify f = get ?>= put . f
However, additionally to these, we have other ways of representing the combinators that are more explicit about the indexing due to restriction via (:=). This can be useful in order to pass around more information about the indexing.
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
Finally, we can use all this to implement an example. For instance, we can build the indexed type over file handle states not that it's tremendously useful.
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
Then we can build
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)
where
open "foo" >> close                -- typechecks
open "foo" >> close >> close       -- fails
open "foo" >> getHandler >> close  -- typechecks
open "foo" >> close >> getHandler  -- fails
and things like
> 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
()
all work.

                        
这篇关于如何实现索引核心风格索引状态monad？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！