# LANGUAGE NoMonomorphismRestriction #
# LANGUAGE PatternGuards #
{-# LANGUAGE Rank2Types, ExistentialQuantification #-}

-- * Type representation, equality and the safe typecast:
  * the above - the - board version of Data . Typeable

module Typ where

import Control.Monad
import Control.Monad.Error


  * The language of type representations : first - order and typed
-- It is quite like the language of int/neg/add we have seen before,
-- but it is now typed.
  It is first order : the language of simple types is first order

class TSYM trepr where
    tint :: trepr Int
    tarr :: trepr a -> trepr b -> trepr (a->b)

-- * The view interpreter
  The first interpreter is to view the types

newtype ShowT a = ShowT String

instance TSYM ShowT where
    tint = ShowT $ "Int"
    tarr (ShowT a) (ShowT b) = ShowT $ "(" ++ a ++ " -> " ++ b ++ ")"

view_t :: ShowT a -> String
view_t (ShowT s) = s
(~~>) = tarr
-- * //
-- * Quantifying over the TSYM interpreter
-- This closes the type universe

newtype TQ t = TQ{unTQ :: forall trepr. TSYM trepr => trepr t}

  TQ is itself an interpreter , the trivial one
instance TSYM TQ where
    tint = TQ tint
    tarr (TQ a) (TQ b) = TQ (tarr a b)

-- Sample type expressions

tt1 = (tint `tarr` tint) `tarr` tint
  tt1 : : ( TSYM trepr ) = >  ( ( Int - > Int ) - > Int )

tt2 = tint `tarr` (tint `tarr` tint)
  tt2 : : ( TSYM trepr ) = >  ( Int - > Int - > Int )

tt1_view = view_t (unTQ tt1)
-- "((Int -> Int) -> Int)"

tt2_view = view_t (unTQ tt2)
-- "(Int -> (Int -> Int))"

-- * //
-- * Show Typ-able expressions
-- * No Show type class constraint!

-- The signature is quite like gshow in a generic programming
  library such as EMGM or LIGD
show_as :: TQ a -> a -> String
show_as tr a = 
    case unTQ tr of ShowAs _ f -> f a

-- The implementation of the interpreter ShowAs shows off
  the technique of accumulating new  as we traverse the old
-- one. We shall see more examples later.
-- One is again reminded of attribute grammars.

data ShowAs a = ShowAs (TQ a) (a -> String)

instance TSYM ShowAs where
    tint = ShowAs tint show  -- as Int
    tarr (ShowAs t1 _) (ShowAs t2 _) =
        let t = tarr t1 t2 in
	ShowAs t (\_ ->  "<function of the type " ++ 
	                 view_t (unTQ t) ++ ">")
tt0_show = show_as tint 5
  " 5 "

tt1_show = show_as tt1 undefined
-- "<function of the type ((Int -> Int) -> Int)>"

-- We can't show functional values, but at least we should be
-- able to show their types

-- * //
-- * Type representation
  * Compare with Dyta .  . TypeRep
-- It is not a data structure!
data Typ = forall t. Typ (TQ t)


-- * //
-- * Alternative to quantification: copying
  Before instantiating one interpreter , we fork it .
  One copy can be instantiated , but the other remains polymorphic
-- Compare with Prolog's copy_term
-- This approach keeps the type universe extensible
  Again the same pattern : traverse one TQ and build another
  ( another two actually )

data TCOPY trep1 trep2 a = TCOPY (trep1 a) (trep2 a)

instance (TSYM trep1, TSYM trep2) 
    => TSYM (TCOPY trep1 trep2)
  where
    tint = TCOPY tint tint
    tarr (TCOPY a1 a2) (TCOPY b1 b2) = 
	TCOPY (tarr a1 b1) (tarr a2 b2)

-- * //
-- * Equality and safe type cast

-- * c is NOT necessarily a functor or injective!
-- For example, repr is not always a functor
-- I wonder if we can generalize to an arbitrary type function
-- represented by its label lab:
  newtype EQU a b = EQU ( forall lab . ( Apply lab a - > Apply lab b )
-- That would let us _easily_ show, for example, that
  EQU ( a , b ) ( c , d ) implies EQU a c , for all types a , b , c , d.

newtype EQU a b = EQU{equ_cast:: forall c. c a -> c b}

-- * Leibniz equality is reflexive, symmetric and transitive
-- Here is the constructive proof

refl :: EQU a a
refl = EQU id

-- * An Unusual `functor'
tran :: EQU a u -> EQU u b -> EQU a b
tran au ub = equ_cast ub au
  Why it works ? We consider ( EQU a u ) as ( EQU a ) u ,
  and so instantiate c to be EQU a

newtype FS b a = FS{unFS:: EQU a b}

symm :: EQU a b -> EQU b a
symm equ = unFS . equ_cast equ . FS $ refl

-- Useful type-level lambdas, so to speak
newtype F1 t b a = F1{unF1:: EQU t (a->b)}

newtype F2 t a b = F2{unF2:: EQU t (a->b)}

eq_arr :: EQU a1 a2 -> EQU b1 b2 -> EQU (a1->b1) (a2->b2)
eq_arr a1a2 b1b2 = 
    unF2 . equ_cast b1b2 . F2 . unF1 . equ_cast a1a2 . F1 $ refl

  How does this work ? what is the type of  above ?

-- * //
-- * Decide if (trepr a) represents a type that is equal to some type b
-- Informally, we compare a value that _represents_ a type b
-- against the _type_ b

-- We do that by interpreting trepr a in a particular way

-- * A constructive `deconstructor'
data AsInt a = AsInt (Maybe (EQU a Int))

instance TSYM AsInt where
    tint     = AsInt $ Just refl
    tarr _ _ = AsInt $ Nothing

-- This function proves useful later
as_int :: AsInt a -> c a -> Maybe (c Int)
as_int (AsInt (Just equ)) r = Just $ equ_cast equ r
as_int _ _ = Nothing

-- * Another constructive `deconstructor'

data AsArrow a = 
    forall b1 b2. AsArrow (TQ a) (Maybe (TQ b1, TQ b2, EQU a (b1->b2)))

instance TSYM AsArrow where
    tint       = AsArrow tint Nothing
    tarr (AsArrow t1 _) (AsArrow t2 _) = 
	         AsArrow (tarr t1 t2) $ Just (t1,t2,refl)

as_arrow :: AsArrow a -> AsArrow a
as_arrow = id

-- More cases could be added later on...

newtype SafeCast a = SafeCast (forall b. TQ b -> Maybe (EQU a b))

instance TSYM SafeCast where
    tint = SafeCast $ \tb -> 
	     case unTQ tb of AsInt eq -> fmap symm eq
    tarr (SafeCast t1) (SafeCast t2) = 
	 SafeCast $ \tb -> do
	     AsArrow _ (Just (b1,b2,equ_bb1b2)) <- 
		 return $ as_arrow (unTQ tb)
	     equ_t1b1 <- t1 b1
	     equ_t2b2 <- t2 b2
	     return $ tran (eq_arr equ_t1b1 equ_t2b2) (symm equ_bb1b2)


-- * Cf. Data.Typeable.gcast
  Data.Typeable.gcast : : ( Data . Typeable .   , Data . Typeable .  a ) = >
--                         c a -> Maybe (c b)
  We use our own ` Typeable ' , implemented without
  invoking GHC internals

safe_gcast :: TQ a -> c a -> TQ b -> Maybe (c b)
safe_gcast (TQ ta) ca tb = cast ta
 where cast (SafeCast f) = 
	 maybe Nothing (\equ -> Just (equ_cast equ ca)) $ f tb

-- There is a tantalizing opportunity of making SafeCast extensible

-- * //
-- * Our own version of Data.Dynamic
  We replace Data .  with  a

data Dynamic = forall t. Dynamic (TQ t) t

tdn1 = Dynamic tint 5

tdn2 = Dynamic tt1 ($ 1)

tdn3 = Dynamic (tint `tarr` (tint `tarr` tint)) (*)

tdn_show (Dynamic tr a) = show_as tr a

newtype Id a = Id a
tdn_eval1 (Dynamic tr d) x = do
  Id f <- safe_gcast tr (Id d) tt1
  return . show $ f x

tdn_eval2 (Dynamic tr d) x y = do
  Id f <- safe_gcast tr (Id d) tt2 
  return . show $ f x y

tdn1_show = tdn_show tdn1
  " 5 "

tdn2_show = tdn_show tdn2
-- "<function of the type ((Int -> Int) -> Int)>"

tdn3_show = tdn_show tdn3
-- "<function of the type (Int -> (Int -> Int))>"

tdn1_eval = tdn_eval1 tdn1 (+4)
-- Nothing

tdn2_eval = tdn_eval1 tdn2 (+4)
  Just " 5 "

tdn2_eval' = tdn_eval2 tdn2 3 14
-- Nothing

tdn3_eval = tdn_eval2 tdn3 3 14
  Just " 42 "


main = do
       print tt1_view
       print tt2_view
       print tt0_show
       print tt1_show
       print tdn1_show
       print tdn2_show
       print tdn3_show
       print tdn1_eval
       print tdn2_eval
       print tdn2_eval'
       print tdn3_eval

# LANGUAGE Rank2Types, ExistentialQuantification #
 * Type representation, equality and the safe typecast:
 It is quite like the language of int/neg/add we have seen before,
 but it is now typed.
 * The view interpreter
 * //
 * Quantifying over the TSYM interpreter
 This closes the type universe
 Sample type expressions
 "((Int -> Int) -> Int)"
 "(Int -> (Int -> Int))"
 * //
 * Show Typ-able expressions
 * No Show type class constraint!
 The signature is quite like gshow in a generic programming
 The implementation of the interpreter ShowAs shows off
 one. We shall see more examples later.
 One is again reminded of attribute grammars.
 as Int
 "<function of the type ((Int -> Int) -> Int)>"
 We can't show functional values, but at least we should be
 able to show their types
 * //
 * Type representation
 It is not a data structure!
 * //
 * Alternative to quantification: copying
 Compare with Prolog's copy_term
 This approach keeps the type universe extensible
 * //
 * Equality and safe type cast
 * c is NOT necessarily a functor or injective!
 For example, repr is not always a functor
 I wonder if we can generalize to an arbitrary type function
 represented by its label lab:
 That would let us _easily_ show, for example, that
 * Leibniz equality is reflexive, symmetric and transitive
 Here is the constructive proof
 * An Unusual `functor'
 Useful type-level lambdas, so to speak
 * //
 * Decide if (trepr a) represents a type that is equal to some type b
 Informally, we compare a value that _represents_ a type b
 against the _type_ b
 We do that by interpreting trepr a in a particular way
 * A constructive `deconstructor'
 This function proves useful later
 * Another constructive `deconstructor'
 More cases could be added later on...
 * Cf. Data.Typeable.gcast
                         c a -> Maybe (c b)
 There is a tantalizing opportunity of making SafeCast extensible
 * //
 * Our own version of Data.Dynamic
 "<function of the type ((Int -> Int) -> Int)>"
 "<function of the type (Int -> (Int -> Int))>"
 Nothing
 Nothing
# LANGUAGE NoMonomorphismRestriction #
# LANGUAGE PatternGuards #

  * the above - the - board version of Data . Typeable

module Typ where

import Control.Monad
import Control.Monad.Error


  * The language of type representations : first - order and typed
  It is first order : the language of simple types is first order

class TSYM trepr where
    tint :: trepr Int
    tarr :: trepr a -> trepr b -> trepr (a->b)

  The first interpreter is to view the types

newtype ShowT a = ShowT String

instance TSYM ShowT where
    tint = ShowT $ "Int"
    tarr (ShowT a) (ShowT b) = ShowT $ "(" ++ a ++ " -> " ++ b ++ ")"

view_t :: ShowT a -> String
view_t (ShowT s) = s
(~~>) = tarr

newtype TQ t = TQ{unTQ :: forall trepr. TSYM trepr => trepr t}

  TQ is itself an interpreter , the trivial one
instance TSYM TQ where
    tint = TQ tint
    tarr (TQ a) (TQ b) = TQ (tarr a b)


tt1 = (tint `tarr` tint) `tarr` tint
  tt1 : : ( TSYM trepr ) = >  ( ( Int - > Int ) - > Int )

tt2 = tint `tarr` (tint `tarr` tint)
  tt2 : : ( TSYM trepr ) = >  ( Int - > Int - > Int )

tt1_view = view_t (unTQ tt1)

tt2_view = view_t (unTQ tt2)


  library such as EMGM or LIGD
show_as :: TQ a -> a -> String
show_as tr a = 
    case unTQ tr of ShowAs _ f -> f a

  the technique of accumulating new  as we traverse the old

data ShowAs a = ShowAs (TQ a) (a -> String)

instance TSYM ShowAs where
    tarr (ShowAs t1 _) (ShowAs t2 _) =
        let t = tarr t1 t2 in
	ShowAs t (\_ ->  "<function of the type " ++ 
	                 view_t (unTQ t) ++ ">")
tt0_show = show_as tint 5
  " 5 "

tt1_show = show_as tt1 undefined


  * Compare with Dyta .  . TypeRep
data Typ = forall t. Typ (TQ t)


  Before instantiating one interpreter , we fork it .
  One copy can be instantiated , but the other remains polymorphic
  Again the same pattern : traverse one TQ and build another
  ( another two actually )

data TCOPY trep1 trep2 a = TCOPY (trep1 a) (trep2 a)

instance (TSYM trep1, TSYM trep2) 
    => TSYM (TCOPY trep1 trep2)
  where
    tint = TCOPY tint tint
    tarr (TCOPY a1 a2) (TCOPY b1 b2) = 
	TCOPY (tarr a1 b1) (tarr a2 b2)


  newtype EQU a b = EQU ( forall lab . ( Apply lab a - > Apply lab b )
  EQU ( a , b ) ( c , d ) implies EQU a c , for all types a , b , c , d.

newtype EQU a b = EQU{equ_cast:: forall c. c a -> c b}


refl :: EQU a a
refl = EQU id

tran :: EQU a u -> EQU u b -> EQU a b
tran au ub = equ_cast ub au
  Why it works ? We consider ( EQU a u ) as ( EQU a ) u ,
  and so instantiate c to be EQU a

newtype FS b a = FS{unFS:: EQU a b}

symm :: EQU a b -> EQU b a
symm equ = unFS . equ_cast equ . FS $ refl

newtype F1 t b a = F1{unF1:: EQU t (a->b)}

newtype F2 t a b = F2{unF2:: EQU t (a->b)}

eq_arr :: EQU a1 a2 -> EQU b1 b2 -> EQU (a1->b1) (a2->b2)
eq_arr a1a2 b1b2 = 
    unF2 . equ_cast b1b2 . F2 . unF1 . equ_cast a1a2 . F1 $ refl

  How does this work ? what is the type of  above ?



data AsInt a = AsInt (Maybe (EQU a Int))

instance TSYM AsInt where
    tint     = AsInt $ Just refl
    tarr _ _ = AsInt $ Nothing

as_int :: AsInt a -> c a -> Maybe (c Int)
as_int (AsInt (Just equ)) r = Just $ equ_cast equ r
as_int _ _ = Nothing


data AsArrow a = 
    forall b1 b2. AsArrow (TQ a) (Maybe (TQ b1, TQ b2, EQU a (b1->b2)))

instance TSYM AsArrow where
    tint       = AsArrow tint Nothing
    tarr (AsArrow t1 _) (AsArrow t2 _) = 
	         AsArrow (tarr t1 t2) $ Just (t1,t2,refl)

as_arrow :: AsArrow a -> AsArrow a
as_arrow = id


newtype SafeCast a = SafeCast (forall b. TQ b -> Maybe (EQU a b))

instance TSYM SafeCast where
    tint = SafeCast $ \tb -> 
	     case unTQ tb of AsInt eq -> fmap symm eq
    tarr (SafeCast t1) (SafeCast t2) = 
	 SafeCast $ \tb -> do
	     AsArrow _ (Just (b1,b2,equ_bb1b2)) <- 
		 return $ as_arrow (unTQ tb)
	     equ_t1b1 <- t1 b1
	     equ_t2b2 <- t2 b2
	     return $ tran (eq_arr equ_t1b1 equ_t2b2) (symm equ_bb1b2)


  Data.Typeable.gcast : : ( Data . Typeable .   , Data . Typeable .  a ) = >
  We use our own ` Typeable ' , implemented without
  invoking GHC internals

safe_gcast :: TQ a -> c a -> TQ b -> Maybe (c b)
safe_gcast (TQ ta) ca tb = cast ta
 where cast (SafeCast f) = 
	 maybe Nothing (\equ -> Just (equ_cast equ ca)) $ f tb


  We replace Data .  with  a

data Dynamic = forall t. Dynamic (TQ t) t

tdn1 = Dynamic tint 5

tdn2 = Dynamic tt1 ($ 1)

tdn3 = Dynamic (tint `tarr` (tint `tarr` tint)) (*)

tdn_show (Dynamic tr a) = show_as tr a

newtype Id a = Id a
tdn_eval1 (Dynamic tr d) x = do
  Id f <- safe_gcast tr (Id d) tt1
  return . show $ f x

tdn_eval2 (Dynamic tr d) x y = do
  Id f <- safe_gcast tr (Id d) tt2 
  return . show $ f x y

tdn1_show = tdn_show tdn1
  " 5 "

tdn2_show = tdn_show tdn2

tdn3_show = tdn_show tdn3

tdn1_eval = tdn_eval1 tdn1 (+4)

tdn2_eval = tdn_eval1 tdn2 (+4)
  Just " 5 "

tdn2_eval' = tdn_eval2 tdn2 3 14

tdn3_eval = tdn_eval2 tdn3 3 14
  Just " 42 "


main = do
       print tt1_view
       print tt2_view
       print tt0_show
       print tt1_show
       print tdn1_show
       print tdn2_show
       print tdn3_show
       print tdn1_eval
       print tdn2_eval
       print tdn2_eval'
       print tdn3_eval
