从Typed Racket union中提取类型

Question

我有一个函数,有点像assoc,搜索列表中的符号并返回列表中的任一个#f或位置.

这个函数的返回类型应该是工会#f和Natural,(U #f Natural).

但是当我想将该值用作数字时,它总是会输入不匹配,因为该值不仅仅是自然值,而且实际上是一个联合.

如何将Natural值拉出并避免类型不匹配错误？

Answer 1

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,所以它必须是a Natural.在第二种情况下,函数只是错误而不返回,因此类型仍然成立.

在大多数情况下,您不仅仅会在失败案例中出错,而且还会提供某种替代行为.这仍然允许您在主体内细化类型.

(define n : (Option Natural) #f)

(cond
  [n
   ; do something with n as a number
   (+ n 1)]
  [else
   ; do something else
   (void)])

在第一种情况的主体内,其类型n被细化为Natural,因此可以这样使用.

在你实际的情况下也只想抛出时,类型不匹配的错误,你可以使用assert或cast.前者实际上是一个派生概念,它基本上执行与上面第一个例子相同的检查.你这样使用它:

(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实际上不是a Natural,那么这也会引发错误,否则整个表达式就变成了类型Natural.