{-|
Module: Data.SubType
Description: existentially quantified sub-type embeddings
Maintainer: Olaf Klinke
Stability: experimental

Functions with codomain `x`, regardless of their domain, 
can be encoded in the GADT 

@
data Codomain :: Type -> Type where
    Fun :: (y -> x) -> Codomain x
@

This module decorates this GADT with constraints on the domain `y` 
and generalizes functions to morphisms of arbitrary categories. 
-}
{-# LANGUAGE GADTs, KindSignatures, ConstraintKinds, PolyKinds, RankNTypes, ScopedTypeVariables #-}
module Data.SubType (SomeSubType(..),idSubType,runEmbedding,
    subDomain,runEmbeddingDynamic,
    GSubType(..),
    idGSubType,
    mapGSubType,
    runGEmbedding) where
import Data.Kind (Type,Constraint)
import Data.Proxy (Proxy(..))
import Data.Void (Void)
import Control.Category (Category,(<<<))
import qualified Control.Category as Cat
import Type.Reflection (Typeable,SomeTypeRep(..),someTypeRep)
import Data.Dynamic (Dynamic,fromDynamic)

-- * Sub-types in the category Hask

-- | Constrained sub-types. 
-- This data type records the embedding function 
-- but hides its domain in an existential type. 
-- This allows us to compute an embedding at run-time. 
-- As an extra parameter, we pass a type class so that only 
-- those sub-types are representable that are member of this class.
data SomeSubType :: (Type -> Constraint) -> Type -> Type where
    EmptySubType :: SomeSubType con t
    Embed :: con x => (x -> y) -> SomeSubType con y
-- TODO: any Category would do here.

domain :: forall cat a b. Typeable a => cat a b -> SomeTypeRep
domain :: forall {k} {k} (cat :: k -> k -> *) (a :: k) (b :: k).
Typeable a =>
cat a b -> SomeTypeRep
domain cat a b
_ = Proxy a -> SomeTypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a)

-- | The representation of the type of the domain of the sub-type embedding.
subDomain :: SomeSubType Typeable x -> SomeTypeRep
subDomain :: forall x. SomeSubType Typeable x -> SomeTypeRep
subDomain SomeSubType Typeable x
EmptySubType = Proxy Void -> SomeTypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep (Proxy Void
forall {k} (t :: k). Proxy t
Proxy :: Proxy Void)
subDomain (Embed x -> x
f) = (x -> x) -> SomeTypeRep
forall {k} {k} (cat :: k -> k -> *) (a :: k) (b :: k).
Typeable a =>
cat a b -> SomeTypeRep
domain x -> x
f

-- | post-compose embeddings with functions. 
-- This allows us to nest embeddings. 
instance Functor (SomeSubType con) where
    fmap :: forall a b. (a -> b) -> SomeSubType con a -> SomeSubType con b
fmap a -> b
_ SomeSubType con a
EmptySubType = SomeSubType con b
forall (con :: * -> Constraint) t. SomeSubType con t
EmptySubType
    fmap a -> b
g (Embed x -> a
f) = (x -> b) -> SomeSubType con b
forall (con :: * -> Constraint) y y.
con y =>
(y -> y) -> SomeSubType con y
Embed (a -> b
g(a -> b) -> (x -> a) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.x -> a
f)

-- | embed a type into itself via the identity function.
idSubType :: con t => SomeSubType con t
idSubType :: forall (con :: * -> Constraint) t. con t => SomeSubType con t
idSubType = (t -> t) -> SomeSubType con t
forall (con :: * -> Constraint) y y.
con y =>
(y -> y) -> SomeSubType con y
Embed t -> t
forall a. a -> a
id

-- | In order to run an embedding with unknown domain, 
-- we need a function that can convert a single universal type @rep@ 
-- to any sub-type. 
-- 'Nothing' is returned if the @rep@ value does not represent 
-- an element of the sub-type, in particular if the sub-type is empty. 
runEmbedding :: (forall x. con x => rep -> Maybe x) -> 
    SomeSubType con y -> 
    rep -> Maybe y
runEmbedding :: forall (con :: * -> Constraint) rep y.
(forall x. con x => rep -> Maybe x)
-> SomeSubType con y -> rep -> Maybe y
runEmbedding forall x. con x => rep -> Maybe x
maybeFrom (Embed x -> y
f) = (x -> y) -> Maybe x -> Maybe y
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> y
f (Maybe x -> Maybe y) -> (rep -> Maybe x) -> rep -> Maybe y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. rep -> Maybe x
forall x. con x => rep -> Maybe x
maybeFrom
runEmbedding forall x. con x => rep -> Maybe x
_ SomeSubType con y
EmptySubType = Maybe y -> rep -> Maybe y
forall a b. a -> b -> a
const Maybe y
forall a. Maybe a
Nothing

