How to implement indexed index status monad with index?

Question

I am trying to understand index-core indexed monads. I am stuck in the paradox that I cannot understand the principles until I build some examples, and I cannot build examples until I understand the principles.

I am trying to build an indexed state monad. As long as my intuition tells me that it should be something like this

 type a :* b = forall i. (ai, bi) newtype IState fai = IState { runIState :: fi -> (a :* f) } 

and that I can restore the "limited" state monad by setting f = Identity and selecting a accordingly:

 type IState' ss' a = IState Identity (a := s') s 

But I feel pretty lost. Can someone confirm that I'm on the right lines?

I use a similar question on indexed sequel to a monad as a guide, but I don't think it's really close enough.

Answer 1

We can replicate Gabriel's argument from the linked indexed Cont response. If the standard state state monad

 State ss' a = s -> (a, s') 

then we generalize it in stages. First, using Identity to reflect specific types s and s' as fibers in a space with an indexed type Identity .

 State ss' a = s -> (a, s') ~ Identity s -> (a, Identity s') 

then, generalizing the type of the value of a to the indexed type also by the index "destination", type s' .

  ~ Identity s -> (a , Identity s') ~ Identity s -> (a s', Identity s') 

and then using the existential type to remove the target index. We will restore it later.

 data a :* b = forall i . P (ai) (bi) Identity s -> (a s', Identity s') ~ Identity s -> P a Identity 

Finally, note that Identity is an indexed type of state space and a indexed type of value space, so we can write IState as

 newtype IState s -- indexed state space a -- indexed value space i -- index = IState { runIState :: si -> a :* s } -- State { runState :: s -> (a, s) } for comparison 

---

Why use a batch with existential quantile instead of universally quantified? The first push is due to the fact that the index associated with a is positive in IState , while it is negative in ICont . The second hint comes from writing returnI . If we use the universally quantified version and try to write returnI

 newtype IState' sai = IState' { runIState' :: si -> (forall i . (ai, si)) } returnI :: ai -> IState' sai returnI a = IState' (\si -> (?forget a, ?forget si)) 

we will need this forget function, which forgets all the information about the index.

However, if instead we use an entity with an entity of a quantified pair, then before the constructor of the returning pair, i.e. developer of the IState value, you need to select the index. This allows us to instantiate IFunctor and IMonad

 instance IFunctor (IState s) where -- fmapI :: (a :-> b) -> IState sa :-> IState sb 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 sa return ai = IState (\si -> P ai si) -- bindI :: (a :-> IState sb) -> (IState sa :-> IState sb) bindI fm = IState $ \s -> case runIState ms of P ax sx -> runIState (f ax) sx 

The only drawback to using this existential pair is that it ... is quite difficult to use. For example, we would really like to use a constructor with an index pointed to (:=) to fix a known index and project from an existential pair.

 one :: (a := i :* b) -> a two :: (a := i :* b) -> bi 

Unfortunately, Haskell is not smart enough to force existence even when we know what it is, so the second of these predictions has a dubious implementation

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

---

Finally, the proof is in the pudding. We can use IState to implement the standard addition of state effects that we are used to seeing.

 -- Higher order unit type data U1 a = U1 put :: si -> IState s U1 j put s = IState (\_ -> P U1 s) get :: IState ssi get = IState (\s -> P ss) 

and use them to implement some common higher order combinators, such as modification (which requires an explicit type signature, but you can figure it out from the implementation manually with some thought)

 modify :: (s :-> s) -> IState s U1 i modify f = get ?>= put . f 

However, in addition, we have other ways of representing combinators that are more explicit with respect to indexing due to a constraint through (:=) . This may be useful to convey additional indexing information.

 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 modify' f = get >>= put' . V . f modify'' :: (si -> sk) -> IState s (() := k) i modify'' f = get' >>= put' . f 

Finally, we can use all of this to implement the example. For example, we can create an indexed type over file descriptors, but this is not very 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 () 

everyone is working.