<br><br><div class="gmail_quote">2011/12/2 Sam Tobin-Hochstadt <span dir="ltr">&lt;<a href="mailto:samth@ccs.neu.edu">samth@ccs.neu.edu</a>&gt;</span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div><div></div><div class="h5">On Fri, Dec 2, 2011 at 6:26 PM, Ismael Figueroa Palet<br>
&lt;<a href="mailto:ifigueroap@gmail.com">ifigueroap@gmail.com</a>&gt; wrote:<br>
&gt; Sam, first I want to thank you for all your answers, you&#39;ve helped me a lot.<br>
&gt; Thanks!<br>
&gt;<br>
&gt;&gt; &gt; I&#39;m trying to implement a function wrapper, that given any function<br>
&gt;&gt; &gt; returns<br>
&gt;&gt; &gt; a function of the same type, but that maybe applies a different<br>
&gt;&gt; &gt; argument. So<br>
&gt;&gt; &gt; far I haven&#39;t been successful, and based on previous questions to the<br>
&gt;&gt; &gt; mail<br>
&gt;&gt; &gt; list it seemed that I needed to go to an untyped module because I<br>
&gt;&gt; &gt; couldn&#39;t<br>
&gt;&gt; &gt; constraint values to a given type.<br>
&gt;&gt;<br>
&gt;&gt; In general, I don&#39;t think that any solution is going to work here.<br>
&gt;&gt; You can&#39;t take arbitrary functions and apply them to specific<br>
&gt;&gt; arguments (such as the string &quot;blabla&quot;) in a type-safe way.<br>
&gt;<br>
&gt;<br>
&gt; For what I know, the design goal of Typed Racket is to avoid all runtime<br>
&gt; errors. Maybe that is too strict for programs like the one I intend to make.<br>
&gt; The idea of proposing a cast operation is to be able to establish a tradeoff<br>
&gt; between type safety and expressive power, according to the programmer needs.<br>
&gt;<br>
&gt;&gt;<br>
&gt;&gt; In you particular example, the function `f&#39; is a constant function.<br>
&gt;&gt; But what if it expected `Integer&#39; as its argument?  Then your untyped<br>
&gt;&gt; code would be violating the type invariants.<br>
&gt;<br>
&gt;<br>
&gt; I think in that case a contract violation error should happen (?)<br>
&gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; However, you can make your program work just by removing the<br>
&gt;&gt; parameterization over `A&#39;, and replacing that with `Any&#39;.  Then your<br>
&gt;&gt; program is safe, and your untyped module can safely call the function<br>
&gt;&gt; with any value it wants.<br>
&gt;<br>
&gt;<br>
&gt; In that case, my program can only work with values of type Any, and I&#39;d need<br>
&gt; to make all functions Any -&gt; (T Any) since I can&#39;t downcast to any other<br>
&gt; type, but since I&#39;m passing functions as arguments I will have the problem<br>
&gt; of subtyping between functions...<br>
&gt;<br>
&gt;&gt; As an additional note, the `CAST&#39; operation you describe below, can&#39;t<br>
&gt;&gt; do exactly what you expect, because it&#39;s runtime semantics depends on<br>
&gt;&gt; how you instantiate `B&#39;.  But that would mean that you&#39;d have to<br>
&gt;&gt; generate code for the `CAST&#39; without knowing what `B&#39; is.<br>
&gt;<br>
&gt;<br>
&gt; do you think it can work if I do (CAST f (Integer -&gt; Boolean)) instead?<br>
<br>
</div></div>Yes, this could work.  I haven&#39;t added `cast&#39; yet, but I&#39;ll try to do that soon.<br>
<div class="im"><br>
&gt; Maybe the flaw in my reasoning is that I think that when you evaluate the<br>
&gt; polymorphic function, then you know what A and B are... so you should be<br>
&gt; able to cast a value to B, is not that so?<br>
&gt;<br>
&gt; is it that you statically prove that the body is OK for all A and B and then<br>
&gt; you don&#39;t get that information when applying??<br>
<br>
</div>Yes, this latter description is how Typed Racket works.<br>
<div class="im"><br>
&gt;&gt;<br>
&gt;&gt; Typed<br>
&gt;&gt; Racket, like ML or Haskell, doesn&#39;t pass type parameters around as<br>
&gt;&gt; values, so you can&#39;t do this.<br>
&gt;<br>
&gt;<br>
&gt; I don&#39;t know much about how the type system of ML or Haskell works.<br>
&gt;<br>
&gt; What I&#39;m trying to do, so you get the full picture, is to write a variation<br>
&gt; of Aspect Scheme in Typed Racket, so you can statically check that advice is<br>
&gt; well-typed. I couldn&#39;t type correctly the weaver function, so I tried with<br>
&gt; an untyped module. Maybe it is not possible at all??<br>
<br>
</div>That sounds neat.  However, I&#39;m suspicious that you won&#39;t be able to<br>
type check everything that people currently write in Aspect Scheme<br>
without changing some part of Typed Racket to understand your system<br>
better.<br></blockquote><div><br>It seems so... the biggest problem for now is that either I can&#39;t construct the woven function with the same type as the original one, or I can&#39;t apply it :-p (the problem at the origin of the thread)<br>
<br>I think the weaver should have type (All (A B) ((A -&gt; B) jp aspect-env -&gt; (A -&gt; B))) and that&#39;s what I&#39;ve been trying to do, unsuccesfully.<br><br>Any ideas for a reduced version that might work?<br><br>
I was thinking of using a union type with a certain subset of types, and then manually check one-by-one to produce the expected result.<br><br>Thanks<br clear="all"></div></div><br>-- <br>Ismael<br><br>