{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveDataTypeable    #-}
-- |
-- Module      : TypeLevel.Reify
-- Copyright   : Alexey Khudyakov
-- License     : BSD3-style (see LICENSE)
--
-- Maintainer  : Alexey Khudyakov <alexey.skladnoy@gmail.com>
-- Stability   : unstable
-- Portability : unportable (GHC only)
module TypeLevel.Reify ( Witness(..)
                       , Reify(..)
                       ) where

import Data.Data (Data,Typeable)


-- | Value with type tag
data Witness t a = Witness { Witness t a -> a
getValue :: a }
                   deriving (Int -> Witness t a -> ShowS
[Witness t a] -> ShowS
Witness t a -> String
(Int -> Witness t a -> ShowS)
-> (Witness t a -> String)
-> ([Witness t a] -> ShowS)
-> Show (Witness t a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall t a. Show a => Int -> Witness t a -> ShowS
forall t a. Show a => [Witness t a] -> ShowS
forall t a. Show a => Witness t a -> String
showList :: [Witness t a] -> ShowS
$cshowList :: forall t a. Show a => [Witness t a] -> ShowS
show :: Witness t a -> String
$cshow :: forall t a. Show a => Witness t a -> String
showsPrec :: Int -> Witness t a -> ShowS
$cshowsPrec :: forall t a. Show a => Int -> Witness t a -> ShowS
Show,Witness t a -> Witness t a -> Bool
(Witness t a -> Witness t a -> Bool)
-> (Witness t a -> Witness t a -> Bool) -> Eq (Witness t a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall t a. Eq a => Witness t a -> Witness t a -> Bool
/= :: Witness t a -> Witness t a -> Bool
$c/= :: forall t a. Eq a => Witness t a -> Witness t a -> Bool
== :: Witness t a -> Witness t a -> Bool
$c== :: forall t a. Eq a => Witness t a -> Witness t a -> Bool
Eq,Typeable,Typeable (Witness t a)
DataType
Constr
Typeable (Witness t a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Witness t a -> c (Witness t a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Witness t a))
-> (Witness t a -> Constr)
-> (Witness t a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Witness t a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Witness t a)))
-> ((forall b. Data b => b -> b) -> Witness t a -> Witness t a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Witness t a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Witness t a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Witness t a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Witness t a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a))
-> Data (Witness t a)
Witness t a -> DataType
Witness t a -> Constr
(forall b. Data b => b -> b) -> Witness t a -> Witness t a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Witness t a -> c (Witness t a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Witness t a)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Witness t a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Witness t a -> u
forall u. (forall d. Data d => d -> u) -> Witness t a -> [u]
forall t a. (Data t, Data a) => Typeable (Witness t a)
forall t a. (Data t, Data a) => Witness t a -> DataType
forall t a. (Data t, Data a) => Witness t a -> Constr
forall t a.
(Data t, Data a) =>
(forall b. Data b => b -> b) -> Witness t a -> Witness t a
forall t a u.
(Data t, Data a) =>
Int -> (forall d. Data d => d -> u) -> Witness t a -> u
forall t a u.
(Data t, Data a) =>
(forall d. Data d => d -> u) -> Witness t a -> [u]
forall t a r r'.
(Data t, Data a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Witness t a -> r
forall t a r r'.
(Data t, Data a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Witness t a -> r
forall t a (m :: * -> *).
(Data t, Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
forall t a (m :: * -> *).
(Data t, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
forall t a (c :: * -> *).
(Data t, Data a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Witness t a)
forall t a (c :: * -> *).
(Data t, Data a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Witness t a -> c (Witness t a)
forall t a (t :: * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Witness t a))
forall t a (t :: * -> * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Witness t a))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Witness t a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Witness t a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Witness t a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Witness t a -> c (Witness t a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Witness t a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Witness t a))
$cWitness :: Constr
$tWitness :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
$cgmapMo :: forall t a (m :: * -> *).
(Data t, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
gmapMp :: (forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
$cgmapMp :: forall t a (m :: * -> *).
(Data t, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
gmapM :: (forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
$cgmapM :: forall t a (m :: * -> *).
(Data t, Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Witness t a -> m (Witness t a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Witness t a -> u
$cgmapQi :: forall t a u.
(Data t, Data a) =>
Int -> (forall d. Data d => d -> u) -> Witness t a -> u
gmapQ :: (forall d. Data d => d -> u) -> Witness t a -> [u]
$cgmapQ :: forall t a u.
(Data t, Data a) =>
(forall d. Data d => d -> u) -> Witness t a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Witness t a -> r
$cgmapQr :: forall t a r r'.
(Data t, Data a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Witness t a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Witness t a -> r
$cgmapQl :: forall t a r r'.
(Data t, Data a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Witness t a -> r
gmapT :: (forall b. Data b => b -> b) -> Witness t a -> Witness t a
$cgmapT :: forall t a.
(Data t, Data a) =>
(forall b. Data b => b -> b) -> Witness t a -> Witness t a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Witness t a))
$cdataCast2 :: forall t a (t :: * -> * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Witness t a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Witness t a))
$cdataCast1 :: forall t a (t :: * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Witness t a))
dataTypeOf :: Witness t a -> DataType
$cdataTypeOf :: forall t a. (Data t, Data a) => Witness t a -> DataType
toConstr :: Witness t a -> Constr
$ctoConstr :: forall t a. (Data t, Data a) => Witness t a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Witness t a)
$cgunfold :: forall t a (c :: * -> *).
(Data t, Data a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Witness t a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Witness t a -> c (Witness t a)
$cgfoldl :: forall t a (c :: * -> *).
(Data t, Data a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Witness t a -> c (Witness t a)
$cp1Data :: forall t a. (Data t, Data a) => Typeable (Witness t a)
Data)

-- | Convert type level into value level using 
class Reify t a where
  witness :: Witness t a