{-|
Description : Classes for working with type of kind @k -> *@
Copyright   : (c) Galois, Inc 2014-2019
Maintainer  : Joe Hendrix <jhendrix@galois.com>

This module declares classes for working with types with the kind
@k -> *@ for any kind @k@.  These are generalizations of the
"Data.Functor.Classes" types as they work with any kind @k@, and are
not restricted to '*'.
-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Parameterized.Classes
  ( -- * Equality exports
    Equality.TestEquality(..)
  , (Equality.:~:)(..)
  , EqF(..)
  , PolyEq(..)
    -- * Ordering generalization
  , OrdF(..)
  , lexCompareF
  , OrderingF(..)
  , joinOrderingF
  , orderingF_refl
  , toOrdering
  , fromOrdering
  , ordFCompose
    -- * Typeclass generalizations
  , ShowF(..)
  , showsF
  , HashableF(..)
  , CoercibleF(..)
    -- * Type function application constructor
  , TypeAp(..)
    -- * Optics generalizations
  , IndexF
  , IxValueF
  , IxedF(..)
  , IxedF'(..)
  , AtF(..)
    -- * KnownRepr
  , KnownRepr(..)
    -- * Re-exports
  , Data.Hashable.Hashable(..)
  , Data.Maybe.isJust
  ) where

import Data.Functor.Const
import Data.Functor.Compose (Compose(..))
import Data.Kind
import Data.Hashable
import Data.Maybe (isJust)
import Data.Proxy
import Data.Type.Equality as Equality

import Data.Parameterized.Compose ()

-- We define these type alias here to avoid importing Control.Lens
-- modules, as this apparently causes problems with the safe Hasekll
-- checking.
type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s

------------------------------------------------------------------------
-- CoercibleF

-- | An instance of 'CoercibleF' gives a way to coerce between
--   all the types of a family.  We generally use this to witness
--   the fact that the type parameter to @rtp@ is a phantom type
--   by giving an implementation in terms of Data.Coerce.coerce.
class CoercibleF (rtp :: k -> Type) where
  coerceF :: rtp a -> rtp b

instance CoercibleF (Const x) where
  coerceF :: Const x a -> Const x b
coerceF (Const x
x) = x -> Const x b
forall k a (b :: k). a -> Const a b
Const x
x

------------------------------------------------------------------------
-- EqF

-- | @EqF@ provides a method @eqF@ for testing whether two parameterized
-- types are equal.
--
-- Unlike 'TestEquality', this only works when the type arguments are
-- the same, and does not provide a proof that the types have the same
-- type when they are equal. Thus this can be implemented over
-- parameterized types that are unable to provide evidence that their
-- type arguments are equal.
class EqF (f :: k -> Type) where
  eqF :: f a -> f a -> Bool

instance Eq a => EqF (Const a) where
  eqF :: Const a a -> Const a a -> Bool
eqF (Const a
x) (Const a
y) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y

------------------------------------------------------------------------
-- PolyEq

-- | A polymorphic equality operator that generalizes 'TestEquality'.
class PolyEq u v where
  polyEqF :: u -> v -> Maybe (u :~: v)

  polyEq :: u -> v -> Bool
  polyEq u
x v
y = Maybe (u :~: v) -> Bool
forall a. Maybe a -> Bool
isJust (u -> v -> Maybe (u :~: v)
forall u v. PolyEq u v => u -> v -> Maybe (u :~: v)
polyEqF u
x v
y)

------------------------------------------------------------------------
-- Ordering

-- | Ordering over two distinct types with a proof they are equal.
data OrderingF x y where
  LTF :: OrderingF x y
  EQF :: OrderingF x x
  GTF :: OrderingF x y

orderingF_refl :: OrderingF x y -> Maybe (x :~: y)
orderingF_refl :: OrderingF x y -> Maybe (x :~: y)
orderingF_refl OrderingF x y
o =
  case OrderingF x y
o of
    OrderingF x y
LTF -> Maybe (x :~: y)
forall a. Maybe a
Nothing
    OrderingF x y
EQF -> (x :~: x) -> Maybe (x :~: x)
forall a. a -> Maybe a
Just x :~: x
forall k (a :: k). a :~: a
Refl
    OrderingF x y
GTF -> Maybe (x :~: y)
forall a. Maybe a
Nothing

-- | Convert 'OrderingF' to standard ordering.
toOrdering :: OrderingF x y -> Ordering
toOrdering :: OrderingF x y -> Ordering
toOrdering OrderingF x y
LTF = Ordering
LT
toOrdering OrderingF x y
EQF = Ordering
EQ
toOrdering OrderingF x y
GTF = Ordering
GT

-- | Convert standard ordering to 'OrderingF'.
fromOrdering :: Ordering -> OrderingF x x
fromOrdering :: Ordering -> OrderingF x x
fromOrdering Ordering
LT = OrderingF x x
forall k (x :: k) (y :: k). OrderingF x y
LTF
fromOrdering Ordering
EQ = OrderingF x x
forall k (x :: k). OrderingF x x
EQF
fromOrdering Ordering
GT = OrderingF x x
forall k (x :: k) (y :: k). OrderingF x y
GTF

-- | @joinOrderingF x y@ first compares on @x@, returning an
-- equivalent value if it is not `EQF`.  If it is `EQF`, it returns @y@.
joinOrderingF :: forall j k (a :: j) (b :: j) (c :: k) (d :: k)
              .  OrderingF a b
              -> (a ~ b => OrderingF c d)
              -> OrderingF c d
joinOrderingF :: OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF OrderingF a b
EQF (a ~ b) => OrderingF c d
y = OrderingF c d
(a ~ b) => OrderingF c d
y
joinOrderingF OrderingF a b
LTF (a ~ b) => OrderingF c d
_ = OrderingF c d
forall k (x :: k) (y :: k). OrderingF x y
LTF
joinOrderingF OrderingF a b
GTF (a ~ b) => OrderingF c d
_ = OrderingF c d
forall k (x :: k) (y :: k). OrderingF x y
GTF

------------------------------------------------------------------------
-- OrdF

-- | The `OrdF` class is a total ordering over parameterized types so
-- that types with different parameters can be compared.
--
-- Instances of `OrdF` are expected to satisfy the following laws:
--
-- [__Transitivity__]: if @leqF x y && leqF y z@ = 'True', then @leqF x = z@ = @True@
-- [__Reflexivity__]: @leqF x x@ = @True@
-- [__Antisymmetry__]: if @leqF x y && leqF y x@ = 'True', then @testEquality x y@ = @Just Refl@
--
-- Note that the following operator interactions are expected to hold:
--
-- * @geqF x y@ iff @leqF y x@
-- * @ltF  x y@ iff @leqF x y && testEquality x y = Nothing@
-- * @gtF  x y@ iff @ltF y x@
-- * @ltF  x y@ iff @compareF x y == LTF@
-- * @gtF  x y@ iff @compareF x y == GTF@
-- * @isJust (testEquality x y)@ iff @compareF x y == EQF@
--
-- Furthermore, when @x@ and @y@ both have type @(k tp)@, we expect:
--
-- * @compareF x y == EQF@ equals @compare x y@ when @Ord (k tp)@ has an instance.
-- * @isJust (testEquality x y)@ equals @x == y@ when @Eq (k tp)@ has an instance.
--
-- Minimal complete definition: either 'compareF' or 'leqF'.
-- Using 'compareF' can be more efficient for complex types.
class TestEquality ktp => OrdF (ktp :: k -> Type) where
  {-# MINIMAL compareF | leqF #-}

  compareF :: ktp x -> ktp y -> OrderingF x y
  compareF ktp x
x ktp y
y =
    case ktp x -> ktp y -> Maybe (x :~: y)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality ktp x
x ktp y
y of
      Just x :~: y
Refl -> OrderingF x y
forall k (x :: k). OrderingF x x
EQF
      Maybe (x :~: y)
Nothing | ktp x -> ktp y -> Bool
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> Bool
leqF ktp x
x ktp y
y -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
              | Bool
otherwise -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

  leqF :: ktp x -> ktp y -> Bool
  leqF ktp x
x ktp y
y =
    case ktp x -> ktp y -> OrderingF x y
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF ktp x
x ktp y
y of
      OrderingF x y
LTF -> Bool
True
      OrderingF x y
EQF -> Bool
True
      OrderingF x y
GTF -> Bool
False

  ltF :: ktp x -> ktp y -> Bool
  ltF ktp x
x ktp y
y =
    case ktp x -> ktp y -> OrderingF x y
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF ktp x
x ktp y
y of
      OrderingF x y
LTF -> Bool
True
      OrderingF x y
EQF -> Bool
False
      OrderingF x y
GTF -> Bool
False

  geqF :: ktp x -> ktp y -> Bool
  geqF ktp x
x ktp y
y =
    case ktp x -> ktp y -> OrderingF x y
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF ktp x
x ktp y
y of
      OrderingF x y
LTF -> Bool
False
      OrderingF x y
EQF -> Bool
True
      OrderingF x y
GTF -> Bool
True

  gtF :: ktp x -> ktp y -> Bool
  gtF ktp x
x ktp y
y =
    case ktp x -> ktp y -> OrderingF x y
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF ktp x
x ktp y
y of
      OrderingF x y
LTF -> Bool
False
      OrderingF x y
EQF -> Bool
False
      OrderingF x y
GTF -> Bool
True

-- | Compare two values, and if they are equal compare the next values,
-- otherwise return LTF or GTF
lexCompareF :: forall j k (f :: j -> Type) (a :: j) (b :: j) (c :: k) (d :: k)
             .  OrdF f
            => f a
            -> f b
            -> (a ~ b => OrderingF c d)
            -> OrderingF c d
lexCompareF :: f a -> f b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
lexCompareF f a
x f b
y = OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (f a -> f b -> OrderingF a b
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF f a
x f b
y)

-- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated
-- for the \"inner\" functor. The type-level evidence of equality is deduced
-- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.
ordFCompose :: forall k l (f :: k -> Type) (g :: l -> k) x y.
                (forall w z. f w -> f z -> OrderingF w z)
            -> Compose f g x
            -> Compose f g y
            -> OrderingF x y
ordFCompose :: (forall (w :: k) (z :: k). f w -> f z -> OrderingF w z)
-> Compose f g x -> Compose f g y -> OrderingF x y
ordFCompose forall (w :: k) (z :: k). f w -> f z -> OrderingF w z
ordF_ (Compose f (g x)
x) (Compose f (g y)
y) =
  case f (g x) -> f (g y) -> OrderingF (g x) (g y)
forall (w :: k) (z :: k). f w -> f z -> OrderingF w z
ordF_ f (g x)
x f (g y)
y of
    OrderingF (g x) (g y)
LTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
    OrderingF (g x) (g y)
GTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF
    OrderingF (g x) (g y)
EQF -> OrderingF x y
forall k (x :: k). OrderingF x x
EQF

instance OrdF f => OrdF (Compose f g) where
  compareF :: Compose f g x -> Compose f g y -> OrderingF x y
compareF Compose f g x
x Compose f g y
y = (forall (w :: k) (z :: k). f w -> f z -> OrderingF w z)
-> Compose f g x -> Compose f g y -> OrderingF x y
forall k l (f :: k -> *) (g :: l -> k) (x :: l) (y :: l).
(forall (w :: k) (z :: k). f w -> f z -> OrderingF w z)
-> Compose f g x -> Compose f g y -> OrderingF x y
ordFCompose forall (w :: k) (z :: k). f w -> f z -> OrderingF w z
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF Compose f g x
x Compose f g y
y

------------------------------------------------------------------------
-- ShowF

-- | A parameterized type that can be shown on all instances.
--
-- To implement @'ShowF' g@, one should implement an instance @'Show'
-- (g tp)@ for all argument types @tp@, then write an empty instance
-- @instance 'ShowF' g@.
class ShowF (f :: k -> Type) where
  -- | Provides a show instance for each type.
  withShow :: p f -> q tp -> (Show (f tp) => a) -> a

  default withShow :: Show (f tp) => p f -> q tp -> (Show (f tp) => a) -> a
  withShow p f
_ q tp
_ Show (f tp) => a
x = a
Show (f tp) => a
x

  showF :: forall tp . f tp -> String
  showF f tp
x = Proxy f -> Proxy tp -> (Show (f tp) => String) -> String
forall k (f :: k -> *) (p :: (k -> *) -> *) (q :: k -> *) (tp :: k)
       a.
ShowF f =>
p f -> q tp -> (Show (f tp) => a) -> a
withShow (Proxy f
forall k (t :: k). Proxy t
Proxy :: Proxy f) (Proxy tp
forall k (t :: k). Proxy t
Proxy :: Proxy tp) (f tp -> String
forall a. Show a => a -> String
show f tp
x)

  -- | Like 'showsPrec', the precedence argument is /one more/ than the
  -- precedence of the enclosing context.
  showsPrecF :: forall tp. Int -> f tp -> String -> String
  showsPrecF Int
p f tp
x = Proxy f
-> Proxy tp
-> (Show (f tp) => String -> String)
-> String
-> String
forall k (f :: k -> *) (p :: (k -> *) -> *) (q :: k -> *) (tp :: k)
       a.
ShowF f =>
p f -> q tp -> (Show (f tp) => a) -> a
withShow (Proxy f
forall k (t :: k). Proxy t
Proxy :: Proxy f) (Proxy tp
forall k (t :: k). Proxy t
Proxy :: Proxy tp) (Int -> f tp -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
p f tp
x)

showsF :: ShowF f => f tp -> String -> String
showsF :: f tp -> String -> String
showsF f tp
x = Int -> f tp -> String -> String
forall k (f :: k -> *) (tp :: k).
ShowF f =>
Int -> f tp -> String -> String
showsPrecF Int
0 f tp
x

instance Show x => ShowF (Const x)

------------------------------------------------------------------------
-- IxedF

type family IndexF       (m :: Type) :: k -> Type
type family IxValueF     (m :: Type) :: k -> Type

-- | Parameterized generalization of the lens @Ixed@ class.
class IxedF k m where
  -- | Given an index into a container, build a traversal that visits
  --   the given element in the container, if it exists.
  ixF :: forall (x :: k). IndexF m x -> Traversal' m (IxValueF m x)

-- | Parameterized generalization of the lens @Ixed@ class,
--   but with the guarantee that indexes exist in the container.
class IxedF k m => IxedF' k m where
  -- | Given an index into a container, build a lens that
  --   points into the given element in the container.
  ixF' :: forall (x :: k). IndexF m x -> Lens' m (IxValueF m x)

------------------------------------------------------------------------
-- AtF

-- | Parameterized generalization of the lens @At@ class.
class IxedF k m => AtF k m where
  -- | Given an index into a container, build a lens that points into
  --   the given position in the container, whether or not it currently
  --   exists.  Setting values of @atF@ to a @Just@ value will insert
  --   the value if it does not already exist.
  atF :: forall (x :: k). IndexF m x -> Lens' m (Maybe (IxValueF m x))

------------------------------------------------------------------------
-- HashableF

-- | A default salt used in the implementation of 'hash'.
defaultSalt :: Int
#if WORD_SIZE_IN_BITS == 64
defaultSalt = 0xdc36d1615b7400a4
#else
defaultSalt :: Int
defaultSalt = Int
0x087fc72c
#endif
{-# INLINE defaultSalt #-}

-- | A parameterized type that is hashable on all instances.
class HashableF (f :: k -> Type) where
  hashWithSaltF :: Int -> f tp -> Int

  -- | Hash with default salt.
  hashF :: f tp -> Int
  hashF = Int -> f tp -> Int
forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
hashWithSaltF Int
defaultSalt

instance Hashable a => HashableF (Const a) where
  hashWithSaltF :: Int -> Const a tp -> Int
hashWithSaltF Int
s (Const a
x) = Int -> a -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s a
x

------------------------------------------------------------------------
-- TypeAp

-- | Captures the value obtained from applying a type to a function so
-- that we can use parameterized class instance to provide unparameterized
-- instances for specific types.
--
-- This is the same as `Ap` from @Control.Applicative@, but we introduce
-- our own new type to avoid orphan instances.
newtype TypeAp (f :: k -> Type) (tp :: k) = TypeAp (f tp)

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

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

instance ShowF f => Show (TypeAp f tp) where
  showsPrec :: Int -> TypeAp f tp -> String -> String
showsPrec Int
p (TypeAp f tp
x) = Int -> f tp -> String -> String
forall k (f :: k -> *) (tp :: k).
ShowF f =>
Int -> f tp -> String -> String
showsPrecF Int
p f tp
x

instance HashableF f => Hashable (TypeAp f tp) where
  hashWithSalt :: Int -> TypeAp f tp -> Int
hashWithSalt Int
s (TypeAp f tp
x) = Int -> f tp -> Int
forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
hashWithSaltF Int
s f tp
x

------------------------------------------------------------------------
-- KnownRepr

-- | This class is parameterized by a kind @k@ (typically a data
-- kind), a type constructor @f@ of kind @k -> *@ (typically a GADT of
-- singleton types indexed by @k@), and an index parameter @ctx@ of
-- kind @k@.
class KnownRepr (f :: k -> Type) (ctx :: k) where
  knownRepr :: f ctx