How to use dates (especially gregor) with Typed Racket?

[Marc Kaufmann]

Hi,

this is hopefully easier, but I can't figure out how to `(require/typed gregor)` inside a typed racket file. Here are my failed attempts (I want time to work, hence I try to import gregor/time):

```

#lang typed/racket

; Try to get time struct from gregor/time
(require/typed gregor/time
               [#:struct time ([hour : Integer]
                               [minute : Integer]
                               [second : Integer]
                               [nanosecond : Integer])])

; This just checks that the time structure isn't in gregor
(require/typed gregor
               [#:struct time ([hour : Integer]
                               [minute : Integer]
                               [second : Integer]
                               [nanosecond : Integer])]
               [current-time (->* () (#:tz String) time)])

```

These fail with errors of the kind

"

only-in: identifier `struct:time' not included in nested require spec

at: gregor

in: (only-in gregor struct:time (time time2))

"

So, maybe I am wrong to think that time is a struct. But when I print one in the REPL, it says #<time ...>, which I thought would mean it's a struct.

My next step was to check the type of it in the REPL with typed racket... but that doesn't work since requiring gregor in a REPL with typed/racket leads to the same errors (obviously, since how would it know anything more...).

Hence, I fire up DrRacket, following the trail to the definition of the time structure and I find that the structure itself is never provided out, but only used to define the function `time?` and others. But that makes me wonder: how can I define the type for time so that I can use gregor inside typed/racket if I can't import the structure (which in my understanding defines the type of time)? I can't figure out what thing `(current-time)` is, apparently  `(struct Time (hms ns) ...)` but I don't see any contracts on hms or ns to figure out what they are... but even if I did, would I define my own structure `(struct my-time ([hms : HMS] [ns : NS])` and use that?

Cheers,

Marc

PS: If any Vim users our there can tell me how to jump to definitions of required libraries I'd be ever so happy.

[Ben Greenman]

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"
```

[Jon Zeppieri]

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

[Marc Kaufmann]

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

[Marc Kaufmann]

I meant `require/typed` obviously, not `require-typed`.

[Ben Greenman]

On 12/7/19, Marc Kaufmann <marc.ka...@gmail.com> 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."

The docs says a little more --- there are 4 sentences that come right
before this one.

I think those sentences would be better off with:
1. a link to `make-predicate`
2. and English words at the start & end of each sentence

Let me know if you have other suggestions

> 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.)

The docs for -> show the infix notation.

Is the example still difficult to figure out? We could replace it, but
I'm not sure what could be better

(if want to stop using infix notation here, then the other uses on the
same page need to change too)

>
> 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).

Right, a `Time` is any value that `time?` says yes to.

About performance: in type-checked code, you can expect to pay for
every call to `time?` and nothing else. The run-time hit should be the
same as using cond/if with any simple predicate.

[Marc Kaufmann]

On Saturday, December 7, 2019 at 3:04:25 PM UTC+1, Ben Greenman wrote:

On 12/7/19, Marc Kaufmann <marc.ka...@gmail.com> 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."

The docs says a little more --- there are 4 sentences that come right
before this one.

I think those sentences would be better off with:
1. a link to `make-predicate`
2. and English words at the start & end of each sentence

Let me know if you have other suggestions

So here is the paragraph:

> The fourth case defines a new type t. pred, imported from module m, is a predicate for this type. The type is defined as precisely those values to which pred produces #t. pred must have type (Any -> Boolean). Opaque types must be required lexically before they are used.

When I came to the documentation, I was skimming, in part because I didn't know whether this would be helpful or not. I am not a fan of the "The first/second/... case..." when there are many cases and I can no longer see what the cases were - and in fact I miscounted the rows, so I thought this applied to something else for a while. Or rather, I like it, but only if it is

"The fourth case defines a new *opaque* type t. ..."

When I got to the last sentence starting with 'Opaque types...', I had to think again to realize this is the fourth case talked about - even though no one at any point talked about opaque types, so I was wondering where I'd missed them.

Second sentence "This type t is defined via the predicate `pred`, imported from module m. More precisely, it is defined as precisely ... .

> 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.)

The docs for -> show the infix notation.

Yeah, I followed that and therefore realized that it was infix notation. Just to explain why I said it, even though I do *not* think that this particular instance should get changed: The point I was making is that for someone like me who doesn't live and breathe Racket, any extra layer of abstraction that isn't the same everywhere is extra cognitive load. Imagine me replacing every few words by a French word. I guess the fact that Racket contracts and Typed Racket don't use exactly the same notation is just a (very minor) nuisance. And I realize that it is incredibly hard to write helpful and clear documentation, so I'm not saying that I'd do a better job.

I only very recently started to be able to read and understand the Racket reference, while before I skipped all the arrow bits (and hence higher-order functions) and used the examples to reverse-engineer what form the arguments must take. That means that often I can't figure out what I need from the reference even when it's there.

Is the example still difficult to figure out? We could replace it, but
I'm not sure what could be better

I think what I'd suggest is to add an example with #:opaque to the Typed Racket Guide, part 6 (https://docs.racket-lang.org/ts-guide/typed-untyped-interaction.html).

(if want to stop using infix notation here, then the other uses on the
same page need to change too)

No, I think it's fine.

>
> 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).

Right, a `Time` is any value that `time?` says yes to.

About performance: in type-checked code, you can expect to pay for
every call to `time?` and nothing else. The run-time hit should be the
same as using cond/if with any simple predicate.

Great. Thanks a lot Ben.

Cheers,
Marc

[Ben Greenman]

Thanks for the feedback! I opened a pull request for the docs:

https://github.com/racket/typed-racket/pull/886

Happy to continue the discussion over there.
(The example I added to the guide is maybe too simple.)