[Haskell-cafe] Re: Applying a Dynamic function to a container of Dynamics

[oleg at okmij.org]

Alfonso Acosta wrote:
> dynApp allows to apply a Dynamic function to a Dynamic argument:
>
> dynApp :: Dynamic -> Dynamic -> Dynamic
>
> I don't seem to find a way (without modifying Data.Dynamic itself) to
> code this function

This is not very difficult if we have a well-delineated (and still
infinite) type universe: to be precise, if we know the signature of
our type terms. That is usually a reasonable assumption. The trick is
to build a function that is an inverse of typeOf: given a TypeRep, we
wish to find its representative, a value whose type has the given
TypeRep. We use the result of this inverse function (to be called
reflect) when applying fromDynamic. We know that writing of reflect
is possible because we know the syntax of the type language (by
assumption) and because Haskell luckily is inconsistent as a logic
and so every type is populated. 

The code below borrows most of the machinery from the 
type-checker/typed-compiler
	http://okmij.org/ftp/Haskell/staged/IncopeTypecheck.hs
which may be entitled 'How to program hypothetical proofs', as the
long title comments explain. The above code essentially implements dynApp,
which is called there typecheck_app. We adapt that code below. We
assume that our type universe is described by the following syntax
	 data Type = Bool | Int | Type -> Type


Regarding the previous problem: the following bit

> -- 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))

was indeed essential. One of the main lessons of our APLAS paper was
the realization that things become significantly simpler if we do more
work at the value production site. We could not have implemented typed
Partial Evaluation or typed CPS so simply. The latter usually
considered to require significantly complex type systems, beyond the
reach of the mainstream languages. Incidentally, that paper promotes a
different way of building typed DSL (the final tagless way). 

	http://okmij.org/ftp/papers/tagless-final-APLAS.pdf
	http://www.cs.rutgers.edu/~ccshan/tagless/talk.pdf
	http://www.cs.rutgers.edu/~ccshan/quote/language.pdf

I was thinking that perhaps that method might be beneficial to your
application. I don't know your DSL language well enough to be able to
tell though...

{-# OPTIONS -fglasgow-exts -W #-}

module DA where

import Data.Typeable
import Data.Dynamic


data Dyn = forall a. Typeable a => Dyn a

-- Check to see if a term represents a function. If so,
-- return terms that witness the type of the argument and of the body
reflect_fn :: TypeRep -> Maybe (Dyn, Dyn)
reflect_fn tfun
   | (con,[arg1,arg2]) <- splitTyConApp tfun, con == arrowTyCon
   = Just (reflect arg1, reflect arg2)
reflect_fn _ = Nothing

arrowTyCon = typeRepTyCon (typeOf (undefined::Int->Int))

-- reflect typerep to a type (witness). The inverse of typeOf.
reflect :: TypeRep -> Dyn
reflect x | x == typeOf (undefined::Int)  = Dyn (undefined::Int)
reflect x | x == typeOf (undefined::Bool) = Dyn (undefined::Bool)
reflect x | Just (Dyn e1, Dyn e2) <- reflect_fn x
   = let mkfun :: a -> b -> (a->b); mkfun = undefined
     in Dyn (mkfun e1 e2)

-- the re-implementation of dynApply
mydynApply :: Dynamic -> Dynamic -> Maybe Dynamic
mydynApply e1 e2 |
       let tfun = dynTypeRep e1,
       let targ = dynTypeRep e2,
       Just tres <- funResultTy tfun targ,
       Dyn a <- reflect targ,
       Dyn b <- reflect tres,
       Just e1' <- fromDynamic e1,
       Just e2' <- fromDynamic e2 `asTypeOf` (Just a)
     = return $ toDyn (e1' e2' `asTypeOf` b)
mydynApply e1 e2 =
    fail $ unwords ["Bad App, of types ",show (dynTypeRep e1),"and",
                    show (dynTypeRep e2)]


test1 :: Maybe Bool
test1 = mydynApply (toDyn not) (toDyn False) >>= fromDynamic
-- Just True

test2 :: Maybe Bool
test2 = mydynApply (toDyn not) (toDyn (1::Int)) >>= fromDynamic
-- Nothing

test3 :: Maybe Int
test3 = mydynApply (toDyn ((+)::Int->Int->Int)) (toDyn (1::Int)) >>= 
	(\f -> mydynApply f (toDyn (2::Int))) >>=
	fromDynamic
-- Just 3