I meant `require/typed` obviously, not `require-typed`. On Saturday, December 7, 2019 at 11:17:00 AM UTC+1, Marc Kaufmann wrote: > > Thanks Ben and Jon, that did the trick. > > I realized when following the code that the structure wasn't exported - > but I didn't know how to work around that. I now also checked the > documentation, and the only thing I found on opaque types is > https://docs.racket-lang.org/ts-reference/special-forms.html?q=opaque#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._require%2Ftyped%29%29. > > What it says about opaque types is: > > "Opaque types must be required lexically before they are used." > > followed by an example that is even now non-trivial for me to parse and > figure out. (I started going down the rabbit hole when the `->` was not > used in the first position of the definition, nor written as `. -> .` Turns > out types can be defined via infix notation, which is nice but unexpected.) > > So there are two questions: > > 1. What does #:opaque do? > 2. How could I have found that out by searching - or essentially the way > to do it was "Email the list". If the latter, that's fine, the email list > is very helpful and it would be good to add some additional explanation of > opaque types to the documentation of `require-typed`, and possibly even to > the typed racket reference. Probably the part talking about typed-racket > untyped racket interaction. > > Let me try answering my first question: #:opaque defines a new type via a > predicate function -- here `time?` -- that is being imported (can I use it > without require-typed? I guess there would be no point, but I haven't > thought this through). This is not based on the usual type constructors > using other types, but based on whether a thing returns `#true` when passed > to the predicate, in my case `time?`. I assume this means that the type is > verified via contracts, so if I do this a lot I should expect some run-time > performance hits (if I call this function a bunch, which isn't an issue in > my case). > > Cheers, > Marc > > On Wednesday, December 4, 2019 at 6:26:47 PM UTC+1, Jon Zeppieri wrote: >> >> On Tue, Dec 3, 2019 at 8:55 PM Ben Greenman <benjamin...@gmail.com> >> wrote: >> > >> > The error is because gregor/time doesn't export a struct. But >> > nevermind that, because you're probably best off with an opaque type: >> > >> > ``` >> > #lang typed/racket >> > >> > (require/typed gregor/time >> > [#:opaque Time time?] >> > [time (->* [Integer] [Integer Integer Integer] Time)] >> > [time->iso8601 (-> Time String)]) >> > >> > (require/typed gregor >> > [current-time (->* [] [#:tz String] Time)]) >> > >> > (time->iso8601 (current-time)) >> > ;; "21:04:25.687808105" >> > ``` >> >> Also, most operations on the date/time data structures are generic, >> which makes it a bit more complicated to use with typed racket. The >> generic predicates, like `time-provider?`, should probably map to >> union types, like so (though people like Ben, who are more savvy about >> typed racket, might have other ideas): >> >> ``` >> #lang typed/racket >> >> (require/typed gregor/time >> [#:opaque Time time?] >> [time (->* [Integer] [Integer Integer Integer] Time)] >> [time->iso8601 (-> Time String)]) >> >> (require/typed gregor >> [#:opaque Datetime datetime?] >> [datetime (->* [Integer] [Integer Integer Integer >> Integer Integer Integer] Datetime)]) >> >> (define-type Time-Provider (U Time Datetime)) >> >> (require/typed gregor >> [current-time (->* [] [#:tz String] Time)] >> [->hours (-> Time-Provider Integer)]) >> >> (time->iso8601 (current-time)) >> (->hours (current-time)) >> ``` >> >> Also, if you want to be more specific with your types: >> ``` >> #lang typed/racket #:with-refinements >> >> (define-type Hour (Refine [n : Integer] (and (>= n 0) (< n 24)))) >> (define-type Minute (Refine [n : Integer] (and (>= n 0) (< n 60)))) >> (define-type Second (Refine [n : Integer] (and (>= n 0) (< n 60)))) >> (define-type Nanosecond (Refine [n : Integer] (and (>= n 0) (< n >> 1000000000)))) >> >> (require/typed >> gregor/time >> [#:opaque Time time?] >> [time (->* [Hour] [Minute Second Nanosecond] Time)]) >> ``` >> ... though this might make the proof obligations too onerous, >> depending on how you're using the library. >> >> - Jon >> >
-- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/10a47274-6a9c-4cc6-b554-05a286531f9f%40googlegroups.com.
