在Typed/Racket中键入函数类型的谓词

Question

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

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

我想要一个派生类型的函数:

(: 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的差异是由于我在指定问题时没有考虑其含义.

问题

在#lang typed/racket为众多的Lisp,函数,或者更恰当:程序,都是一流的dataypes.

默认情况下,arity#lang racket类型的过程以及参数类型中的任何其他特性必须通过契约来完成.在#lang typed/racket过程中,由于语言的"烘焙合同",由arity和它们的参数类型以及返回值键入.

以数学为例

的类型化的球拍指南提供了一个例子使用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破灭:

使用类型(Any - > Boolean:t)计算类型t的谓词.t可能不包含函数类型,或者可能引用可变数据的类型,例如(Vectorof Integer).

从根本上说,类型具有静态检查和合同之外的用途.作为该语言的一等成员,我们希望能够调度我们更精细的程序类型.从概念上讲,所需要的是谓词Cyclic2NN?和SingleBound2NN?.只使用arity进行调度case-lambda是不够的.

来自Untyped Racket的指导

幸运的是,Lisps是用于编写Lisps的领域特定语言,一旦我们重新开启以展示向导,最终我们可以得到我们想要的东西.关键是以另一种方式处理问题并询问"我们如何使用谓词typed/racket为我们提供程序？"

结构是Racket用户定义的数据类型,是扩展其类型系统的基础.结构非常强大,即使在基于类的对象系统中," 类和对象也是根据结构类型实现的 ".

在#lang racket结构中可以应用作为给出#:property关键字使用prop:procedure的过程,然后是对其值的过程.该文档提供了两个示例:

第一个示例指定要作为过程应用的结构的字段.显然,至少有一次指出,该字段必须包含一个评估过程的值.

> ;; #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"

在第二示例中,匿名过程λ直接作为属性值的一部分提供.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

将其应用于打字/球拍

唉,这两种语法都没有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)

与define-struct类似,但定义了一个过程结构.procd e用作prop:procedure的值,并且必须具有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

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

Answer 2

在一般情况下,由于Racket中的类型实现方式,您想要的是不可能的.Racket有合同,它是运行时包装器,可以保护程序的其他部分.函数契约是一个将函数视为黑盒子的包装器 - 表单的契约(-> number? number?)可以包装任何函数,新的包装器函数首先检查它是否收到一个number?然后将它传递给包装函数,然后检查包装函数返回一个number?.这一切都是动态完成的,每次调用该函数.Typed Racket添加了静态检查类型的概念,但由于它可以提供和要求非类型化模块的值,因此这些值受到代表其类型的合同的保护.

在您的函数中dispatcher,您在运行时f 动态接受函数,然后根据您获得的函数类型执行某些操作.但是函数是黑盒子 - 合同实际上并不知道它们包装的函数,只是检查它们的行为是否正常.没有办法判断是否给出了表单的形式或功能的功能.由于可以接受任何可能的功能,因此功能是黑盒子,没有关于他们接受或承诺的信息.只能假设合同中的函数是正确的并尝试使用它.这也是原因dispatcher(-> number? number?)(-> string? string?)dispatcherdispatcherdefine-type 没有为函数类型自动生成谓词 - 没有办法证明函数具有动态类型,你只能将它包装在契约中并假设它的行为.

例外情况是arity信息 - 所有函数都知道它们接受了多少个参数.该procedure-arity功能将为您提供此信息.所以,当你不能在运行时的函数类型派遣一般,你可以派遣的功能参数数量.这是做什么的case-lambda- 它使一个函数根据它收到的参数数量进行调度:

(: dispatcher (case-> [-> Calculate-with-one-number Number Void]
                      [-> Calculate-with-two-numbers Number Number Void]))

(define dispatcher
  (case-lambda
    [([f : Calculate-with-one-number]
      [arg : Number])
     (do-something arg)]
    [([f : Calculate-with-two-numbers]
      [arg1 : Number]
      [arg2 : Number])
     (do-something-else arg1 arg2)]
    [else 42]))