Re: [Haskell-cafe] Polymorphic dynamic typing

2007-11-23 Thread Derek Elkins 
On Fri, 2007-11-23 at 18:45 +, 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.

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

Re: [Haskell-cafe] Polymorphic dynamic typing

2007-11-23 Thread 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}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Polymorphic dynamic typing

2007-11-23 Thread Don Stewart 
derek.a.elkins:
 On Fri, 2007-11-23 at 18:45 +, 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.

That is the end point. Clean's dynamics only include a stripped down
type checker -- the step beyond that is something like hs-plugins, which
reuses the compiler's type checker at runtime splice points.

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