Does anyone know of a trick to accomplish `typeOf id'? Using something else than TypeRep as the representation, of course.
Yes. The analysis of polymorphic types has been used in the inverse type-checker http://okmij.org/ftp/Haskell/types.html#de-typechecker The enclosed code computes TypeRep of polymorphic values. The code returns real TypeRep. Here are a few examples: tt2 = mytypof not -- Bool -> Bool tt3 = mytypof [True] -- [Bool] tt4 = mytypof id -- any1 -> any1 tt5 = mytypof [] -- [any1] tt6 = mytypof const -- any1 -> any2 -> any1 tt7 = mytypof Just -- any1 -> Maybe any1 tt8 = mytypof map -- (any1 -> any2) -> [any1] -> [any2] tt9 = mytypof maybe -- any1 -> (any2 -> any1) -> Maybe any2 -> any1 The code was tested on GHC 6.8.2. I don't have access to any computer with GHC 6.10, so I can't say how it works with that version of GHC. {-# LANGUAGE ScopedTypeVariables, EmptyDataDecls #-} {-# LANGUAGE FlexibleInstances, FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE OverlappingInstances #-} {-# LANGUAGE IncoherentInstances #-} module Typeof where import Data.Typeable -- tests tt1 = mytypof True -- Bool tt2 = mytypof not -- Bool -> Bool tt3 = mytypof [True] -- [Bool] tt4 = mytypof id -- any1 -> any1 tt5 = mytypof [] -- [any1] tt6 = mytypof const -- any1 -> any2 -> any1 tt7 = mytypof Just -- any1 -> Maybe any1 tt8 = mytypof map -- (any1 -> any2) -> [any1] -> [any2] tt9 = mytypof maybe -- any1 -> (any2 -> any1) -> Maybe any2 -> any1 class MyTypeable a where mytypof :: a -> TypeRep -- Gamma is the sequence of type varaibles. It is used to assign -- different indices to different type variables instance (Analyze a result, MyTypeable' HNil gout result) => MyTypeable a where mytypof a = fst $ mytypof' HNil (analyze a) class MyTypeable' gin gout classification | gin classification -> gout where mytypof' :: gin -> classification -> (TypeRep,gout) instance Typeable a => MyTypeable' gin gin (TAtomic a) where mytypof' gin _ = (typeOf (undefined::a), gin) instance Typeable a => MyTypeable' gin gin (TAtomic1 a) where mytypof' gin _ = (typeOf (undefined::a), gin) instance (MyTypeable' gin g a, MyTypeable' g gout b) => MyTypeable' gin gout (TFunction a b) where mytypof' gin _ = let (tr1,g) = mytypof' gin (undefined::a) (tr2,gout) = mytypof' g (undefined::b) in (mkFunTy tr1 tr2,gout) instance (MyTypeable' gin g c, MyTypeable' g gout a) => MyTypeable' gin gout (TConstructed c a) where mytypof' gin _ = let (tr1,g) = mytypof' gin (undefined::c) (tr2,gout) = mytypof' g (undefined::a) in (mkTyConApp (typeRepTyCon tr1) [tr2],gout) instance (HIndex a gin n, MyTypeable'' n gin gout (TVariable a)) => MyTypeable' gin gout (TVariable a) where mytypof' = mytypof'' (undefined::n) class MyTypeable'' n gin gout classification | n gin classification ->gout where mytypof'' :: n -> gin -> classification -> (TypeRep,gout) instance HLen gin n1 => MyTypeable'' Z gin (HCons a gin) (TVariable a) where mytypof'' _ gin _ = (mkany (undefined::S n1), HCons (undefined::a) gin) instance Nat n => MyTypeable'' (S n) gin gin (TVariable a) where mytypof'' _ gin _ = (mkany (undefined::S n), gin) mkany :: Nat n => n -> TypeRep mkany n = mkTyConApp (mkTyCon ts) [] where ts = "any" ++ show (nat n) -- Lookup the index of an item x in the list l -- The index is 1-based. If not found, return 0 class Nat n => HIndex x l n | x l -> n instance HIndex x HNil Z instance (Nat n, TypeEq x a f, HIndex' f x (HCons a l) n) => HIndex x (HCons a l) n class HIndex' f x l n | f x l -> n instance HLen l n => HIndex' HTrue x l n instance HIndex x l n => HIndex' HFalse x (HCons a l) n -- Length of a list class Nat n => HLen l n | l -> n instance HLen HNil Z instance HLen l n => HLen (HCons a l) (S n) -- Analyze a type -- Result of the type analysis data TAtomic a data TVariable a data TFunction a b data TConstructed c a -- only one level: kind * -> * data TAtomic1 a data TVariable1 a data Level1 a data W a = W a -- We can have more levels, cf Typeable2, etc. class Analyze a b | a -> b analyze:: Analyze a b => a -> b analyze = undefined instance TypeCast f (TAtomic Int) => Analyze Int f instance TypeCast f (TAtomic Bool) => Analyze Bool f instance TypeCast f (TAtomic Char) => Analyze Char f instance TypeCast f (TAtomic Int) => Analyze (W Int) f instance TypeCast f (TAtomic Bool) => Analyze (W Bool) f instance TypeCast f (TAtomic Char) => Analyze (W Char) f instance (Analyze (c x) rx, Analyze (d y) ry, TypeCast f (TFunction rx ry)) => Analyze (c x->d y) f instance (Analyze (W x) rx, Analyze (d y) ry, TypeCast f (TFunction rx ry)) => Analyze (x->d y) f instance (Analyze (c x) rx, Analyze (W y) ry, TypeCast f (TFunction rx ry)) => Analyze (c x->y) f instance (Analyze (W x) rx, Analyze (W y) ry, TypeCast f (TFunction rx ry)) => Analyze (x->y) f instance (Analyze (W x) rx, Analyze (W y) ry, TypeCast f (TFunction rx ry)) => Analyze (W (x->y)) f instance (Analyze (Level1 (c ())) rc, Analyze (W x) rx, TypeCast f (TConstructed rc rx)) => Analyze (c x) f instance TypeCast f (TAtomic1 ([] ())) => Analyze (Level1 ([] ())) f instance TypeCast f (TAtomic1 (Maybe ())) => Analyze (Level1 (Maybe ())) f instance TypeCast f (TVariable1 (c ())) => Analyze (Level1 (c ())) f -- the most general instance instance TypeCast f (TVariable a) => Analyze (W a) f -- instance TypeCast f (TVariable a) => Analyze a f -- the most general instance {- ta1 = analyze True -- ta1 :: TAtomic Bool ta2 = analyze not -- ta2 :: TFunction (TAtomic Bool) (TAtomic Bool) ta3 = analyze [True] -- ta3 :: TConstructed (TAtomic1 [()]) (TAtomic Bool) ta4 = analyze id -- ta4 :: TFunction (TVariable GHC.Prim.Any) (TVariable GHC.Prim.Any) ta5 = analyze [] -- ta5 :: TConstructed (TAtomic1 [()]) (TVariable GHC.Prim.Any) ta6 = analyze const -- ta6 :: TFunction -- (TVariable GHC.Prim.Any) -- (TFunction (TVariable GHC.Prim.Any) (TVariable GHC.Prim.Any)) -} -- Standard HList stuff data Z data S a class Nat a where nat :: a -> Int instance Nat Z where nat _ = 0 instance Nat a => Nat (S a) where nat _ = succ (nat (undefined::a)) data HTrue data HFalse instance Show HTrue where show _ = "HTrue" instance Show HFalse where show _ = "HFalse" data HNil = HNil deriving Show data HCons a b = HCons a b deriving Show -- literally lifted from the HList library class TypeCast a b | a -> b, b->a where typeCast :: a -> b class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x = x class TypeEq' () x y b => TypeEq x y b | x y -> b where type'eq :: x -> y -> b type'eq _ _ = undefined::b class TypeEq' q x y b | q x y -> b class TypeEq'' q x y b | q x y -> b instance TypeEq' () x y b => TypeEq x y b instance TypeCast b HTrue => TypeEq' () x x b instance TypeEq'' q x y b => TypeEq' q x y b instance TypeEq'' () x y HFalse