Got it. Thanks for taking the time to clarify it for me. Ray
On Fri, Nov 2, 2012 at 3:05 PM, Sam Tobin-Hochstadt <[email protected]>wrote: > On Fri, Nov 2, 2012 at 2:40 PM, Ray Racine <[email protected]> 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. > > (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 > [email protected] >
____________________ Racket Users list: http://lists.racket-lang.org/users
