Copyright | (c) Galois Inc 2019 |
---|---|
Maintainer | Langston Barrett <langston@galois.com> |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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):
{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} 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 -> Type) Source #
Instances
FoldableF (All :: (k -> Type) -> Type) Source # | |
Defined in Data.Parameterized.All 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 # | |
ShowF f => Show (All f) Source # | |
EqF f => Eq (All f) Source # | |