[racket] TR Parameterization Question

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