WIP: add type-out provide-spec

[bennn]

(Work-in-progress because there's a bug with (type-out (struct ...)) -- you can't use the struct inside the defining module.)

Adds initial support for a type-out provide spec.

Design goals:

• Behavior is a superset of contract-out (currently missing #:exists and #:forall)
• Look like an ML-style interface, with all type defs. and typed identifiers

Current look:

#lang typed/racket/base

(provide
  (type-out
    (type FullName (List String String))
    (struct person ([name : FullName] [id : Natural]))
    (get-first-name (-> FullName String))))

(define (get-first-name fn)
  (car fn))

Later on, I'd like to add #:exists & #:forall to bind variables across multiple type definitions, and options to export opaque types and ADTs. But I think it's better to address those separately.

[bennn]

Possible issue: I'm re-ordering the top-level forms so that type declarations come first. Without this, type annotations aren't associated with the right definitions.

Not sure whether this will change to fix the bug with structs.

[samth]

A few thoughts:

• Can you describe the intended semantics of this briefly? Is it a replacement for top-level type annotations, or an ML-style signature (ie, you'd still need annotations internally), or something else?
• I really don't think struct definitions should go in the provide form. That's not how it works in contract-out -- you have to have a definition of the struct in the module, and it's not how it works in ML either. Changing that should make the struct issue easier to solve.

[bennn]

• Yes, this is intended as a replacement for top-level type definitions.* The idea is to put types where the user is more likely to see them & keep abusing provide as an API. I also want to offer a smooth migration from contract-out -- just change "contract" to "type" and you're rolling.
• Removing struct defs would solve the issue, but then (type-out (struct ...)) is pretty much a no-op. We can only check that both type annotations (in the provide & at the definition) match.

* Non-provided functions would still need an annotation

[bennn]

Leif pointed out that we definitely don't want struct properties declared in a provide form, so now I'm in favor of writing the fields twice (in code & in the type-out). We could then also use the type-out to hide some fields or use different types.

[samth]

I think we should start with something that just handles type annotations, and see how that works. I don't think provide should produce definitions (except as an implementation detail, as in contract-out), and I think information hiding a la ML modules is a larger design issue that deserves more thought before we start implementing.

[bennn]

Ok. Do you mind if it allows define-type aliases?

... (type-out T (Listof Integer)) ...

=== becomes ===>

(define-type T (Listof Integer))
(provide T)

[samth]

That's what I mean about definitions. I don't think provide should introduce new bindings in the module. Nothing else in Racket works that way.

[bennn]

Checkpoint:

• No longer makes definitions, just adds annotations & renames. (doc-screenshot)
• TODO: struct types are currently ignored. We should check that:
  • field types match implementation
  • super declarations are correct
  • all fields are annotated (can't leave out field / super field from type-out)
  • (anything else?)

Is there an easy way to get struct information from the struct type name? I tried struct-type-info but I haven't got the right inspector. (I can probably copy what contract-out does, once I understand that.)

#lang typed/racket/base
(struct s ())
(call-with-values (lambda () (struct-type-info struct:s)) list)
;; struct-type-info: current inspector cannot extract info for structure type

[bennn]

Things are pretty good now, but I'm blocked on 1 problem and have a few questions:

Problem: this is currently incompatible with the #:type-name option because I assume the struct name is the type name. How can I get a type name from a struct name?

Questions

• type-out annotations for struct fields are only checked, not enforced. So (struct s ([x : Integer])) ... (type-out s ([x : Real]))) ... is valid and users will get integers from s-x. Should we fix this, and reject non-exact type-out annotations?
• Currently check struct recursively to make sure all supertype fields are given annotations. Should we not do that (I'm thinking we should not do that)
• Order of struct field annotations is not enforced. (Probably should be)

EDIT: supertype fields must not be included, field order is enforced

[bennn]

status update: this PR is not ready to merge because it doesn't handle structs as well as contract-out. Need to fix #322 first.