-- | It is guaranteed that for every @f :: y -> x@ with @Typeable y@,
-- 
-- @
-- runEmbeddingDynamic (Embed f) (toDyn y) = Just (f y)
-- @
runEmbeddingDynamic :: SomeSubType Typeable x -> Dynamic -> Maybe x
runEmbeddingDynamic :: forall x. SomeSubType Typeable x -> Dynamic -> Maybe x
runEmbeddingDynamic = (forall x. Typeable x => Dynamic -> Maybe x)
-> SomeSubType Typeable x -> Dynamic -> Maybe x
forall (con :: * -> Constraint) rep y.
(forall x. con x => rep -> Maybe x)
-> SomeSubType con y -> rep -> Maybe y
runEmbedding Dynamic -> Maybe x
forall x. Typeable x => Dynamic -> Maybe x
fromDynamic

-- * Sub-types in arbitrary categories

-- | Poly-kinded version of 'SomeSubType' 
-- generalized to arbitrary categories.
data GSubType :: (k -> k -> Type) -> (k -> Constraint) -> k -> Type where
    GEmpty :: GSubType cat con x
    GEmbed :: con y => cat y x -> GSubType cat con x
    -- TODO: an unconstrained Gid would be useful, 
    -- so that types that do not satisfy @con@ can have at least the identity sub-type.

-- | the identiy morphism
idGSubType :: (Category cat, con x) => GSubType cat con x
idGSubType :: forall {k} (cat :: k -> k -> *) (con :: k -> Constraint) (x :: k).
(Category cat, con x) =>
GSubType cat con x
idGSubType = cat x x -> GSubType cat con x
forall {k} (con :: k -> Constraint) (y :: k) (cat :: k -> k -> *)
       (x :: k).
con y =>
cat y x -> GSubType cat con x
GEmbed (cat x x
forall (a :: k). cat a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
Cat.id)

-- | @'GSubType' cat con@ is functorial on @cat@.
mapGSubType :: Category cat => cat x y -> GSubType cat con x -> GSubType cat con y
mapGSubType :: forall {k} (cat :: k -> k -> *) (x :: k) (y :: k)
       (con :: k -> Constraint).
Category cat =>
cat x y -> GSubType cat con x -> GSubType cat con y
mapGSubType cat x y
h (GEmbed cat y x
f) = cat y y -> GSubType cat con y
forall {k} (con :: k -> Constraint) (y :: k) (cat :: k -> k -> *)
       (x :: k).
con y =>
cat y x -> GSubType cat con x
GEmbed (cat x y
h cat x y -> cat y x -> cat y y
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
<<< cat y x
f)
mapGSubType cat x y
_ GSubType cat con x
GEmpty = GSubType cat con y
forall {k} (cat :: k -> k -> *) (con :: k -> Constraint) (x :: k).
GSubType cat con x
GEmpty

-- | generic version of 'runEmbedding'. 
runGEmbedding :: (forall g. con g => cat g f -> Dynamic -> Maybe (g ())) -- ^ dynamically convert to the sub-type
    -> (forall s . cat s f -> s () -> f ()) -- ^ run the @cat@ morphism
    -> GSubType cat con f -- ^ the sub-type embedding
    -> Dynamic            -- ^ dynamic representation of the argument
    -> Maybe (f ())
runGEmbedding :: forall (con :: (* -> *) -> Constraint)
       (cat :: (* -> *) -> (* -> *) -> *) (f :: * -> *).
(forall (g :: * -> *). con g => cat g f -> Dynamic -> Maybe (g ()))
-> (forall (s :: * -> *). cat s f -> s () -> f ())
-> GSubType cat con f
-> Dynamic
-> Maybe (f ())
runGEmbedding forall (g :: * -> *). con g => cat g f -> Dynamic -> Maybe (g ())
maybeFrom forall (s :: * -> *). cat s f -> s () -> f ()
runCat (GEmbed cat y f
h) = (y () -> f ()) -> Maybe (y ()) -> Maybe (f ())
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (cat y f -> y () -> f ()
forall (s :: * -> *). cat s f -> s () -> f ()
runCat cat y f
h) (Maybe (y ()) -> Maybe (f ()))
-> (Dynamic -> Maybe (y ())) -> Dynamic -> Maybe (f ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. cat y f -> Dynamic -> Maybe (y ())
forall (g :: * -> *). con g => cat g f -> Dynamic -> Maybe (g ())
maybeFrom cat y f
h
runGEmbedding forall (g :: * -> *). con g => cat g f -> Dynamic -> Maybe (g ())
_ forall (s :: * -> *). cat s f -> s () -> f ()
_ GSubType cat con f
GEmpty = Maybe (f ()) -> Dynamic -> Maybe (f ())
forall a b. a -> b -> a
const Maybe (f ())
forall a. Maybe a
Nothing
-- TODO: generalizing Dynamic to @rep@ does not work. Why?