{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
-- | Provides the type @SuchThat@, which encapsulates an existentially quantified type.
module Data.SuchThat (
  -- * Constrained Containers
   SuchThat(..)
  ,ambiguate
  ,ambiguously
  -- * ForAny
  ,ForAny
  -- ** Functions that work with ForAny
  ,discoverStructure
  ,naturalTransformation
  ,unNaturalTransformation
  -- * Constrained Values
  ,Some
  ,some
  ,Satisfies
  ,Contains
  -- * Type Machinery
  ,Constrain
  ) where

import Data.Functor.Identity
import GHC.Exts (Constraint)
import Control.Monad (void)
import Unsafe.Coerce (unsafeCoerce)

-- | A @'SuchThat' c p@ is a @p s@, where @s@ is such that it satisfies all of the constraints in @c@.
-- Note that you must always wrap results from pattern-matching on the @'SuchThat'@ constructor in a @'SuchThat'@, or GHC will complain about @s@ escaping its scope.
--
-- Ideally, we would write:
--
-- > type SuchThat (c :: [k -> Constraint]) (p :: k -> *) = forall s. Constrain c s => p s
-- 
-- But type synonyms don't work that way
data SuchThat (c :: [k -> Constraint]) (p :: k -> *) = forall s. Constrain c s => SuchThat (p s)

-- | Inject a value into a @'SuchThat'@. It becomes more ambiguous because it throws out the exact type of @s@.
ambiguate :: forall c p s. Constrain c s => p s -> SuchThat c p
ambiguate :: forall {k} (c :: [k -> Constraint]) (p :: k -> *) (s :: k).
Constrain c s =>
p s -> SuchThat c p
ambiguate = p s -> SuchThat c p
forall {k} (c :: [k -> Constraint]) (p :: k -> *) (s :: k).
Constrain c s =>
p s -> SuchThat c p
SuchThat

-- | Escape from a @'SuchThat'@ by running a universally quantified continuation.
ambiguously :: forall c p r. (forall s. Constrain c s => p s -> r) -> SuchThat c p -> r
ambiguously :: forall {k} (c :: [k -> Constraint]) (p :: k -> *) r.
(forall (s :: k). Constrain c s => p s -> r) -> SuchThat c p -> r
ambiguously forall (s :: k). Constrain c s => p s -> r
f (SuchThat p s
ps) = p s -> r
forall (s :: k). Constrain c s => p s -> r
f p s
ps

-- | A @'ForAny' f@ is an @f@ containing some arbitrary values, meaning you can only apply operations that would work /for any/ type of value it contains.
-- This is useful if the type parameter is phantom because it allows you to ignore it. 
-- This is called "ghost busting" because it removes the phantom.
-- It can also be used for reading only the /structure/ of something rather than the actual values.
-- For example, @'ForAny' []@ is isomorphic to both the natural numbers, and the fixed point of @'Data.Maybe.Maybe'@.
type ForAny = SuchThat '[]

-- | If the type constructor in question is a functor, we can scope out its structure by converting every element to @()@.
-- Note that this is actually the most general way to do this, since the type signature would otherwise be @Functor p => SuchThat c p -> (forall x. x -> a) -> p a@.
-- That means the output type must be isomorphic to @()@ because that is the terminal object in @Hask@.
--
--   >>> discoverStructure (ambiguate ['a','b','c'] :: ForAny [])
--   [(),(),()]
--   
--   >>> discoverStructure (ambiguate (Just "hi") :: ForAny Maybe)
--   Just ()
--
--   >>> discoverStructure (ambiguate Nothing :: ForAny Maybe) 
--   Nothing
discoverStructure :: Functor p => SuchThat c p -> p ()
discoverStructure :: forall (p :: * -> *) (c :: [* -> Constraint]).
Functor p =>
SuchThat c p -> p ()
discoverStructure = (forall s. Constrain c s => p s -> p ()) -> SuchThat c p -> p ()
forall {k} (c :: [k -> Constraint]) (p :: k -> *) r.
(forall (s :: k). Constrain c s => p s -> r) -> SuchThat c p -> r
ambiguously p s -> p ()
forall s. Constrain c s => p s -> p ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void

-- | A function between @'SuchThat' c@'s between different type constructors is isomorphic to a natural transformation between those type constructors.
-- This is especially useful if @c ~ '[]@, meaning you have a @'ForAny'@.
naturalTransformation :: (forall x. f x -> g x) -> (forall c. SuchThat c f -> SuchThat c g)
naturalTransformation :: forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x)
-> forall (c :: [k -> Constraint]). SuchThat c f -> SuchThat c g
naturalTransformation forall (x :: k). f x -> g x
n = (forall (s :: k). Constrain c s => f s -> SuchThat c g)
-> SuchThat c f -> SuchThat c g
forall {k} (c :: [k -> Constraint]) (p :: k -> *) r.
(forall (s :: k). Constrain c s => p s -> r) -> SuchThat c p -> r
ambiguously (g s -> SuchThat c g
forall {k} (c :: [k -> Constraint]) (p :: k -> *) (s :: k).
Constrain c s =>
p s -> SuchThat c p
ambiguate (g s -> SuchThat c g) -> (f s -> g s) -> f s -> SuchThat c g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f s -> g s
forall (x :: k). f x -> g x
n)

