[Haskell-cafe] typeOf for polymorphic value
Lennart Augustsson
lennart at augustsson.net
Fri Mar 27 11:05:15 EDT 2009
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, <oleg at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
More information about the Haskell-Cafe
mailing list