[racket] TR Parameterization Question

From: Ray Racine (ray.racine at gmail.com)
Date: Fri Nov 2 14:40:20 EDT 2012

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.

#lang typed/racket/base

(struct: (T) S0 ([v : (Sequenceof T)]))

(struct: (T V) S1 ([x : (S T V)]
                   [f : (T -> Boolean)]))

(struct: (T V) S2 ([x : (S T V)]
                   [f : (T -> V)]))

(define-type (S T V) (U (S0 T) (S1 T V) (S2 T V)))

(define: s0 : (S0 String) (S0 '("hello" "big" "world")))

(define: s1 : (S1 String Nothing) (S1 s0 (λ: ((s : String)) (>
(string-length s) 4))))

(define: s2 : (S2 String Symbol) (S2 s0 (λ: ((s : String)) (string->symbol
s))))

(define: cvt : (String -> Symbol) (S2-f s2))

;;===================================================

;(struct: (T) S0 ([v : (Sequenceof T)]))
;
;(struct: (T) S1 ([x : (S T)]
;                 [f : (T -> Boolean)]))
;
;(struct: (T) S2 ([x : (S T)]
;                 [f : (All (V) T -> V)]))
;
;(define-type (S T) (U (S0 T) (S1 T) (S2 T)))
;
;(define: s0 : (S0 String) (S0 '("hello" "world")))
;
;(define: s1 : (S1 String) ((inst S1 String) s0 (λ: ((s : String)) (>
(string-length s) 3))))
;
;(define: s2 : (S2 String) ((inst S2 String) s0 (λ: ((s : String))
(string->symbol s))))
;
;(define: cvt : (String -> Symbol) (S2-f s2))
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20121102/25c862cd/attachment.html>

Posted on the users mailing list.