On Tue, Dec 3, 2019 at 8:55 PM Ben Greenman <benjaminlgreen...@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/CAKfDxxzq0S6-fzMA%3D%2BVfdxH7ZBqkDFO%2BUHt_Nabj%3DOipP%3DMMwQ%40mail.gmail.com.
