{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, RebindableSyntax #-}

module Control.IxMonad.ReadOnlyWriter (HNil'(..), HCons'(..), put, AppendA(..)) where

import Control.IxMonad
import Data.HList hiding (Monad(..), append)
import Prelude hiding (Monad(..))

instance IxMonad (,) where
    type Inv (,) s t = AppendA s t

    type Unit (,) = HNil'
    type Plus (,) s t = Append s t

    return x = (HNil', x)
    (r, a) >>= k = let (s, b) = k a in (r `append` s, b)
 
put :: a -> (HCons' a HNil', ())
put x = (HCons' x HNil', ())

-- Type-level append

class AppendA s t where
    type Append s t
    append :: s -> t -> Append s t

instance AppendA HNil' t where
    type Append HNil' t = t
    append HNil' t = t

instance AppendA xs ys => AppendA (HCons' x xs) ys where
    type Append (HCons' x xs) ys = HCons' x (Append xs ys)
    append (HCons' x xs) ys = HCons' x (append xs ys)