Sam, first I want to thank you for all your answers, you&#39;ve helped me a lot. Thanks!<br><br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div>
&gt; I&#39;m trying to implement a function wrapper, that given any function returns<br>
&gt; a function of the same type, but that maybe applies a different argument. So<br>
&gt; far I haven&#39;t been successful, and based on previous questions to the mail<br>
&gt; list it seemed that I needed to go to an untyped module because I couldn&#39;t<br>
&gt; constraint values to a given type.<br>
<br>
</div>In general, I don&#39;t think that any solution is going to work here.<br>
You can&#39;t take arbitrary functions and apply them to specific<br>
arguments (such as the string &quot;blabla&quot;) in a type-safe way.<br></blockquote><div><br>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.<br>
<br></div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

<br>
In you particular example, the function `f&#39; is a constant function.<br>
But what if it expected `Integer&#39; as its argument?  Then your untyped<br>
code would be violating the type invariants.<br></blockquote><div><br>I think in that case a contract violation error should happen (?)<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">


<br>
However, you can make your program work just by removing the<br>
parameterization over `A&#39;, and replacing that with `Any&#39;.  Then your<br>
program is safe, and your untyped module can safely call the function<br>
with any value it wants.</blockquote><div><br>In that case, my program can only work with values of type Any, and I&#39;d need to make all functions Any -&gt; (T Any) since I can&#39;t downcast to any other type, but since I&#39;m passing functions as arguments I will have the problem of subtyping between functions...  <br>

<br></div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
As an additional note, the `CAST&#39; operation you describe below, can&#39;t<br>
do exactly what you expect, because it&#39;s runtime semantics depends on<br>
how you instantiate `B&#39;.  But that would mean that you&#39;d have to<br>
generate code for the `CAST&#39; without knowing what `B&#39; is.</blockquote><div><br>do you think it can work if I do (CAST f (Integer -&gt; Boolean)) instead?<br><br>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?<br>
<br>is it that you statically prove that the body is OK for all A and B and then you don&#39;t get that information when applying??<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

Typed<br>
Racket, like ML or Haskell, doesn&#39;t pass type parameters around as<br>
values, so you can&#39;t do this.<br></blockquote><div><br>I don&#39;t know much about how the type system of ML or Haskell works.<br><br>What I&#39;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&#39;t type correctly the weaver function, so I tried with an untyped module. Maybe it is not possible at all??<br>
<br>Thanks again<br clear="all"></div></div><br>-- <br>Ismael<br><br>