Fold.hs

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE KindSignatures    #-}

module Fold where

data Nat = Z | S Nat

data Vect (n :: Nat) a where
  Nil  :: Vect 'Z a
  Cons :: a -> Vect n a -> Vect ('S n) a

instance Foldable (Vect 'Z) where
  foldr _ b _ = b

instance Foldable (Vect n) => Foldable (Vect ('S n)) where
  foldr f b (Cons x xs) = f x (foldr f b xs)

test :: Int
test = foldr (+) 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))

-- $ ghc -O1 Fold.hs -ddump-simpl

-- test :: Int
-- [GblId,
--  Caf=NoCafRefs,
--  Str=m,
--  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
--          WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
-- test = GHC.Types.I# 10#