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