HasochistIntersperse.hs

{-# Language PolyKinds, GADTs, ScopedTypeVariables, TypeApplications #-}

module HasochistIntersperse (intersperse) where

import Data.Singletons

data Between a v = Empty | Has v deriving (Eq, Ord, Show)

instance forall k (a :: k) v.
         (SingI a, SingKind k, v ~ Demote k, Semigroup v) =>
         Semigroup (Between a v) where
    Empty <> x = x
    x <> Empty = x
    (Has x) <> (Has y) = Has (x <> demote @a <> y)

instance forall k (a :: k) v.
         (SingI a, SingKind k, v ~ Demote k, Semigroup v) =>
         Monoid (Between a v) where
    mempty = Empty

unBetween :: Monoid v => Between a v -> v
unBetween Empty = mempty
unBetween (Has x) = x

intersperse :: forall f v k.
               (SingKind k, v ~ Demote k, Foldable f, Monoid v) =>
               v -> f v -> v
intersperse x xs = withSomeSing x $
    \(sx :: Sing a) -> withSingI sx (unBetween $ foldMap (Has @a) xs)