Shallow / Optional types

[bennn]

Now that Typed Racket has Shallow & Optional modes, we might be able to make the math library work for untyped code without crazy slowdowns.

But it's not as simple as changing the whole math library to use #lang typed/racket/shallow, because that'll slow down all the current #lang typed/racket clients of math.

I think what we need is a graceful way to provide two versions of math (without actually cloning the codebase):

1. keep the original
2. add math/untyped or something, which uses Shallow

[bennn]

Maybe TR should have a multi lang that copies well-typed code into a few different submodules.

[racket-discourse-github-bot]

This issue has been mentioned on Racket Discussions. There might be relevant details there:

https://racket.discourse.group/t/pre-release-shallow-and-optional-types/1303/6

[Rscho314]

@bennn At what stage does (static) typechecking happen in the typed/racket process? In other words, is expanding to different submodules with specific type strictness straightforward, or does it require a rework of typed/racket itself?

[bennn]

Static typechecking is early. The rough pipeline is: macro-expand -> typecheck -> optimize -> protect -> done.

But, the multi lang idea is still going to need a rework of TR because the later passes depend on a type environment. If we typecheck the outer module and then copy it to two inner modules, we need to make two copies of the type env. that match the syntax locations in the inner modules.

As a first step, though, we should make sure that math compiles & runs with a different #lang and no other changes. Then we can try a simple package (no changes to TR) that provides two versions in a simple way. Then we should try to deduplicate the typechecking work.

EDIT: maybe, something really simple like choose-lang with no-check is best, if it works!, because no-check doesn't run the typechecker.

[Rscho314]

I clearly don't have the chops to go anywhere near the expander or the typechecker, unfortunately. Here is a very naive contribution. A replacement attempt with:

