Folding... heterogeneously.

HFolds.hs

{-# LANGUAGE AllowAmbiguousTypes     #-}
{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE QuantifiedConstraints   #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE ScopedTypeVariables     #-}
{-# LANGUAGE TypeApplications        #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module HFolds where

import Data.Kind (Type)

data HList (xs :: [Type]) where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)

class HFoldr c acc xs r where
  hfoldr
    :: (forall x y z. c x y z => x -> y -> z)
    -> acc -> HList xs -> r

instance acc ~ r => HFoldr c acc '[] r where
  hfoldr _ acc _ = acc

instance (c x acc' r, HFoldr c acc xs acc')
    => HFoldr c acc (x ': xs) r where
  hfoldr f acc (HCons x xs)
    = f x (hfoldr @c f acc xs :: acc')

-------------------------------------------------------------------------------
-- MONOIDAL FOLDING.

class    (Monoid m, c x, y ~ m, z ~ m) => FoldWith c m x y z
instance (Monoid m, c x, y ~ m, z ~ m) => FoldWith c m x y z

fold
  :: forall c xs m
   . Monoid m
  => HFoldr (FoldWith c m) m xs m
  => (forall x. c x => x -> m)
  -> HList xs
  -> m

fold f
  = hfoldr @(FoldWith c m) (\x acc -> f x <> acc) (mempty @m)

foldMap
  :: forall a m xs
   . Monoid m
  => HFoldr (FoldWith ((~) a) m) m xs m
  => (a -> m)
  -> HList xs
  -> m

foldMap f = fold @((~) a) f

-------------------------------------------------------------------------------
-- LIST APPENDING.

class (forall xs. y ~ HList xs => z ~ HList (x ': xs))
    => Append x y z | x y -> z, z -> x y where
  append' :: x -> y -> z

instance Append x (HList xs) (HList (x ': xs)) where
  append' = HCons

append
  :: forall xs ys rs
   . HFoldr Append ys xs rs
  => HList xs
  -> ys
  -> rs

append
  = flip (hfoldr @Append append')

---

eg0
  :: HList '[Int, String]
  -> HList '[Bool, ()]
  -> HList '[Int, String, Bool, ()]

eg0
  = append