------------------------------------------------------------------------
-- |
-- Module           : Data.Parameterized.All
-- Copyright        : (c) Galois, Inc 2019
-- Maintainer       : Langston Barrett <langston@galois.com>
-- 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):
--
-- @
--   {-# 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/
------------------------------------------------------------------------

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

module Data.Parameterized.All
  ( All(..)
  , allConst
  ) where

import Data.Functor.Const (Const(..))
import Data.Kind

import Data.Parameterized.Classes
import Data.Parameterized.TraversableF

newtype All (f :: k -> Type) = All { forall k (f :: k -> *). All f -> forall (x :: k). f x
getAll :: forall x. f x }

instance FunctorF All where
  fmapF :: forall (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x) -> All f -> All g
fmapF forall (x :: k). f x -> g x
f (All forall (x :: k). f x
a) = forall k (f :: k -> *). (forall (x :: k). f x) -> All f
All (forall (x :: k). f x -> g x
f forall (x :: k). f x
a)

instance FoldableF All where
  foldMapF :: forall m (e :: k -> *).
Monoid m =>
(forall (s :: k). e s -> m) -> All e -> m
foldMapF forall (s :: k). e s -> m
toMonoid (All forall (x :: k). e x
x) = forall (s :: k). e s -> m
toMonoid forall (x :: k). e x
x

instance ShowF f => Show (All f) where
  show :: All f -> String
show (All forall (x :: k). f x
fa) = forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
showF forall (x :: k). f x
fa

instance EqF f => Eq (All f) where
  (All forall (x :: k). f x
x) == :: All f -> All f -> Bool
== (All forall (x :: k). f x
y) = forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
eqF forall (x :: k). f x
x forall (x :: k). f x
y

allConst :: a -> All (Const a)
allConst :: forall {k} a. a -> All (Const a)
allConst a
a = forall k (f :: k -> *). (forall (x :: k). f x) -> All f
All (forall {k} a (b :: k). a -> Const a b
Const a
a)