Re: [Haskell-cafe] typeOf for polymorphic value

2009-03-27 Thread Roland Zumkeller 
Hi Lennart,

This is not a real solution, but maybe helpful. The hint package
(wrapping the ghc API) has its typeOf:

cabal install hint

 import Language.Haskell.Interpreter
 runInterpreter (typeOf \\x - x)
Right t - t

Best,

Roland


On Wed, Mar 25, 2009 at 7:33 PM, Lennart Augustsson
lenn...@augustsson.net wrote:
 Using Data.Typeable.typeOf we can get a representation of the the type
 of a monomorphic value, for instance
  Prelude Data.Typeable typeOf not
  Bool - Bool

 But if we try using it on a polymorphic value it fails
  Prelude Data.Typeable typeOf id

  interactive:1:0:
    Ambiguous type variable `a' in the constraint:
      `Typeable a' arising from a use of `typeOf' at interactive:1:0-8
    Probable fix: add a type signature that fixes these type variable(s)

 And understandably so.  Does anyone know of a trick to accomplish `typeOf id'?
 Using something else than TypeRep as the representation, of course.

 Any tricks and existing language extensions are welcome.
 (As ghc moves towards first class polymorphic values this question
 gets more interesting.)

  -- Lennart
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe




-- 
http://roland.zumkeller.googlepages.com/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] typeOf for polymorphic value

2009-03-27 Thread Lennart Augustsson 
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

[Haskell-cafe] typeOf for polymorphic value

2009-03-25 Thread Lennart Augustsson 
Using Data.Typeable.typeOf we can get a representation of the the type
of a monomorphic value, for instance
  Prelude Data.Typeable typeOf not
  Bool - Bool

But if we try using it on a polymorphic value it fails
  Prelude Data.Typeable typeOf id

  interactive:1:0:
Ambiguous type variable `a' in the constraint:
  `Typeable a' arising from a use of `typeOf' at interactive:1:0-8
Probable fix: add a type signature that fixes these type variable(s)

And understandably so.  Does anyone know of a trick to accomplish `typeOf id'?
Using something else than TypeRep as the representation, of course.

Any tricks and existing language extensions are welcome.
(As ghc moves towards first class polymorphic values this question
gets more interesting.)

  -- Lennart
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] typeOf for polymorphic value

2009-03-25 Thread oleg 

 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