[Haskell-cafe] Dynamic typing of polymorphic functions

[oleg at okmij.org]

Alfonso Acosta wrote:

> mapSY :: (Typeable a, Typeable b) => (a -> b) -> Signal a -> Signal b
> mapSY f (Signal primSig) = Signal (PrimSignal (MapSY  (toDyn f) primSig))
>
> The following process would be really useful but its compilation
> obviously fails:
>
> mapSnd :: Signal (a, a) -> Signal a
> mapSnd = mapSY snd
>
>
>     Could not deduce (Typeable a) from the context () arising from a
> use of `mapSY'
>     Possible fix:
>       add (Typeable a) to the context of the type signature for `mapSnd'

It seems the compiler's complaint is reasonable. The signature of the
mapSY function says that mapSY may only be applied _provided_ that type
variables 'a' and 'b' are instantiated to the types that are members
of Typeable. That is, mapSY has a condition on its use. When you
write

> mapSndInt :: Signal (Int, Int) -> Signal Int
> mapSndInt = mapSY (snd :: (Int, Int) -> Int)

the condition is satisfied: 'a' and 'b' are instantiated to Int, and
Int is a member of Typeable. The definition of mapSnd has no
constraint. The compiler is upset: mapSY requires a condition, and
mapSnd does not provide any, and there is no obvious way how an
obligation Typeable a could have been satisfied otherwise. So, writing

> mapSnd :: Typeable a => Signal (a, a) -> Signal a
> mapSnd = mapSY snd

is the logical thing to do. 

> Well, strangely enough, adding the "Typeable a" constraint hushed GHC
> but an error was instead triggered at runtime.

Perhaps the latter is the real problem. If one switches to dynamic
typing, the type errors show up as run-time errors. I believe the
typing of eval is a bit odd (and also not very useful). The following
code seems to work. It also shows how to apply a polymorphic function,
pairing, to to signals of any type. Here's a test:

> signal3 = cons const0 (cons const0 const1)
  *Foo> :t signal3
   signal3 :: Signal (Int, (Int, Float))

> test1 = mapSnd signal3
  test1 :: Signal (Int, Float)
> test12 = beval test1
   *Foo> :t test12
   test12 :: (Int, Float)
   *Foo> test12
   (0,1.0)

{-# OPTIONS -fglasgow-exts #-}

module Foo where

import Data.Typeable
import Data.Dynamic

-- the phantom type parameter makes signal typing consistent
newtype Signal a = Signal PrimSignal

newtype PrimSignal = PrimSignal (Proc (PrimSignal))

data Proc input =  MapSY Dynamic -- The processing function
                         input       --  The process input
                             -- the rest of the processes are omitted
		 | Const Dynamic
		 | Cons Dynamic input input

eval :: PrimSignal -> Dynamic
-- evaluates the output of a process for one input
eval (PrimSignal (MapSY dynF dynIn)) = dynApp dynF (eval dynIn)
eval (PrimSignal (Cons cns a1 a2)) = dynApp (dynApp cns (eval a1)) (eval a2)
eval (PrimSignal (Const inp)) = inp

-- better eval
beval :: Typeable a => Signal a -> a
beval (Signal s) = maybe undefined id (fromDynamic (eval s))

-- sample signals
const0 :: Signal Int
const0 = Signal (PrimSignal (Const (toDyn (0::Int))))
const1 :: Signal Float
const1 = Signal (PrimSignal (Const (toDyn (1::Float))))

-- the map process constructor
mapSY :: (Typeable a, Typeable b) => (a -> b) -> Signal a -> Signal b
mapSY f (Signal primSig) = Signal (PrimSignal (MapSY  (toDyn f) primSig))

add1 :: Signal Int -> Signal Int
add1 = mapSY ((+1) :: Int -> Int)

mapSndInt :: Signal (Int, Int) -> Signal Int
mapSndInt = mapSY (snd :: (Int, Int) -> Int)

-- it is important to give the signature to (,) below: we pack the cons
-- function of the right type!
cons :: forall a b. (Typeable a, Typeable b) =>
	Signal a -> Signal b -> Signal (a,b)
cons (Signal sig1) (Signal sig2) = 
    Signal (PrimSignal (Cons (toDyn ((,)::a->b->(a,b))) sig1 sig2))

mapSnd :: (Typeable a, Typeable b) => Signal (b, a) -> Signal a
mapSnd = mapSY snd


signal3 = cons const0 (cons const0 const1)
-- *Foo> :t signal3
-- signal3 :: Signal (Int, (Int, Float))

test1 = mapSnd signal3
-- test1 :: Signal (Int, Float)

test11 = let Signal s = test1 in eval s
-- *Foo> test11
-- <<(Int,Float)>>
-- Too bad. But we can do better.


test12 = beval test1
{-
*Foo> :t test12
test12 :: (Int, Float)
*Foo> test12
(0,1.0)
-}