[racket] Typed Racket: problem with interaction between typed/untyped modules

Sam, first I want to thank you for all your answers, you've helped me a
lot. Thanks!

 > I'm trying to implement a function wrapper, that given any function
> returns
> > a function of the same type, but that maybe applies a different
> argument. So
> > far I haven't been successful, and based on previous questions to the
> mail
> > list it seemed that I needed to go to an untyped module because I
> couldn't
> > constraint values to a given type.
>
> In general, I don't think that any solution is going to work here.
> You can't take arbitrary functions and apply them to specific
> arguments (such as the string "blabla") in a type-safe way.
>

For what I know, the design goal of Typed Racket is to avoid all runtime
errors. Maybe that is too strict for programs like the one I intend to
make. The idea of proposing a cast operation is to be able to establish a
tradeoff between type safety and expressive power, according to the
programmer needs.


> In you particular example, the function `f' is a constant function.
> But what if it expected `Integer' as its argument?  Then your untyped
> code would be violating the type invariants.
>

I think in that case a contract violation error should happen (?)


>
> However, you can make your program work just by removing the
> parameterization over `A', and replacing that with `Any'.  Then your
> program is safe, and your untyped module can safely call the function
> with any value it wants.


In that case, my program can only work with values of type Any, and I'd
need to make all functions Any -> (T Any) since I can't downcast to any
other type, but since I'm passing functions as arguments I will have the
problem of subtyping between functions...

As an additional note, the `CAST' operation you describe below, can't
> do exactly what you expect, because it's runtime semantics depends on
> how you instantiate `B'.  But that would mean that you'd have to
> generate code for the `CAST' without knowing what `B' is.


do you think it can work if I do (CAST f (Integer -> Boolean)) instead?

Maybe the flaw in my reasoning is that I think that when you evaluate the
polymorphic function, then you know what A and B are... so you should be
able to cast a value to B, is not that so?

is it that you statically prove that the body is OK for all A and B and
then you don't get that information when applying??


> Typed
> Racket, like ML or Haskell, doesn't pass type parameters around as
> values, so you can't do this.
>

I don't know much about how the type system of ML or Haskell works.

What I'm trying to do, so you get the full picture, is to write a variation
of Aspect Scheme in Typed Racket, so you can statically check that advice
is well-typed. I couldn't type correctly the weaver function, so I tried
with an untyped module. Maybe it is not possible at all??

Thanks again

-- 
Ismael
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20111202/29ab6c19/attachment.html>