使用多态联合类型的出现类型

Question

假设我想将以下无类型代码转换为有类型的球拍。这些函数受到 SICP 的启发，它们展示了如何完全从函数构造数据结构。

(define (make-pair x y)
    (lambda (c)
        (cond
            ((= c 1) x)
            ((= c 2) y)
            (error "error in input, should be 1 or 2"))))

(define (first p) (p 1))
(define (second p) (p 2))

要将其直接转换为键入的球拍，make-pair 函数的返回值似乎是(: make-pair (All (A B) (-> A B (-> Number (U A B)))))。然后，first 的类型应该是(: first (All (A B) (-> (-> Number (U A B)) A)))。然而，在实现函数时，我们现在不能直接调用(p 1)，因为我们需要某种出现类型来确保first 只返回A 类型。将first 的返回类型更改为(U A B) 是可行的，但随后出现键入的负担由用户承担，而不是在API 中。那么在这种情况下，我们如何在first 中使用出现类型（即如何对类型变量A 使用谓词），以便我们可以安全地只返回对的第一个组件？

更新

我尝试了一种与上面略有不同的方法，它需要将 A 和 B 的谓词作为参数提供给 make-pair 函数。下面是代码：

#lang typed/racket


(define-type FuncPair (All (A B) (List (-> Number (U A B)) (-> A Boolean) (-> B Boolean))))

(: make-pair (All (A B) (-> A B (-> A Boolean) (-> B Boolean) (FuncPair A B))))
(define (make-pair x y x-pred y-pred)
    (list
        (lambda ([c : Number])
            (cond
                ((= c 1) x)
                ((= c 2) y)
                (else (error "Wrong input!"))))
        x-pred
        y-pred))

(: first (All (A B) (-> (FuncPair A B) Any)))
(define (first p)
    (let ([pair-fn (car p)]
          [fn-pred (cadr p)])
        (let ([f-value (pair-fn 1)])
            (if (fn-pred f-value)
                f-value
                (error "Cannot get first value in pair")))))

但是，这在检查(fn-pred f-value) 条件中失败，错误为expected: A given: (U A B) in: f-value

Answer 1

从问题开头的无类型代码来看，似乎一对 A 和 B 是一个函数，给定1，返回 A，给定 2，返回 B。表达方​​式这种类型的函数带有case-> 类型：

#lang typed/racket

(define-type (Pairof A B)
  (case-> [1 -> A] [2 -> B]))

可以像原始无类型代码一样定义访问器，只需添加类型注释：

(: first : (All (A B) [(Pairof A B) -> A]))
(define (first p) (p 1))
(: second : (All (A B) [(Pairof A B) -> B]))
(define (second p) (p (ann 2 : 2)))

构造函数的类型应该是：

(: make-pair : (All (A B) [A B -> (Pairof A B)]))

但是构造函数并不能完全按原样工作。有一个问题是您的 else 子句缺少其中的 else 部分。修复给你：

(: make-pair : (All (A B) [A B -> (Pairof A B)]))
(define (make-pair x y)
  (lambda (c)
    (cond
      [(= c 1) x]
      [(= c 2) y]
      [else (error "error in input, should be 1 or 2")])))

这几乎是对的，如果打字球拍足够棒，那就是。 Typed Racket 将equal? 专门用于出现类型，但它对= 不做同样的事情。将 = 更改为 equal? 可以解决此问题。

(: make-pair : (All (A B) [A B -> (Pairof A B)]))
(define (make-pair x y)
  (lambda (c)
    (cond
      [(equal? c 1) x]
      [(equal? c 2) y]
      [else (error "error in input, should be 1 or 2")])))

理想情况下，出现类型应该与 = 一起使用，但也许像 (= 2 2.0) 之类的东西返回 true 使得它更难实现且不太有用。