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