{-# 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)