gmane.comp.lang.haskell.cafe

oleg | 20 Dec 11:46

Dynamic typing of polymorphic functions

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

(Continue reading)

headers

Alfonso Acosta | 21 Dec 12:13

Re: Dynamic typing of polymorphic functions

Hi Oleg!

Thanks a lot for your answer, you turn out to end up solving every
problem I get stuck in :)

This bit was the essential part of it.

On Dec 20, 2007 11:47 AM,  <oleg <at> okmij.org> wrote:

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

headers

oleg | 22 Dec 10:44

Re: Applying a Dynamic function to a container of Dynamics

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

(Continue reading)