Providing name only to sub-module?

Questions & Answers
,
1

Context: Inspired by Lean's #guard commands, I'd like to implement "static unit tests" in Racket, where tests give the same interactive feedback as types.

An example would look something like below:

(define (factorial n)
  (if (< n 2) 1 (* n (- n 1))))

(with-examples (factorial)
  (check-equal? (factorial 0) (*))
  (check-equal? (factorial 1) (* 1))
  (check-equal? (factorial 4) (* 1 2 3 4)) ; fail
  )

Currently, what I'm doing is creating a sub-module using module*, then requiring the enclosing module at for-syntax time. But the enclosing module may not necessarily export the function in general (e.g. it may just be a helper). So what I'm doing is whenever the programmer writes (with-examples (name) _ ...), I generate a throwaway alias name* and provide it to the sub-module instead, which it renames back to name.

What I don't like about this approach is that there will be no arrow in DrRacket if I place the cursor on factorial in the sub-module.

My question: Is there a better way to do this in Racket, to provide only specifically to a sub-module, and not necessarily everyone?

Thanks!!

1 Like
2

The typical way for a submodule to require the "public interface" of its outer module would be something like (module* name (submod "..") ___).

#lang racket/base

(define public 42)
(define private 43)

(provide (all-from-out racket/base)
         public)

(module* m (submod "..")
  (println public)) ;works, but using `private` would be an error

Not only does this limit m to exports, it goes through any contracts that might be attached at the module boundary (sometimes you might care).

This approach avoids needing to make aliases. However it doesn't seem to help with the main thing you didn't like about your approach:

The arrows aren't better -- there's just an arrow from public to (submod ".."). :frowning:

3

I see thanks!! So even in the expanded code, the arrow points to the module. That's why in the macro one, there's no arrow pointing back to the original :frowning:

#lang racket/base

(define public 42)
(define private 43)

(provide (all-from-out racket/base)
         (rename-out [private private*])
         public)

(module* m (submod "..")
  (require (rename-in (submod "..") [private* private]))
  (println private)
  (println public))
4

One thing you might try is to generate binders and references that have the right syntax locations, but are in dead code. You could use the factorial that's written at the top of with-examples both in the enclosing module (as a reference) and in the newly created module (as a binder) to get at least some arrows. Check Syntax doesn't care if you use an identifier with the same source location in multiple different unrelated scopes. It does it's best with what it finds. :slight_smile:

I tried to write an example to illustrate but ran into trouble with the submodule. Are you doing some kind of hygiene bending operations on the generated submodule?

5

Thanks Robby!! So actually I get two arrows now pointing to both binding positions, which is reasonable. I don't know how it happened and what I did differently :smiley:

Unreasonable question: We don't need to do anything for a submodule defined by module* to access the enclosing module's definitions if it's in the same phase:

#lang racket/base

(define x 42)

(module* test #f
  (println x))

Is it possible to have the submodule access the enclosing module during the submodule's for-syntax phase without explicitly providing/requiring anything?