HFold.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module HFold where

-- base
import Data.Coerce
  ( coerce )
import Data.Functor.Const
  ( Const(Const) )
import Data.Kind
  ( Type, Constraint )
import Data.Monoid
  ( Endo(Endo) )

----------------------------------------------------------------------------

type FoldC :: ( Type -> Constraint ) -> Type -> Type
type FoldC c s = forall f. Applicative f => ( forall a. c a => a -> f a ) -> s -> f s

type HasFoldC :: ( Type -> Constraint ) -> Type -> Constraint
class HasFoldC c s where
  foldC :: FoldC c s

foldrC :: forall c b s
       .  HasFoldC c s
       => ( forall a. c a => a -> b -> b ) -> s -> b -> b
foldrC f = coerce foldF
    where
      foldF :: s -> Const (Endo b) s
      foldF = foldC @c ( coerce . f )



infixr 3 `HCons`
type HList :: [Type] -> Type
data HList as where
  HNil  :: HList '[]
  HCons :: a -> HList as -> HList (a ': as)

instance HasFoldC c (HList '[]) where
  foldC _ = pure
instance ( c a, HasFoldC c (HList as) ) => HasFoldC c (HList (a ': as)) where
  foldC f ( HCons a as ) = HCons <$> f a <*> foldC @c f as



hfoldr :: forall (c :: Type -> Constraint) (b :: Type) (as :: [Type])
       .  HasFoldC c (HList as)
       => (forall a. c a => a -> b -> b) -> HList (b ': as) -> b
hfoldr f ( HCons b as ) = foldrC @c f as b

hMax :: forall (a :: Type) (as :: [Type])
     . ( Ord a, HasFoldC ((~) a) (HList as) )
     => HList (a ': as) -> a
hMax = hfoldr @((~) a) max


test :: Int
test = hMax testHList
  where
    testHList :: HList '[ Int, Int, Int ]
    testHList = 2 `HCons` 3 `HCons` 1 `HCons` HNil

-- > test
-- 3