{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Universe.Instances.Extended (
-- | Instances for 'Universe' and 'Finite' for function-like functors and the empty type.
Universe(..), Finite(..)
) where
import Control.Comonad.Trans.Traced (TracedT (..))
import Data.Functor.Rep (Representable (..), Co(..))
import Data.Universe.Class (Universe (..), Finite (..))
import Data.Universe.Helpers (retag, Tagged, Natural)
-- | We could do this:
--
-- instance Universe (f a) => Universe (Co f a) where universe = map Rep universe
--
-- However, since you probably only apply Rep to functors when you want to
-- think of them as being representable, I think it makes sense to use an
-- instance based on the representable-ness rather than the inherent
-- universe-ness.
--
-- Please complain if you disagree!
--
instance (Representable f, Finite (Rep f), Ord (Rep f), Universe a)
=> Universe (Co f a)
where universe = map tabulate universe
instance (Representable f, Finite s, Ord s, Finite (Rep f), Ord (Rep f), Universe a)
=> Universe (TracedT s f a)
where universe = map tabulate universe
instance (Representable f, Finite (Rep f), Ord (Rep f), Finite a)
=> Finite (Co f a)
where universeF = map tabulate universeF; cardinality = retag (cardinality :: Tagged (Rep (Co f) -> a) Natural)
instance (Representable f, Finite s, Ord s, Finite (Rep f), Ord (Rep f), Finite a)
=> Finite (TracedT s f a)
where universeF = map tabulate universeF; cardinality = retag (cardinality :: Tagged (Rep (TracedT s f)) Natural)