<div>The immediate below works for me. It nags in the sense that S1 has a irrelevant type parameter.</div><div>Below I attempt to shift the type parameter inside, which the TR parse happily allows. However, later things fall apart.</div>
<div><br></div><div>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.</div><div><br>
</div><div>Roughly supports a running of a combinations of S as follows:</div><div>(applyS (applyS s0 s1) s2) ==> '(hello world)</div><div><br></div><div>So which of the following are correct statements.</div><div>
1) In the below, the parameterization of f in S2 should give a syntax error.</div><div>2) In the below, it should work but there is a TR bug or I'm doing it wrong etc.</div><div>3) In the below, the S2 definition and parameterization of f is syntactically fine but it doesn't mean what I think it means.</div>
<div>4) In the above, there is a way to do the above and avoid the use of the dummy Nothing in S1.</div><div><br></div><div>#lang typed/racket/base</div><div><br></div><div>(struct: (T) S0 ([v : (Sequenceof T)]))</div><div>
<br></div><div>(struct: (T V) S1 ([x : (S T V)]</div><div> [f : (T -> Boolean)]))</div><div><br></div><div>(struct: (T V) S2 ([x : (S T V)]</div><div> [f : (T -> V)]))</div><div><br>
</div><div>(define-type (S T V) (U (S0 T) (S1 T V) (S2 T V)))</div><div><br></div><div>(define: s0 : (S0 String) (S0 '("hello" "big" "world")))</div><div><br></div><div>(define: s1 : (S1 String Nothing) (S1 s0 (ė: ((s : String)) (> (string-length s) 4))))</div>
<div><br></div><div>(define: s2 : (S2 String Symbol) (S2 s0 (ė: ((s : String)) (string->symbol s))))</div><div><br></div><div>(define: cvt : (String -> Symbol) (S2-f s2))</div><div><br></div><div>;;===================================================</div>
<div> </div><div>;(struct: (T) S0 ([v : (Sequenceof T)]))</div><div>;</div><div>;(struct: (T) S1 ([x : (S T)]</div><div>; [f : (T -> Boolean)]))</div><div>;</div><div>;(struct: (T) S2 ([x : (S T)]</div>
<div>; [f : (All (V) T -> V)]))</div><div>;</div><div>;(define-type (S T) (U (S0 T) (S1 T) (S2 T)))</div><div>;</div><div>;(define: s0 : (S0 String) (S0 '("hello" "world")))</div>
<div>;</div><div>;(define: s1 : (S1 String) ((inst S1 String) s0 (ė: ((s : String)) (> (string-length s) 3))))</div><div>;</div><div>;(define: s2 : (S2 String) ((inst S2 String) s0 (ė: ((s : String)) (string->symbol s))))</div>
<div>;</div><div>;(define: cvt : (String -> Symbol) (S2-f s2))</div><div><br></div>