# Narrowing a string

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

A `string` alternative is the bare kind, every string, or `{:string, set}`: a `Feel.Type.StringSet` (D-39). A set is one of three things, and the analyzer keeps the simplest:

| Written | Is |
| --- | --- |
| `string = "a"`, `string in {"a", "b"}` | exactly those strings (up to 64) |
| `string in ["a".."m"]`, `string in (.."m")`, `string in ("m"..)` | an interval of strings, in the order of the run; `..` is "no bound" |
| `string except "a"`, `string in (.."a"], ["m"..) except "a", "m"` | every string (or those of the intervals) but the ones left out |

Within the representation budget, string comparisons can keep intervals and excluded points, including ties. Oversized finite sets lose precision. See the common [correctness obligations](../narrowing.md#10-correctness-obligations-and-checks) before treating composed facts as proofs.

## Comparisons with a string

| Condition | `s` when true | `s` when not true |
| --- | --- | --- |
| `s = "a"` | `string = "a"` | `string except "a" \| Null` |
| `s != "a"` | `string except "a" \| Null` | `string = "a"` |
| `s < "m"` | `string in (.."m")` | `string in ["m"..) \| Null` |
| `s <= "m"` | `string in (.."m"]` | `string in ["m"..) except "m" \| Null` |
| `s > "m"` | `string in ("m"..)` | `string in (.."m"] \| Null` |
| `s >= "m"` | `string in ["m"..)` | `string in (.."m"] except "m" \| Null` |

The `null` rules are those of the other kinds: an ordering of `null` is `null`, so a true ordering excludes it and a not-true one keeps `Null`; `s != "a"` is true for `null` ([null.md](null.md)).

### Why `<=` and `>=` have an `except`

The order of the run (`Feel.Runtime.Compare`) is by code point, a prefix first, with a trailing `U+0000` left out of the comparison. That order is not total: `"m"` and `"m\u0000"` are neither below nor above one another, and they are not equal. The strings with the same key, `"m"`, `"m\u0000"`, `"m\u0000\u0000"`, are a **class**, and an interval consists of whole classes. So `s <= "m"` is true for the strings below the class of `"m"`, and for `"m"` itself, **but not** for the other strings of its class. When it is not true, the values left are the whole class and above, without `"m"`: `string in ["m"..) except "m"`. The same holds, mirrored, for `>=`. For almost every use you can read an interval as an interval and an `except` as "and not that one".

## `in`, `and` and `or`

A list of values or ranges is joined in `then` and met in `else`, as for numbers ([number](number.md#between-and-in)).

| Condition | `s` when true | `s` when not true |
| --- | --- | --- |
| `s in ("a", "b")` | `string in {"a", "b"}` | `string except "a", "b" \| Null` |
| `s in ["a".."m"]` | `string in ["a".."m"]` | `string in (.."a"], ["m"..) except "a", "m" \| Null` |
| `s = "a" or s = "b"` | `string in {"a", "b"}` | `string except "a", "b" \| Null` |
| `s in ("a", "b", "c") and s != "b"` | `string in {"a", "c"}` | `string except "a", "c" \| Null` |
| `s > "a" and s < "m"` | `string in ("a".."m")` | `string in (.."a"], ["m"..) \| Null` |

## The other side is not a constant

The other side is read as the set of strings it can be. A name, whose set is not known, gives nothing for equality and little for an ordering. As for numbers, when the other side can be `null` or its kind is not known, `else` learns nothing.

| Condition | `s` when true | `s` when not true |
| --- | --- | --- |
| `s = s2` | `string \| Null` | `string \| Null` |
| `s < s2` | `string` | `string \| Null` |
| `s = v` | `string \| Null` | `string \| Null` |

`s = s2` can be true when both are `null`. `s < s2` is not true for a `null`, so `s` is a string.

## A function of the string

A comparison of a call of a function of strings with a value is not true of a `null`, so in `then` the arguments are of the kinds for which the call gives a value of the kind the other side has (D-170; `Feel.Analysis.Images` says what a call gives). `string length(s) > 3` is not true of a `null`, so `s` is a string. For the length of a string the comparison says more: it is true of the empty string (a length of 0) or of the others, and the others are one set (`StringSet` has no set of the strings of a length), so `string length(s) > 0` leaves every string except `""`, and `string length(s) = 0` leaves `""`.

| Condition | `s` when true | `s` when not true |
| --- | --- | --- |
| `string length(s) > 0` | `string except ""` | `string = "" \| Null` |
| `string length(s) >= 1` | `string except ""` | `string = "" \| Null` |
| `string length(s) != 0` | `string except "" \| Null` | `string = ""` |
| `string length(s) = 0` | `string = ""` | `string except "" \| Null` |
| `string length(s) < 1` | `string = ""` | `string except "" \| Null` |
| `string length(s) > 3` | `string except ""` | `string \| Null` |
| `string length(s) < 3` | `string` | `string except "" \| Null` |
| `upper case(s) = "ABC"` | `string` | `string \| Null` |
| `contains(s, "a") = true` | `string` | `string \| Null` |
| `string length(s) > -1` | `string` | `string \| Null` |

The function gives a value for the strings and for a list of one string. `s` here is a string: for a name that is `Any`, `string length(v) > 0` leaves the strings except `""`, and the lists.

| Condition | `v` when true | `v` when not true |
| --- | --- | --- |
| `string length(v) > 0` | `string except "" \| list<Any \| Null>` | `Any \| Null` |
| `string length(v) = 0` | `string = "" \| list<Any \| Null>` | `Any \| Null` |

## `instance of`

| Condition | `s` when true | `s` when not true |
| --- | --- | --- |
| `s instance of string` | `string` | `Null` |
| `s instance of number` | — | `string \| Null` |

## Limits

- A set of more than **64 strings** is every string: `s = "a1" or s = "a2" or … or s = "a64"` keeps the 64, and a 65th makes it `string`.
- A set of strings with intervals keeps its single strings next to the intervals and the ones left out of them; there is no cap on those.
- A concatenation of sets that have intervals or exceptions (`s + "!"`) is not kept: the result is the bare kind. [todo.md](../todo.md) lists it as still open.

See also: [number](number.md), [null](null.md), [Any](any.md); `Feel.Type.StringSet` has the algebra ([type-system.md](../type-system.md), 3.3).