rpl -R -x "*.rkt" "typed/racket(?:/base)?" "typed/racket/optional" share/pkgs/math-lib/**
find "share/pkgs/math-lib/" -type f \( -name "*.zo" -o -name "*.dep" \) | xargs rm

triggers the following errors in the session (identical whether replacement is typed/racket/optional or typed/racket/shallow):

Welcome to Racket v8.6.0.12 [cs].
> (require math/array)
/home/raoul/Desktop/racket-snapshot/share/pkgs/math-lib/math/private/array/typed-array-struct.rkt:115:14: Type Checker: type mismatch
  expected: (Vectorof Integer)
  given: In-Indexes
  in: ds
 [,bt for context]
/home/raoul/Desktop/racket-snapshot/share/pkgs/math-lib/math/private/array/typed-array-struct.rkt:125:14: Type Checker: type mismatch
  expected: (Vectorof Integer)
  given: In-Indexes
  in: ds
 [,bt for context]
/home/raoul/Desktop/racket-snapshot/share/pkgs/math-lib/math/private/array/typed-array-struct.rkt:142:18: Type Checker: type mismatch
  expected: (Vectorof Integer)
  given: In-Indexes
  in: ds
 [,bt for context]
Type Checker: Summary: 3 errors encountered [,bt for context]
> ,bt
Type Checker: Summary: 3 errors encountered
  location...:
   /home/raoul/Desktop/racket-snapshot/share/pkgs/math-lib/math/private/array/typed-array-struct.rkt:115:14
   /home/raoul/Desktop/racket-snapshot/share/pkgs/math-lib/math/private/array/typed-array-struct.rkt:125:14
   /home/raoul/Desktop/racket-snapshot/share/pkgs/math-lib/math/private/array/typed-array-struct.rkt:142:18
  context...:
   /home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:481:0: type-check
   /home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:711:0: tc-module
   /home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed-racket/tc-setup.rkt:115:12
   /home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed-racket/typed-racket.rkt:22:4
   /home/raoul/Desktop/racket-snapshot/share/pkgs/xrepl-lib/xrepl/xrepl.rkt:1573:0
   /home/raoul/Desktop/racket-snapshot/collects/racket/require-transform.rkt:266:2: expand-import
   /home/raoul/Desktop/racket-snapshot/collects/racket/private/reqprov.rkt:564:5
   /home/raoul/Desktop/racket-snapshot/collects/racket/require-transform.rkt:266:2: expand-import
   /home/raoul/Desktop/racket-snapshot/collects/racket/private/reqprov.rkt:287:21: try-next
   /home/raoul/Desktop/racket-snapshot/collects/racket/private/reqprov.rkt:258:2
   /home/raoul/Desktop/racket-snapshot/collects/syntax/wrap-modbeg.rkt:46:4
   /home/raoul/Desktop/racket-snapshot/share/pkgs/xrepl-lib/xrepl/xrepl.rkt:1573:0
   [repeats 2 more times]
   /home/raoul/Desktop/racket-snapshot/collects/racket/repl.rkt:11:26

[Rscho314]

Dug a little more, and it seems a problem is that as soon as unsafe-array-ref (unsafe-vector-ref synonym) is used in a non-deep type context, it cannot differentiate between cases anymore:

Welcome to Racket v8.6.0.12 [cs].
> (require math/array)
/home/raoul/Desktop/racket-snapshot/share/pkgs/math-lib/math/private/array/typed-array-constructors.rkt:21:62: Type Checker: could not convert type to a contract;
 function type has two cases of arity 2
  identifier: unsafe-vector-ref
  type: (All (a)
          (case-> (-> (Vectorof a) Integer a) (-> VectorTop Integer Any)))
  in: (unsafe-vector-ref js k)

This error is triggered by replacing typed/racket with a shallower version in all files except racket-snapshot/share/pkgs/math-lib/math/private/array/typed-array-struct.rkt, and propagates from there. I don't really know how to go from here. Is there some way to disambiguate in a shallower type context?

[bennn]

Thanks! It looks like there's some Deep code left after the replacement. Could be a submodule, and could be a (require typed/racket) somewhere.

(EDIT: it does! just hard to see with the filename ~That error message should really say "Deep: contract conversion error" somewhere.~)

[Rscho314]

I changed my approach to use a typed/racket/no-check replacement instead, and now the error looks like below. typed-racket-lib/typed/untyped-utils.rkt would suggest that the type of check-array-shape is lost during the identifier renaming?

One thing does bug me, however: even though I'm using typed/racket/no-check, the error is still coming from the type checker. Would that still be due to some residual deeply-typed code in math? I extensively grepped the source, but could find no remaining offender...

Welcome to Racket v8.6.0.12 [cs].
> (require math/array)
/home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed/untyped-utils.rkt:60:13: Type Checker: missing type for identifier;
 consider using `require/typed' to import it
  identifier: check-array-shape2
  from module: typed-utils.rkt
  in: (define check-array-shape check-array-shape2)
 [,bt for context]
> ,bt
/home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed/untyped-utils.rkt:60:13: Type Checker: missing type for identifier;
 consider using `require/typed' to import it
  identifier: check-array-shape2
  from module: typed-utils.rkt
  in: (define check-array-shape check-array-shape2)
  location...:
   /home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed/untyped-utils.rkt:60:13
  context...:
   /home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:481:0: type-check
   /home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:711:0: tc-module
   /home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed-racket/tc-setup.rkt:115:12
   /home/raoul/Desktop/racket-snapshot/share/pkgs/typed-racket-lib/typed-racket/typed-racket.rkt:22:4
   /home/raoul/Desktop/racket-snapshot/share/pkgs/xrepl-lib/xrepl/xrepl.rkt:1573:0
   [repeats 2 more times]
   /home/raoul/Desktop/racket-snapshot/collects/racket/require-transform.rkt:266:2: expand-import
   /home/raoul/Desktop/racket-snapshot/collects/racket/private/reqprov.rkt:564:5
   /home/raoul/Desktop/racket-snapshot/collects/racket/require-transform.rkt:266:2: expand-import
   /home/raoul/Desktop/racket-snapshot/collects/racket/private/reqprov.rkt:287:21: try-next
   /home/raoul/Desktop/racket-snapshot/collects/racket/private/reqprov.rkt:258:2
   /home/raoul/Desktop/racket-snapshot/collects/syntax/wrap-modbeg.rkt:46:4
   /home/raoul/Desktop/racket-snapshot/share/pkgs/xrepl-lib/xrepl/xrepl.rkt:1573:0
   [repeats 2 more times]
   /home/raoul/Desktop/racket-snapshot/collects/racket/repl.rkt:11:26

NB. Trying (require math) instead of (require math/array) yields 3 very similar errors for other identifiers.

[bennn]

Yes, that error means there's some typed code around. It's coming from typed/untyped-utils, so probably a require/untyped-contract or define-typed/untyped-id. I know math uses both those helpers.

We should a TR issue for this. In no-check mode, the helpers should do something more helpful than expand to a type error ... either expand to require and define, or raise a syntax error "unsupported" .

[racket-discourse-github-bot]

This issue has been mentioned on Racket Discussions. There might be relevant details there:

https://racket.discourse.group/t/replacing-lexical-context-in-a-macro/2004/1