-- | The other half of the aforementioned isomorphism. This specialises @c@ to @'['Constains' x]@ under the hood.
unNaturalTransformation :: forall f g. (forall c. SuchThat c f -> SuchThat c g) -> (forall x. f x -> g x)
unNaturalTransformation :: forall {k} (f :: k -> *) (g :: k -> *).
(forall (c :: [k -> Constraint]). SuchThat c f -> SuchThat c g)
-> forall (x :: k). f x -> g x
unNaturalTransformation forall (c :: [k -> Constraint]). SuchThat c f -> SuchThat c g
u (f x
fx :: f x) = (forall (s :: k). Constrain '[(~) x] s => g s -> g x)
-> SuchThat '[(~) x] g -> g x
forall {k} (c :: [k -> Constraint]) (p :: k -> *) r.
(forall (s :: k). Constrain c s => p s -> r) -> SuchThat c p -> r
ambiguously g s -> g x
g s -> g s
forall (s :: k). Constrain '[(~) x] s => g s -> g x
forall a. a -> a
id (SuchThat '[(~) x] g -> g x) -> SuchThat '[(~) x] g -> g x
forall a b. (a -> b) -> a -> b
$ SuchThat '[(~) x] f -> SuchThat '[(~) x] g
forall (c :: [k -> Constraint]). SuchThat c f -> SuchThat c g
u (forall (c :: [k -> Constraint]) (p :: k -> *) (s :: k).
Constrain c s =>
p s -> SuchThat c p
forall {k} (c :: [k -> Constraint]) (p :: k -> *) (s :: k).
Constrain c s =>
p s -> SuchThat c p
ambiguate @'[(~) x] f x
fx)

-- | A @'Contains' x f@ is isomorphic to an @f x@:
--
-- > containsToRaw :: Contains x f -> f x
-- > containsToRaw = ambiguously id
--
-- > rawToContains :: f x -> Contains x f
-- > rawToContains = ambiguate
type Contains x = SuchThat '[(~) x]

-- | A @'Some' c@ is some value that satisfies all the constraints in @c@.
type Some c = SuchThat c Identity

-- | Build a @'Some' c@ from some thing that satisfies @c@.
some :: Constrain c a => a -> Some c
some :: forall (c :: [* -> Constraint]) a. Constrain c a => a -> Some c
some = Identity a -> SuchThat c Identity
forall {k} (c :: [k -> Constraint]) (p :: k -> *) (s :: k).
Constrain c s =>
p s -> SuchThat c p
ambiguate (Identity a -> SuchThat c Identity)
-> (a -> Identity a) -> a -> SuchThat c Identity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity a
forall a. a -> Identity a
Identity

-- | A @'Satisfies' x@ is a value that satisfies the single constraint x.
type Satisfies x = Some '[x]

-- | A type level fold for applying many constraints to the same thing
type family Constrain (c :: [k -> Constraint]) (x :: k) :: Constraint where
  Constrain (c ': '[]) x = c x
  Constrain (c ': cs) x = (c x,Constrain cs x)
  Constrain '[] x = x ~ x