On Fri, 2007-11-23 at 18:45 +0000, Paulo Silva wrote:

Hello,

Type representations using GADTs are being used to achieve dynamic typing in Haskell. However, representing polymorphic types is problematic. Does anyone know any work about including polymorphism in dynamic typing?

Look at Clean's Dynamics. That said, the ultimate end of this direction is to include the type checker in the run-time.

Paulo Silva wrote:

Type representations using GADTs are being used to achieve dynamic typing in Haskell. However, representing polymorphic types is problematic. Does anyone know any work about including polymorphism in dynamic typing?

First, a warning: fragile code follows, possibly leveraging on GHC bugs related to mixing GADTs and type families. Comments welcome. Here's how to make current GHC HEAD (and maybe 6.8 ?) understand some selected polytype representations. We introduce a type family: type family Apply name a :: * Then, we select a particular polytype, say forall a . a -> [a] we introduce a phantom name for it, data Poly1 and define Apply accordingly: type instance Apply Poly1 a = a -> [a] Finally, we build type representations in the usual way: data Rep t where TPoly1 :: Rep Poly1 TAll :: Rep name -> Rep (forall a . Apply name a) Note the use of impredicativity in the TAll type. This indeed runs: *TypeRep> poly (TAll TPoly1) (\a -> [a,a,a]) 6 Regards, Zun. ============================================================ \begin{code} {-# OPTIONS_GHC -Wall -fglasgow-exts #-} module TypeRep where data Rep t where TPoly1 :: Rep Poly1 TPoly2 :: Rep Poly2 TAll :: Rep name -> Rep (forall a . Apply name a) type family Apply name a :: * data Poly1 type instance Apply Poly1 a = (a -> [a]) data Poly2 type instance Apply Poly2 a = ([a] -> [[a]]) poly :: forall a . (Rep a) -> a -> Int poly (TAll TPoly1) x = length (x 'a') + length (x "wow") poly (TAll TPoly2) x = length (x (x ['a'])) poly _ _ = 0 \end{code}