------------------------------------------------------------------------
-- |
-- Module           : Data.Parameterized.Some
-- Copyright        : (c) Galois, Inc 2014-2019
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Description : a GADT that hides a type parameter
--
-- This module provides 'Some', a GADT that hides a type parameter.
------------------------------------------------------------------------
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Data.Parameterized.Some
  ( Some(..)
  , viewSome
  , mapSome
  , traverseSome
  , traverseSome_
  , someLens
  ) where

import Control.Lens (Lens', lens, (&), (^.), (.~))
import Data.Hashable
import Data.Kind
import Data.Parameterized.Classes
import Data.Parameterized.TraversableF


data Some (f:: k -> Type) = forall x . Some (f x)

instance TestEquality f => Eq (Some f) where
  Some f x
x == :: Some f -> Some f -> Bool
== Some f x
y = forall a. Maybe a -> Bool
isJust (forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f x
x f x
y)

instance OrdF f => Ord (Some f) where
  compare :: Some f -> Some f -> Ordering
compare (Some f x
x) (Some f x
y) = forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF f x
x f x
y)

instance (HashableF f, TestEquality f) => Hashable (Some f) where
  hashWithSalt :: Int -> Some f -> Int
hashWithSalt Int
s (Some f x
x) = forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
hashWithSaltF Int
s f x
x
  hash :: Some f -> Int
hash (Some f x
x) = forall k (f :: k -> *) (tp :: k). HashableF f => f tp -> Int
hashF f x
x

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

-- | Project out of Some.
viewSome :: (forall tp . f tp -> r) -> Some f -> r
viewSome :: forall {k} (f :: k -> *) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall (tp :: k). f tp -> r
f (Some f x
x) = forall (tp :: k). f tp -> r
f f x
x

-- | Apply function to inner value.
mapSome :: (forall tp . f tp -> g tp) -> Some f -> Some g
mapSome :: forall {k} (f :: k -> *) (g :: k -> *).
(forall (tp :: k). f tp -> g tp) -> Some f -> Some g
mapSome forall (tp :: k). f tp -> g tp
f (Some f x
x) = forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$! forall (tp :: k). f tp -> g tp
f f x
x

{-# INLINE traverseSome #-}
-- | Modify the inner value.
traverseSome :: Functor m
             => (forall tp . f tp -> m (g tp))
             -> Some f
             -> m (Some g)
traverseSome :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *).
Functor m =>
(forall (tp :: k). f tp -> m (g tp)) -> Some f -> m (Some g)
traverseSome forall (tp :: k). f tp -> m (g tp)
f (Some f x
x) = forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall (tp :: k). f tp -> m (g tp)
f f x
x

{-# INLINE traverseSome_ #-}
-- | Modify the inner value.
traverseSome_ :: Functor m => (forall tp . f tp -> m ()) -> Some f -> m ()
traverseSome_ :: forall {k} (m :: * -> *) (f :: k -> *).
Functor m =>
(forall (tp :: k). f tp -> m ()) -> Some f -> m ()
traverseSome_ forall (tp :: k). f tp -> m ()
f (Some f x
x) = (\()
_ -> ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall (tp :: k). f tp -> m ()
f f x
x

instance FunctorF     Some where fmapF :: forall (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x) -> Some f -> Some g
fmapF     = forall {k} (f :: k -> *) (g :: k -> *).
(forall (tp :: k). f tp -> g tp) -> Some f -> Some g
mapSome
instance FoldableF    Some where foldMapF :: forall m (e :: k -> *).
Monoid m =>
(forall (s :: k). e s -> m) -> Some e -> m
foldMapF  = forall {k} (t :: (k -> *) -> *) m (e :: k -> *).
(TraversableF t, Monoid m) =>
(forall (s :: k). e s -> m) -> t e -> m
foldMapFDefault
instance TraversableF Some where traverseF :: forall (m :: * -> *) (e :: k -> *) (f :: k -> *).
Applicative m =>
(forall (s :: k). e s -> m (f s)) -> Some e -> m (Some f)
traverseF = forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *).
Functor m =>
(forall (tp :: k). f tp -> m (g tp)) -> Some f -> m (Some g)
traverseSome

-- | A lens that is polymorphic in the index may be used on a value with an
-- existentially-quantified index.
someLens :: (forall tp. Lens' (f tp) a) -> Lens' (Some f) a
someLens :: forall {k} (f :: k -> *) a.
(forall (tp :: k). Lens' (f tp) a) -> Lens' (Some f) a
someLens forall (tp :: k). Lens' (f tp) a
l = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (\(Some f x
x) -> f x
x forall s a. s -> Getting a s a -> a
^. forall (tp :: k). Lens' (f tp) a
l) (\(Some f x
x) a
v -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some (f x
x forall a b. a -> (a -> b) -> b
& forall (tp :: k). Lens' (f tp) a
l forall s t a b. ASetter s t a b -> b -> s -> t
.~ a
v))