[racket] TR Parameterization Question

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 <samth at ccs.neu.edu>wrote:

> On Fri, Nov 2, 2012 at 2:40 PM, Ray Racine <ray.racine at gmail.com> 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
> samth at ccs.neu.edu
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20121102/baac5166/attachment.html>