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