{-# LANGUAGE DeriveDataTypeable, StandaloneDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- An example of (data)type introspection
-- Philip Wadler (in Aug 2011) has posed a question about type introspection
-- ``whether the information about types could be turned into a graph 
-- and manipulated as such''
-- Specifically:
--    Given a type, does it contain any substructures of recursive type?
--    Given a type, if it is not recursive, what is it's maximum depth?
--    (E.g., Pair Int (Either Int Int) has depth 3.)

-- This file shows that the questions can be answered using SYB,
-- specifically, Data.Data. 
-- We show the code that computes the depth of a data type
-- and a depth of the specific variant of a data type.
-- The code works for all types for which Data.Data instance exist.
-- For recursive types, the code reports the infinite depth.

module TypeRefl where

import Data.Data
import Prelude hiding (succ)

-- Sample data types
data Pair a b = Pair a b deriving Data

deriving instance Typeable2 Pair

-- Non-recursive data type
data T1 = T1 (Pair Int (Either Int Int))
	deriving (Typeable, Data)

-- Recursive data type
data T2 = F1 T1 | F2 (Pair T1 [T1]) | F3 (Pair T1 T2)
	deriving (Typeable, Data)


-- Warm-up
-- Given a particular value of a data type, determine
-- its depth.
-- For a variant data type, the given value obviously contains
-- one specific variant; we do not have examine the others.
-- This simplifies problem, which can be solved with a 
-- generalized fold.

newtype Depth a = Depth IntW deriving (Show, Eq, Ord)

depth_data :: Data a => a -> Depth a
depth_data = gfoldl branch empty
 where
 branch :: Data d => Depth (d -> b) -> d -> Depth b
 branch (Depth n) d = let Depth n1 = depth_data d
                      in Depth (max n (succ n1))
 empty :: g -> Depth g
 empty _ = Depth (I 1) 			-- Leaf of the type tree


-- Full problem: The depth of a type
-- In this general problem, we are not given any value of the type.
-- If the type is an algebraic sum data type, we have to examine
-- all of its variants, that is, all of its constructors.
-- For the full problem, we need generalized unfold.

-- To detect loops, we keep track of the types we have already seen
type SeenTypes = [TypeRep] 

depth_ctor :: Data a => SeenTypes -> Constr -> Depth a
depth_ctor seen = gunfold branch empty
 where
 branch :: forall r b. Data b => Depth (b -> r) -> Depth r
 branch (Depth n) = let Depth n1 = depth_type' seen :: Depth b
                    in Depth (max n (succ n1))
 empty  :: r -> Depth r
 empty _ = Depth (I 1) 			-- Leaf of the type tree


depth_type' :: forall a. Data a => SeenTypes -> Depth a
depth_type' seen = check seen (typeOf (undefined::a))
 where
 check seen trep | trep `elem` seen = Depth Infinity
 check seen trep = 
     maximum (Depth (I 1): 
	      map (depth_ctor (trep:seen)) (ctors (undefined :: a)))
 ctors :: forall a. Data a => a -> [Constr]  -- all constructors of a data type
 ctors x = let dt = dataTypeOf x
           in case dataTypeRep dt of
                   (AlgRep cons) -> cons
		   _             -> []

depth_type :: forall a. Data a => Depth a
depth_type = depth_type' []

-- tests


t1 = depth_data $ T1 (Pair 1 (Left 2))
-- Depth (I 4)

t2 = depth_type :: Depth T1
-- Depth (I 4)

t21 = depth_type :: Depth (Maybe T1)
-- Depth (I 5)

t22 = depth_type :: Depth (T1, Maybe T1)
-- Depth (I 6)

t23 = depth_type :: Depth ((Int,T1), Maybe T1)
-- Depth (I 6)

t24 = depth_type :: Depth ((Int,T1), [T1])
-- Depth Infinity (List is a recursive data type)


t3 = depth_data $ (F2 (Pair (T1 (Pair 1 (Left 2))) []))
-- Depth (I 6)

t4 = depth_type :: Depth T2
-- Depth Infinity


-- An Int with the positive Infinity
data IntW = Infinity | I Int deriving (Eq, Show)

instance Ord IntW where
  compare Infinity Infinity = EQ
  compare Infinity x        = GT
  compare x Infinity        = LT
  compare (I x) (I y)       = compare x y

succ :: IntW -> IntW
succ Infinity = Infinity
succ (I x)    = I (x+1)