Got it.  Thanks for taking the time to clarify it for me.<div><br></div><div>Ray</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Nov 2, 2012 at 3:05 PM, Sam Tobin-Hochstadt <span dir="ltr">&lt;<a href="mailto:samth@ccs.neu.edu" target="_blank">samth@ccs.neu.edu</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Fri, Nov 2, 2012 at 2:40 PM, Ray Racine &lt;<a href="mailto:ray.racine@gmail.com">ray.racine@gmail.com</a>&gt; wrote:<br>

&gt; The immediate below works for me.  It nags in the sense that S1 has a<br>
&gt; irrelevant type parameter.<br>
&gt; Below I attempt to shift the type parameter inside, which the TR parse<br>
&gt; happily allows.  However, later things fall apart.<br>
&gt;<br>
&gt; One interpretation of what I&#39;m tying to do is: S0 encodes a Collection of T,<br>
&gt; S1 encodes a filter of a Collection of T and S2 encodes a mapping of a<br>
&gt; Collection of T to a Collection of V.<br>
&gt;<br>
&gt; Roughly supports a running of a combinations of S as follows:<br>
&gt; (applyS (applyS s0 s1) s2) ==&gt; &#39;(hello world)<br>
&gt;<br>
&gt; So which of the following are correct statements.<br>
&gt; 1) In the below, the parameterization of f in S2 should give a syntax error.<br>
&gt; 2) In the below, it should work but there is a TR bug or I&#39;m doing it wrong<br>
&gt; etc.<br>
&gt; 3) In the below, the S2 definition and parameterization of f is<br>
&gt; syntactically fine but it doesn&#39;t mean what I think it means.<br>
&gt; 4) In the above, there is a way to do the above and avoid the use of the<br>
&gt; dummy Nothing in S1.<br>
<br>
</div>(3) is the correct answer. Moving the quantification inside the type<br>
of the `f` field means something very different from &quot;omitting&quot; the<br>
extra type parameter.  Instead, (All (V) (T -&gt; V)) means that each<br>
`S2` must have an `f` that can produce any `V` that its consumer might<br>
want.  Since the definer of the function can&#39;t know what `V` the user<br>
will pick, it can&#39;t return anything at all, and must error or loop<br>
forever.<br>
<br>
The uncommented code that you wrote is correct here. Another way to<br>
think about this is to write down the data type in Haskell.<br>
<br>
data S t v = S0 [t] | S1 (S t v) (t -&gt; Boolean) | S2 (S t v) (t -&gt; v)<br>
<br>
This corresponds exactly to what you wrote, complete with extra type<br>
parameters for S1:<br>
<br>
Prelude&gt; :t S1<br>
S1 :: S t v -&gt; (t -&gt; Bool) -&gt; S t v<br>
<br>
Typed Racket has you specify these separately, and it fills in a type<br>
for `V` earlier than Haskell does, but here it fills in the most<br>
useful type, `Nothing`, which can be put in any context.<br>
--<br>
sam th<br>
<a href="mailto:samth@ccs.neu.edu">samth@ccs.neu.edu</a><br>
</blockquote></div><br></div>