# Narrowing a date

[Narrowing](../narrowing.md) › date. The names in the examples are those of [section 2](../narrowing.md#2-the-names-in-the-examples).

A `date` alternative is the bare kind, every date from `-999999999-01-01` to `999999999-12-31`, or `{:date, set}`: a `Feel.Type.NumberSet` of the **image** of the dates, their number of days in the proleptic Gregorian calendar (`Feel.Type.Image`, D-109). A date is ordered as that number is, so a comparison is read exactly as a number's is, with the image of the other side (D-109). Days are whole numbers, so two sets of dates that follow one another are one (`[2020-01-01..2020-01-05]` and `[2020-01-06..2020-01-09]` are `[2020-01-01..2020-01-09]`, `Feel.Type.NumberSet.join_whole_neighbours/1`): the join of the two branches of an `if` that split the calendar at a day is `date`, not the pieces. A date is not a date and time: they are of different kinds, so each is left only by its own.

## Comparisons

| Condition | `d` when true | `d` when not true |
| --- | --- | --- |
| `d < @"2024-01-01"` | `date in [-999999999-01-01..2024-01-01)` | `date in [2024-01-01..999999999-12-31] \| Null` |
| `d >= @"2024-01-01"` | `date in [2024-01-01..999999999-12-31]` | `date in [-999999999-01-01..2024-01-01) \| Null` |
| `d = @"2024-01-31"` | `date = 2024-01-31` | `date in [-999999999-01-01..2024-01-31), (2024-01-31..999999999-12-31] \| Null` |
| `d != @"2024-01-31"` | `date in [-999999999-01-01..2024-01-31), (2024-01-31..999999999-12-31] \| Null` | `date = 2024-01-31` |
| `d between @"2024-01-01" and @"2024-12-31"` | `date in [2024-01-01..2024-12-31]` | `date in [-999999999-01-01..2024-01-01), (2024-12-31..999999999-12-31] \| Null` |
| `d in [@"2024-01-01"..@"2024-03-31"]` | `date in [2024-01-01..2024-03-31]` | `date in [-999999999-01-01..2024-01-01), (2024-03-31..999999999-12-31] \| Null` |
| `d < dt` | — | `date \| Null` |
| `d = dt` | `Null` | `date \| Null` |
| `d instance of date` | `date` | `Null` |
| `d instance of date and time` | — | `date \| Null` |

The `null` rules are those of every kind ([the rule](../narrowing.md#4-then-else-and-null)). `d < dt` compares kinds that have no order between them, so it is never true; `d = dt` is only true when both are `null`.

## Properties of a date

A fact about `d.year`, `d.month`, `d.day` or `d.weekday` (Table 67) is a fact about `d` too: the days of its set whose property is what the fact leaves (D-194). The year does not decrease with the day, so it leaves **one** interval; the month, the day and the weekday come back every year or week, so they leave **a piece for each**.

A set of days is kept in at most **16 pieces**, and the properties are applied in the order that leaves the fewest: the year (and `value`), then the month, then the day of the month, then the weekday, each on what the one before left.

So a property narrows the date only as far as the date's set is bounded. A bare date has the whole calendar, and `d.month > 6` would need a piece for each of two billion years, so it narrows nothing:

| Condition | `d` when true | `d` when not true |
| --- | --- | --- |
| `d.year = 2024` | `date in [2024-01-01..2024-12-31]` | `date in [-999999999-01-01..2023-12-31], [2025-01-01..999999999-12-31] \| Null` |
| `d.year >= 2020 and d.year <= 2022` | `date in [2020-01-01..2022-12-31]` | `date in [-999999999-01-01..2019-12-31], [2023-01-01..999999999-12-31] \| Null` |
| `d.year = 2024 and d.month = 2` | `date in [2024-02-01..2024-02-29]` | `date \| Null` |
| `d.year = 2024 and d < @"2024-03-01"` | `date in [2024-01-01..2024-02-29]` | `date \| Null` |
| `d.month > 6` | `date` | `date \| Null` |
| `d.month = 2 and d.day = 29` | `date` | `date \| Null` |
| `d.month > 12` | — | `date \| Null` |

The last row: there is no such month, and the condition cannot be true.

When the date is **bounded**, by allowed values or by a condition before, the months and days have pieces to keep (`dr` is a date in `[2020-01-01..2022-12-31]`):

| Condition | `dr` when true | `dr` when not true |
| --- | --- | --- |
| `dr.month > 6` | `date in [2020-07-01..2020-12-31], [2021-07-01..2021-12-31], [2022-07-01..2022-12-31]` | `date in [2020-01-01..2020-06-30], [2021-01-01..2021-06-30], [2022-01-01..2022-06-30] \| Null` |
| `dr.month = 2 and dr.day = 29` | `date = 2020-02-29` | `date in [2020-01-01..2022-12-31] \| Null` |
| `dr.year = 2021` | `date in [2021-01-01..2021-12-31]` | `date in [2020-01-01..2020-12-31], [2022-01-01..2022-12-31] \| Null` |
| `dr.year = 2021 and dr.month >= 11` | `date in [2021-11-01..2021-12-31]` | `date in [2020-01-01..2022-12-31] \| Null` |
| `dr.weekday = 7` | `date in [2020-01-05..2022-12-25]` | `date in [2020-01-01..2022-12-31] \| Null` |
| `dr.month > 12` | — | `date in [2020-01-01..2022-12-31] \| Null` |
| `dr < @"2021-01-01"` | `date in [2020-01-01..2021-01-01)` | `date in [2021-01-01..2022-12-31] \| Null` |

- `dr.month = 2 and dr.day = 29` is the one day of the leap years in the set: February first (three pieces of the months in range), then the 29th of those. Taking the day first would make a piece for each month.
- `dr.weekday = 7` has more than 16 Sundays in the set, so the pieces are replaced by the one interval from the first to the last: a superset, and the best a set of 16 can say.
- **The `else` of an `and` narrows nothing** unless both sides do ([and and or](../narrowing.md#5-and-and-or)), which is why the not-true column of a conjunction is mostly the whole set.

The property itself is a subject too (`d.year > 2000` is about `d.year`, a number):

| Condition | `d.year` when true | `d.year` when not true |
| --- | --- | --- |
| `d.year > 2000` | `number in [2001..999999999]` | `number in [-999999999..2000] \| Null` |

The sets of the properties are exact for `year`, `month`, `day` and `weekday` while the pieces fit (`Feel.Analysis.DateProperties`): each number in them is the property of some day of the set. `value`, the seconds since 1970 of midnight UTC, is a larger set than the days give.

## A function of the date (D-170)

`day of week(d) = "Monday"` is not true of a `null`, so `d` is a date (or a date and time, the day of the clock of which it reads). The days of the week are not a set of days, so nothing more is said.

| Condition | `d` when true | `d` when not true |
| --- | --- | --- |
| `day of week(d) = "Monday"` | `date` | `date \| Null` |
| `month of year(d) != "May"` | `date \| Null` | `date \| Null` |
| `day of year(d) > 100` | `date` | `date \| Null` |

## Date arithmetic in a comparison

A date plus or minus a duration, or the difference of two dates, in a comparison, narrows the operands as an arithmetic operation does ([number](number.md#operations-in-the-comparison)): the date is not `null`, and is one of those that give such a result. The day of the month is clamped (`2024-01-31 + P1M` is `2024-02-29`), so the sets come from `Feel.Analysis.DateArithmetic` and not from adding images. A duration that is not a constant gives no set.

| Condition | `d` when true | `d` when not true |
| --- | --- | --- |
| `d + @"P1D" > @"2024-01-01"` | `date in [2024-01-01..999999999-12-30]` | `date in [-999999999-01-01..2023-12-31], 999999999-12-31 \| Null` |
| `d - @"P1D" < @"2024-01-01"` | `date in [-999999999-01-02..2024-01-01]` | `date in -999999999-01-01, [2024-01-02..999999999-12-31] \| Null` |
| `d + @"P1M" > @"2024-02-29"` | `date in [2024-02-01..999999999-11-30]` | `date in [-999999999-01-01..2024-01-31], [999999999-01-01..999999999-12-31] \| Null` |
| `d - @"2024-01-01" > @"P10D"` | `date in [2024-01-12..999999999-12-31]` | `date in [-999999999-01-01..2024-01-11] \| Null` |
| `d + dd > @"2024-01-01"` | `date` | `date \| Null` |

The ends at the edge of the calendar (`999999999-12-30`, `-999999999-01-02`) are where adding or subtracting the duration would leave the calendar, and the result would be `null`. As for numbers, the `else` branch is the dates the comparison is `false` for and the dates for which the operation is `null` ([number](number.md#operations-in-the-comparison)): the difference of two dates is a duration that can be written, and the sum of a date and a duration can leave the calendar, which `Feel.Analysis.Failure` gives:

* **A duration of days and time** moves a date by the whole days of its seconds, rounded down, so the dates in the set are those within the days of the duration from its end (`d + @"P1D"` for the last day, `d - @"P1D"` for the first).
* **A duration of years and months** moves the year by the months over twelve, rounded up, so the dates in the set are those of the years that the greatest number of months can leave past the calendar: the year of `d + @"P1M"` that is the last, all of it, where only December leaves (the set is wider than the dates the run gives `null` for).
* **A duration that is not a constant** has as many days or months as the type of it says, and a type that has no bound gives every date, so the `else` says nothing (`d + dd`).

## Limits

- **16 pieces** of days; past it a property leaves the set as it was (a longer interval has every month, every day of a month and every weekday).
- A property of an interval with **no whole day** in it (`(2020-01-01..2020-01-02)`) says nothing.

See also: [time](time.md), [date and time](date-and-time.md), [years and months duration](years-and-months-duration.md), [days and time duration](days-and-time-duration.md); [type-system.md](../type-system.md), 3.3.