[Haskell-cafe] Polymorphic dynamic typing

[Roberto Zunino]

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}