Oleg, You rock! And you're a star! So you must be a rock star. :)
Thanks! -- Lennart On Thu, Mar 26, 2009 at 5:33 AM, <o...@okmij.org> wrote: > >> 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 > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
