Data.Parameterized.All

Description : Universal quantification, in a datatype

This module provides All, a GADT that encodes universal quantification/parametricity over a type variable.

The following is an example of a situation in which it might be necessary to use All (though it is a bit contrived):

  {--}
  {--}

  data F (x :: Bool) where
    FTrue :: F 'True
    FFalse :: F 'False
    FIndeterminate :: F b

  data Value =
    VAllF (All F)

  class Valuable a where
    valuation :: a -> Value

  instance Valuable (All F) where
    valuation = VAllF

  val1 :: Value
  val1 = valuation (All FIndeterminate)

For a less contrived but more complex example, see this blog post: http://comonad.com/reader/2008/rotten-bananas/

Documentation

newtype All (f :: k -> *)

Constructors

All

Fields

• getAll :: forall x. f x

Instances

FoldableF (All :: (k -> Type) -> Type)

Defined in Data.Parameterized.All

Methods

foldMapF :: Monoid m => (forall (s :: k0). e s -> m) -> All e -> m

foldrF :: (forall (s :: k0). e s -> b -> b) -> b -> All e -> b

foldlF :: (forall (s :: k0). b -> e s -> b) -> b -> All e -> b

foldrF' :: (forall (s :: k0). e s -> b -> b) -> b -> All e -> b

foldlF' :: (forall (s :: k0). b -> e s -> b) -> b -> All e -> b

toListF :: (forall (tp :: k0). f tp -> a) -> All f -> [a]

FunctorF (All :: (k -> Type) -> Type)

Defined in Data.Parameterized.All

Methods

fmapF :: (forall (x :: k0). f x -> g x) -> All f -> All g

EqF f => Eq (All f)

Defined in Data.Parameterized.All

Methods

(==) :: All f -> All f -> Bool

(/=) :: All f -> All f -> Bool

ShowF f => Show (All f)

Defined in Data.Parameterized.All

Methods

showsPrec :: Int -> All f -> ShowS

show :: All f -> String

showList :: [All f] -> ShowS

allConst :: a -> All (Const a)