Playing around with Type families and Constraint kinds

Example.lhs

In this example we are using both *TypeFamilies* and *ConstraintKinds* to create a monadic 
interface that keeps track of valid state transitions.

This is an evolution from @pittma experiments from the #haskell channel on the Functional Programming slack

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE StandaloneDeriving #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE PolyKinds #-}
> 
> module Next where
> 
> import Data.Kind
> import GHC.Exts
> 
> type family Next (a :: k) :: k -> Constraint
> 

There's some unsoundness here, I fear, but it's soundiness with the best intentions.
A Functor is meant to be structure preserving, so it does not transition the state.
However, this Functor's structure is not properly hidden within a partially applied type.
All of of FSMFunctor's type arity is laid bare: k -> * -> *

> class FSMFunctor (f :: k -> * -> *) where
>   fsmFmap :: (a -> b) -> f s a -> f s b

Like its superclass, FSMApplicative is also structure preserving.

> class FSMFunctor f =>
>       FSMApplicative (f :: k -> * -> *) where
>   type Init f :: k
>   fsmPure :: a -> f (Init f) a
>   fsmAp :: f s (a -> b) -> f s a -> f s b

Aha! Finally a use of our eponymous type family.  Like Indexed Monads, FSMMonad
is the only one in the FSM F-A -M stack that transitions the state indices.

We are defining a constraint s2 from the custom constraint defined on the Next
type family

> class FSMApplicative m =>
>       FSMMonad (m :: k -> * -> *) where
>   (->>=) :: ((Next s) s2) => m s a -> (a -> m s2 b) -> m s2 b
> 
> infixl 3 ->>=
> 
> --------------------------------------------------------------------------------
> 
> data ResourceStatus
>   = New
>   | Open
>   | Closed
> 
> data Resource s a where
>   NewResource :: a -> Resource 'New a
>   OpenResource :: a -> Resource 'Open a
>   ClosedResource :: a -> Resource 'Closed a
> 
> deriving instance Show a => Show (Resource s a)
> 
> class NewTransitions s
> instance NewTransitions 'Open
> 
> class OpenTransitions s
> instance OpenTransitions 'Closed
> 
> type instance Next 'New = NewTransitions
> type instance Next 'Open = OpenTransitions
> 
> instance FSMFunctor Resource where
>   fsmFmap f (NewResource x) = NewResource (f x)
>   fsmFmap f (OpenResource x) = OpenResource (f x)
>   fsmFmap f (ClosedResource x) = ClosedResource (f x)
> 
> instance FSMApplicative Resource where
>   type Init Resource = 'New
>   fsmPure = NewResource
>   fsmAp (NewResource f) (NewResource x) = NewResource (f x)
>   fsmAp (OpenResource f) (OpenResource x) = OpenResource (f x)
>   fsmAp (ClosedResource f) (ClosedResource x) = ClosedResource (f x)
> 
> instance FSMMonad Resource where
>   (->>=) (NewResource x) f = f x
>   (->>=) (OpenResource x) f = f x
>   (->>=) (ClosedResource x) f = f x
> 
> run :: IO ()
> run = do
>   let d = fsmPure "types" :: Resource 'New String
>   putStrLn ("Here's our resource: " ++ show d)
>   putStrLn "Should we open it? (y/n)"
>   ans <- getLine
>   case ans of
>     "y"
>       -- Now we're going to open our door!
>      -> do
>       let d' = d ->>= \x -> ClosedResource ("dependent " ++ x ++ "! (kind of)")
>       putStrLn "Resource opened!"
>       print d'
>     "n" -> putStrLn "okay, then. Goodbye!"
>     _ -> putStrLn (ans ++ " is not a valid input")

^^^ That implementation is incorrect, given we have defined there is no valid transition between a New resource and 
an Closed resource, rightly so the compiler reports:

@
λ [1 of 1] Compiling Next             ( /home/ubuntu/tmp/next/src/Next.hs, interpreted )

/home/ubuntu/tmp/next/src/Next.hs:90:16: warning: [-Wdeferred-type-errors]
    • No instance for (NewTransitions 'Closed)
        arising from a use of ‘->>=’
    • In the expression:
        d ->>= \ x -> ClosedResource ("dependent " ++ x ++ "! (kind of)")
      In an equation for ‘d'’:
          d'
            = d ->>= \ x -> ClosedResource ("dependent " ++ x ++ "! (kind of)")
      In the expression:
        do let d' = d ->>= ...
           putStrLn "Resource opened!"
           print d'
   |
90 |       let d' = d ->>= \x -> ClosedResource ("dependent " ++ x ++ "! (kind of)")
   |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@

If we change the implementation to use @OpenResource@ instead, things work as expected...