parameterized-utils-2.1.1: Classes and data structures for working with data-kind indexed types

Copyright(c) Galois Inc 2019
MaintainerLangston Barrett <langston@galois.com>
Safe HaskellSafe
LanguageHaskell2010

Data.Parameterized.All

Description

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 -> *) Source #

Constructors

All 

Fields

Instances
FoldableF (All :: (k -> Type) -> Type) Source # 
Instance details

Defined in Data.Parameterized.All

Methods

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

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

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

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

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

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

FunctorF (All :: (k -> Type) -> Type) Source # 
Instance details

Defined in Data.Parameterized.All

Methods

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

EqF f => Eq (All f) Source # 
Instance details

Defined in Data.Parameterized.All

Methods

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

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

ShowF f => Show (All f) Source # 
Instance details

Defined in Data.Parameterized.All

Methods

showsPrec :: Int -> All f -> ShowS #

show :: All f -> String #

showList :: [All f] -> ShowS #

allConst :: a -> All (Const a) Source #