Re: [racket-users] How to refine types when filtering values

2018-12-24 Thread Alex Knauth
> On Dec 24, 2018, at 4:34 PM, wanderley.guimar...@gmail.com wrote: > > I am trying typed/racket for the first time and I can't figure out how to > refine a (Listof (U Positive-Byte False)) to (Listof Positive-Byte). > > For example > > (filter identity '(1 2 3)) > - : (Listof Positive-Byte)

Re: [racket-users] How to refine types when filtering values

2018-12-24 Thread wanderley.guimar...@gmail.com
Thanks for the fast response. "Instantiate the type of e with types t" in the documentation was crypt to me. The examples helped to clarify that if you have generic types A and B in a type `(All (A B) A -> B)`, then the instantiate the type `(A -> B)` with `(U Number False) Number)` means that

Re: [racket-users] How to refine types when filtering values

2018-12-24 Thread Matthias Felleisen
> #lang typed/racket > > (define-type MaybePB (U Positive-Byte False)) > > (: f ( [Listof MaybePB] -> [Listof Positive-Byte])) > (define (f x) > ((inst filter MaybePB Positive-Byte) number? x)) > > (f '(1 #false)) -- You received this message because you are subscribed to the Google

[racket-users] How to refine types when filtering values

2018-12-24 Thread wanderley.guimar...@gmail.com
I am trying typed/racket for the first time and I can't figure out how to refine a (Listof (U Positive-Byte False)) to (Listof Positive-Byte). For example > (filter identity '(1 2 3)) - : (Listof Positive-Byte) '(1 2 3) > (filter identity '(1 2 3 #f)) - : (Listof (U False Positive-Byte)) '(1 2 3)