{-# 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 #-}
module Data.SuchThat (
SuchThat(..)
,ambiguate
,ambiguously
,ForAny
,discoverStructure
,naturalTransformation
,unNaturalTransformation
,Some
,some
,Satisfies
,Contains
,Constrain
) where
import Data.Functor.Identity
import GHC.Exts (Constraint)
import Control.Monad (void)
import Unsafe.Coerce (unsafeCoerce)
data SuchThat (c :: [k -> Constraint]) (p :: k -> *) = forall s. Constrain c s => SuchThat (p s)
ambiguate :: forall c p s. Constrain c s => p s -> SuchThat c p
ambiguate = SuchThat
ambiguously :: forall c p r. (forall s. Constrain c s => p s -> r) -> SuchThat c p -> r
ambiguously f (SuchThat ps) = f ps
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 = ambiguously 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 n = ambiguously (ambiguate . 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 u (fx :: f x) = ambiguously id $ u (ambiguate @'[(~) 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 = ambiguate . 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