如何在类型化的球拍中定义语法？

Question

这个有效

#lang racket

(begin-for-syntax
  (define (foo n)
    (+ n 3)))

所以我也希望它能起作用

#lang typed/racket

(: foo : Real -> Real)
(define-for-syntax (foo n)
  (+ n 3))

但如果失败

; :: undefined;
;  cannot reference an identifier before its definition

之后，我在 typed/racket

中依次尝试了以下各项

(define-for-syntax (foo (n : Real)) : Real
  (+ n 3))

(begin-for-syntax
  (: foo (-> Real Real))
  (define (foo n)
    (+ n 3)))

(begin-for-syntax
  (define (foo (n : Real)) : Real
    (+ n 3)))

每一个都因为这样或那样的原因而失败。难道typed/racket搞不定{begin|define}-for-syntax？

Answer 1

#lang typed/racket

(: foo : Real -> Real)
(define-for-syntax (foo n)
  (+ n 3))

失败：

Type Checker: Declaration for `foo' provided, but `foo' has no definition

对我来说，这完全有道理。 foo 在阶段 1 中定义，因此类型声明在阶段 0 中找不到它的定义。

(begin-for-syntax
  (: foo (-> Real Real))
  (define (foo n)
    (+ n 3)))

比较“正确”，但还是有很多问题。代码在阶段 1，但是 : 在阶段 0 被 #lang typed/racket 导入，所以你得到一个错误：

:: undefined

然而，另一个主要问题是，即使您设法在阶段 1 中导入 :，类型检查器仍然无法正常工作。

简而言之，以下是如何让它发挥作用。

#lang typed/racket

(module for-syntax-mod typed/racket
  (provide foo)
  (: foo (-> Real Real))
  (define (foo n)
    (+ n 3)))

(require (for-syntax 'for-syntax-mod))

(begin-for-syntax (println (foo 10)))

这在语言 typed/racket 的子模块 for-syntax-mod 中声明了 foo，因此类型检查器现在将按预期在该子模块上工作。然后我们在阶段 1 导入这个子模块，所以现在 foo 在 begin-for-syntax 中可用。请注意，begin-for-syntax 中的代码仍未进行静态类型检查。

如何在类型化的球拍中定义语法？

How to do define-for-syntax in typed racket?

syntax

macros

typed

racket