racket - Typed/Racket 中函数类型的类型谓词

Question

我正处于设计框架的早期阶段，并且正在玩弄 typed/racket .假设我有以下类型:

   (define-type Calculate-with-one-number (-> Number Number))
   (define-type Calculate-with-two-numbers (-> Number Number Number))

我想要一个按类型分派(dispatch)的函数:

(: dispatcher (-> (U Calculate-with-one-number Calculate-with-two-numbers) Number))

(define (dispatcher f args)
   (cond [(Calculate-with-one-number? f)
          (do-something args)]
         [(Calculate-with-two-numbers? f)
          (do-something-else args)]
         [else 42]))

如何创建类型谓词 Calculate-with-one-number?和 Calculate-with-two-numbers?在 Typed/Racket ?对于非函数谓词，我可以使用 define-predicate .但是不清楚如何实现函数类型的谓词。

Answer 1

由于我是自我回答，因此我冒昧地根据将 arity 作为解决方案的讨论来澄清我的问题的要点。 arity 的差异是由于我在指定问题时没有考虑其含义。

问题

在 #lang typed/racket就像在许多 Lisps、函数中一样，或者更准确地说:procedures , 是一流的数据类型。

默认情况下，#lang racket通过 arity 键入程序并且参数类型中的任何其他特殊性都必须通过契约(Contract)来完成。在 #lang typed/racket由于语言的“内置契约”，过程由参数类型以及它们的参数和返回值的类型进行类型化。

以数学为例

Typed Racket Guide提供 example使用 define-type 定义过程类型:

 (define-type NN (-> Number Number))

这允许更简洁地指定过程:

 ;; Takes two numbers, returns a number
 (define-type 2NN (-> Number Number Number))

 (: trigFunction1 2NN)
 (define (trigFunction1 x s)
   (* s (cos x)))

 (: quadraticFunction1 2NN)
 (define (quadraticFunction1 x b)
   (let ((x1 x))
     (+ b (* x1 x1))))

目标

在像数学这样的领域中，使用更抽象的过程类型会很好，因为知道函数在上限和下限之间是循环的(例如 cos )与只有一个边界(例如我们的二次函数)与渐近(例如双曲线函数)提供了关于问题域的更清晰的推理。能够访问诸如以下内容的抽象会很好:

 (define-type Cyclic2NN (-> Number Number Number))
 (define-type SingleBound2NN (-> Number Number Number))

 (: trigFunction1 Cyclic2NN)
 (define (trigFunction1 x s)
   (* s (cos x)))

 (: quadraticFunction1 SingleBound2NN)
 (define (quadraticFunction1 x b)
   (let ((x1 x))
     (+ b (* x1 x1))))

 (: playTone (-> Cyclic2NN))
 (define (playTone waveform)
   ...)

 (: rabbitsOnFarmGraph (-> SingleBound2NN)
 (define (rabbitsOnFarmGraph populationSize)
   ...)

唉， define-type当涉及到程序时，不会提供这种级别的粒度。更重要的是，我们可以轻松地使用 define-predicate 手动为程序编写这种类型区分的简短错误希望。被打破:

Evaluates to a predicate for the type t, with the type (Any -> Boolean : t). t may not contain function types, or types that may refer to mutable data such as (Vectorof Integer).

从根本上说，类型的用途超出了静态检查和契约(Contract)。作为该语言的一等成员，我们希望能够分派(dispatch)更细粒度的过程类型。从概念上讲，我们需要的是符合 Cyclic2NN? 的谓词。和 SingleBound2NN? .使用 case-lambda 只有 arity 进行调度只是不够。

来自无类型 Racket 的指导

幸运的是，Lisps 是用于编写 Lisps 的领域特定语言，一旦我们拉开帷幕以揭示向导，最终我们就可以得到我们想要的东西。关键是要以另一种方式解决问题并询问“我们如何使用谓词 typed/racket 为我们提供程序？”

结构是 Racket 的用户定义数据类型，是扩展其类型系统的基础。结构是如此强大，以至于即使在基于类的对象系统中，“ classes and objects are implemented in terms of structure types”也是如此。

在 #lang racket结构可以作为程序应用，给出 #:property关键字使用 prop:procedure其次是其值(value)的过程。该文档提供了两个示例:

first example指定要作为过程应用的结构域。显然，至少一旦被指出，该字段必须保存一个评估为过程的值。

> ;; #lang racket
> (struct annotated-proc (base note)
     #:property prop:procedure
      (struct-field-index base))
> (define plus1 (annotated-proc
     (lambda (x) (+ x 1))
     "adds 1 to its argument"))
> (procedure? plus1)
#t
> (annotated-proc? plus1)
#t
> (plus1 10)
11
> (annotated-proc-note plus1)
"adds 1 to its argument"

在 second example匿名过程λ直接作为属性值的一部分提供。 lambda 在第一个位置接受一个操作数，该操作数被解析为用作过程的结构的值。这允许访问存储在结构的任何字段中的任何值，包括那些对过程求值的值。

> ;; #lang racket
> (struct greeter (name)
    #:property prop:procedure
    (lambda (self other)
       (string-append
         "Hi " other
          ", I'm " (greeter-name self))))
> (define joe-greet (greeter "Joe"))
> (greeter-name joe-greet)
"Joe"
> (joe-greet "Mary")
"Hi Mary, I'm Joe"
> (joe-greet "John")
"Hi John, I'm Joe

将其应用于打字/ Racket

唉，这两种语法都不适用于 struct 如在 typed/racket 中实现.问题似乎是当前实现的静态类型检查器不能同时定义结构并将其签名解析为过程。使用 typed/racket 时，似乎没有在正确的阶段提供正确的信息的 struct特殊形式。

为了解决这个问题， typed/racket提供 define-struct/exec 大致对应于 #lang racket 中的第二种句法形式减去关键字参数和属性定义:

    (define-struct/exec name-spec ([f : t] ...) [e : proc-t])

      name-spec     =       name
                    |       (name parent)

Like define-struct, but defines a procedural structure. The procdure e is used as the value for prop:procedure, and must have type proc-t.

它不仅为我们提供了强类型的过程形式，而且比 #lang racket 中的关键字语法更优雅一些。 .解决此答案中重述的问题的示例代码是:

#lang typed/racket

(define-type 2NN (-> Number Number Number))

(define-struct/exec Cyclic2NN
   ((f : 2NN))
   ((lambda(self x s)
     ((Cyclic2NN-f self) x s))
      : (-> Cyclic2NN Number Number Number)))

 (define-struct/exec SingleBound2NN
   ((f : 2NN))
   ((lambda(self x s)
     ((SingleBound2NN-f self) x s))
       : (-> SingleBound2NN Number Number Number)))

 (define trigFunction1 
   (Cyclic2NN 
    (lambda(x s) 
      (* s (cos x)))))

(define quadraticFunction1
  (SingleBound2NN
    (lambda (x b)
      (let ((x1 x))
        (+ b (* x1 x1)))))

定义的过程在以下意义上是强类型的:

> (SingleBound2NN? trigFunction1)
- : Boolean
#f
>  (SingleBound2NN? quadraticFunction1)
- : Boolean
#t

剩下的就是编写一个宏来简化规范。