scheme - 带有剩余参数的类型 Racket 中的 Zip 函数

Question

我正在努力研究将任意数量的列表压缩在一起的函数的语法。我目前有:

(定义 (zip . [lsts : (Listof Any) *])
(应用 map (inst list Any)lsts))


这会在评估时导致以下错误:

Error: struct:exn:fail:syntax /Applications/Racket v6.6/collects/racket/private/kw.rkt:929:25: Type Checker: Bad arguments to function in `apply':

Domains: (-> a b ... b c) (Listof a) (Listof b) ... b

(-> a c) (Pairof a (Listof a))

Arguments: (-> Any * (Listof Any)) (Listof (Listof Any)) *

in: (#%app apply map (#%expression list) lsts)

因为这些评估没问题:

(apply map (inst list Any) '(("asd"1 2) ("cat"3 4)))
;;(("asd""猫") (1 3) (2 4))


(定义(测试。[lsts:(任意列表)*])
列表)
(测试'(1 2 3)'(2 3“狗”))
;;((1 2 3) (2 3 “狗”))


我认为类型检查器提示 apply 每当没有参数传入时就会失败，因为我在尝试评估以下内容时遇到了类似的错误:

(apply map (inst list Any) '())

Error: struct:exn:fail:syntax /Applications/Racket v6.6/collects/racket/private/kw.rkt:929:25: Type Checker: Bad arguments to function in `apply':

Domains: (-> a b ... b c) (Listof a) (Listof b) ... b

(-> a c) (Pairof a (Listof a))

Arguments: (-> Any * (Listof Any)) Null *

in: (#%app apply map (#%expression list) (quote ()))

但我不确定如何向函数指定它至少需要一个参数(列表)。

Answer 1

map 函数需要至少接受一个列表作为参数。考虑一下如果您使用零参数调用 zip 会发生什么。然后您将使用零列表调用 map，这是不允许的。因此，您必须限制您的 zip 函数接受一个或多个参数。您可以通过在剩余参数之前指定一个参数来做到这一点，如下所示:

#lang typed/racket

(define (zip [lst : (Listof Any)] . [lsts : (Listof Any) *])
  (apply map (inst list Any) lst lsts))

还有一点:如果它是多态的会更好。

#lang typed/racket

(: zip : (∀ (A) (-> (Listof A) (Listof A) * (Listof (Listof A)))))
(define (zip lst . lsts)
  (apply map (inst list A) lst lsts))

请注意，域仍然需要是 (Listof A) (Listof A) * 而不仅仅是 (Listof A) *。

更新:更多的多态性

实际上有可能使它的多态性变得更好，因此如果您正好给它 3 个列表，它会生成一个恰好包含 3 个元素的列表。此版本的 zip 类型为

(: zip : (∀ (A B ...)
            (-> (Listof A)         ; first input
                (Listof B) ... B   ; next n inputs, where n is the number of B type-arguments
                (Listof (List A B ... B)))))

但是，如果正文是(apply map list lst lsts)，则list 函数需要类型

(∀ (A B ...) (-> A B ... B (List A B ... B)))

但是，用作函数值的 list 只有类型 (All (a) (-> a * (Listof a)))。相反，我们可以定义一个新函数 listd，它的行为与 list 完全相同，但具有新类型

;; (listd x y z) = (list x y z)
;; but it's assigned a type that's more convenient for `zip`
(: listd : (∀ (A B ...) (-> A B ... B (List A B ... B))))
(define (listd a . bs)
  (cons a bs))

使用它，zip 的点多态版本可以这样定义:

(: zip : (∀ (A B ...)
            (-> (Listof A)         ; first input
                (Listof B) ... B   ; next n inputs, where n is the number of B type-arguments
                (Listof (List A B ... B)))))
(define (zip lst . lsts)
  (apply map (inst listd A B ... B) lst lsts))

使用它:

> (zip (list 'a 'b 'c) (list 1 2 3) (list "do" "re" "mi"))
- : (Listof (List (U 'a 'b 'c) Positive-Byte String))
'((a 1 "do") (b 2 "re") (c 3 "mi"))