Skip to content

Instantly share code, notes, and snippets.

@roman
Last active February 10, 2018 23:15
Show Gist options
  • Save roman/043451849d18f1f60a688f211e99bdb5 to your computer and use it in GitHub Desktop.
Save roman/043451849d18f1f60a688f211e99bdb5 to your computer and use it in GitHub Desktop.
Playing around with Type families and Constraint kinds
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...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment