I’d like to chain state monads with different state types together, like:
stage1 :: a -> State t1 b
stage2 :: b -> State t2 c
chain :: (t1, t2) -> a -> ((t1, t2), c)
chain (s1, s2) = \x ->
let (y, s1') = runState (stage1 x) s1
(z, s2') = runState (stage2 y) s2
in ((s1', s2'), z)
And I’m thinking of making a more generic version, turning the above example into (pseudocode):
chain (s1 :+: s2 :+: HNil) (stage1 :+: stage2 :+: HNil) = \x ->
let (y, s1') = runState (stage1 x) s1
(z, s2') = runState (stage2 y) s2
in (s1' :+: s2' :+: HNil, z)
Finally I end up with these code, but it fails to compile (GHC 9.4.8):
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Main where
import Data.Kind (Type)
import Control.Monad.State
type family KFrom (f :: Type) :: Type where
KFrom (a -> State t b) = a
type family KTo (f :: Type) :: Type where
KTo (a -> State t b) = b
type family From (ks :: [Type]) :: Type where
From (k ': ks) = KFrom k
type family To (ks :: [Type]) :: Type where
To '[k] = KTo k
To (k ': ks) = To ks
-- Errors occur in the definition of Chain
class Chain (ts :: [Type]) (ks :: [Type]) where
chain :: HList ts -> HList ks -> From ks -> (HList ts, To ks)
instance Chain '[t] '[a -> State t b] where
chain (s :+: HNil) (f :+: HNil) = \x ->
let (y, s') = runState (f x) s
in (s' :+: HNil, y)
instance Chain ts ks => Chain (t ': ts) ((a -> State t b) ': ks) where
chain (s :+: ss) (f :+: fs) = \x ->
let (y, s') = runState (f x) s
(ss', z) = chain ss fs y -- Compile Error One
in (s' :+: ss', z) -- Compile Error Two
-- Heterogeneous List Definitions
infixr 4 :+:
data HList :: [Type] -> Type where
HNil :: HList '[]
(:+:) :: t -> HList ts -> HList (t ': ts)
instance Show (HList '[]) where
show HNil = "HNil"
instance (Show x, Show (HList xs)) => Show (HList (x ': xs)) where
show (x :+: xs) = show x ++ " :+: " ++ show xs
Compile Error One
The first error, y :: b
mismatches with x :: From ((a -> State t b) : ks)
, which is due to the lack of evidence that these Kleisli arrows overlaps. But as I changed the signature
instance Chain ts ks => Chain (t ': ts) ((a -> State t b) ': ks) where
-- into
instance Chain ts ks => Chain (t ': ts) ((a -> State t (From ks)) ': ks) where
GHC complains: Illegal type synonym family application ‘From ks’ in instance
.
Compile Error Two
The second error, z :: To ks
mismatches with the result type To ((a -> State t b) : ks)
, which is strange because according to the definition of To
,
type family To (ks :: [Type]) :: Type where
To '[k] = KTo k
To (k ': ks) = To ks
it should be clear that the two types are equal.
I’d appreciate it if you could give me some suggestions on the problem.