Restrict index to only valid transitions

[JordanMartinez]

I doubt this is desirable, but thought it might lead to an interesting discussion.

While using this library for hyper, I discovered that one could subjugate the index change by defining a type signature that resets the index to a prior state. The code will compile since there is nothing restricting what this state change can be. As a result, the guarantees of this library are completely broken.

import Control.Monad.Index.Qualified as Ix

streetLight :: m Green Red a
streetLight = Ix.do
  greenLight
  yellowLight
  redLight
  noCarCrash

-- user function
lightIsGreenAgain :: m Yellow Green Unit
lightIsGreenAgain = -- implementation

streetLight :: m Green Green a
streetLight = Ix.do
  greenLight
  yellowLight
  lightIsGreenAgain
  carCrash

To fix this, I include a ValidTransition type class. The empty dictionary will be erased before runtime due to the recent work in the compiler. Thus, a library could define instances for their domain type that define valid index transitions in their types. If used with kinds, this would make the index more understandable. However, due to the open-natured of kinds, I'm not sure whether this truly fixes the problem. The other tradeoff is higher type-safety at the cost of increased verbosity.

[JordanMartinez]

Yeah, I don't think this is a good idea after playing around with it more...

[garyb]

I think the problem isn't so much with the transition between indices, but more that you shouldn't be able to treat them like phantom type parameters and make operations that just arbitrarily rewrite the index to whatever state - basically, the indexed type should not have its constructor exported, that way you can only do things using the operations that are provided with it.

[JordanMartinez]

the indexed type should not have its constructor exported, that way you can only do things using the operations that are provided with it.

Good point. However, I'm not sure how that will work if I'm storing two slots in the same index. For example, hyper uses indices to track how much of the HTTP response has been written. I then tried augmenting this index to also track whether the HTTP request's body has been read or not. Thus, my index went from responseState to Conn requestState responseState.

newtype Hyper m fromReq fromRes toReq toRes a =
  Hyper (Indexed (ReaderT HttpConn m) (Conn fromReq fromRes) (Conn toReq toRes) a)

The resulting monad (requires 6 types) no longer fits the structure of an indexed monad (requires 4 types). Thus, I'm trying to determine how that should be dealt with... ValidTransition was one approach but it got very complicated and confusing fast...

[JordanMartinez]

Hm... I guess the solution is to not specify Conn in indexed but rather leave that defined in Hyper later...

-- definition
newtype Hyper m from to a =
  Hyper (Indexed (ReaderT HttpConn m) from to a)

-- usage
foo :: Hyper (Conn req StatusLineOpen) (Conn req HeadersOpen) a
foo = Ix.do
  -- ...