[Haskell-cafe] typeOf for polymorphic value

[oleg at okmij.org]

> 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