У меня есть функция, которая вроде как assoc ищет символ в списке и возвращает либо #f, либо позицию в списке.
Тип возврата для этой функции должен быть объединением #f и Natural, (U #f Natural).
Но когда я хочу использовать значение как число, оно всегда будет вводить несоответствие, потому что значение не просто Natural, а фактически является объединением.
Как я могу извлечь значение Natural и избежать ошибки несоответствия типов?
Typed Racket имеет функцию под названием Occurrence Typing, которая позволяет вам фильтровать тип значения с помощью предикатов и утверждений. Основная идея состоит в том, что предикаты, такие как string?, empty? и number?, могут фильтровать типы на основе потока управления программы.
Чтобы проиллюстрировать это, посмотрите этот пример:
(: nat/#f->nat ((U Natural False) -> Natural))
(define (nat/#f->nat n)
(if n n
(error "Expected a number, given " n)))
Это будет проверка типа, потому что, если будет взята первая ветвь, тогда n не может быть #f, поэтому это должно быть Natural. Во втором случае функция просто выдает ошибку и не возвращает, поэтому тип все еще сохраняется.
В большинстве случаев вы не просто ошибетесь в случае сбоя, но вы предоставите какое-то альтернативное поведение. Это по-прежнему позволяет вам уточнить тип внутри самого тела.
(define n : (Option Natural) #f)
(cond
[n
; do something with n as a number
(+ n 1)]
[else
; do something else
(void)])
В теле первого случая тип n уточняется до Natural, поэтому его можно использовать как таковой.
В случае, если вы действительно действительно хотите просто выдать ошибку, когда тип не совпадает, вы можете использовать _ 11_ или _ 12_. Первый - это фактически производная концепция, которая в основном выполняет те же проверки, что и в первом примере выше. Вы используете это так:
(assert n number?) ; now n is a number, and if it isn't, an error is thrown
(+ n 1)
Форма cast немного отличается, поскольку она определяет типы вместо предикатов. Это означает, что вы можете использовать его так:
(+ (cast n Natural) 1)
Это также вызывает ошибку, если оказывается, что n на самом деле не Natural, но в противном случае общее выражение становится типа Natural.
Сделайте что-нибудь вроде этого:
(define i (assoc ...))
(cond
[i <use-i-here>]
[else <raise-error>])
Из (define i (assoc ...)) мы знаем, что i имеет тип возвращаемого значения assoc, то есть либо #f, либо естественный. В предложении cond [i <use-i-here>] <use-i-here> будет оцениваться только в том случае, если i не #f, поэтому проверяющий тип знает, что в <use-i-here> i будет естественным.
