On Thu, Nov 10, 2022, at 3:05 AM, Peter Bex wrote:
> On Thu, Nov 10, 2022 at 08:42:20AM +0100, Marc Nieper-Wißkirchen wrote:
>> PS Trying to find types of the following should also be done when
>> evaluating type systems:
>>
>> (vector 1 'foo '())
>
> And, not to forget, what if you do (vector-set! x 1 "bar") later in the
> program.
>
> Cheers,
> Peter
>

Just to point out the obvious, Sam Tobin-Hochstadt's PhD thesis is titled "Typed Scheme": https://www2.ccs.neu.edu/racket/pubs/dissertation-tobin-hochstadt.pdf

I don't know all of the history, but my understanding is that it builds on several previous attempts to add types to Scheme.

The implementation is the `#lang typed/scheme` language, a variant of the PLT `#lang scheme` language: https://docs.racket-lang.org/ts-reference/Compatibility_Languages.html

The project has become Typed Racket, which has an introductory Guide <https://docs.racket-lang.org/ts-guide/> and a reference manual <https://docs.racket-lang.org/ts-reference/index.html>. The upcoming Racket 8.7 release will include Shallow and Optional Typed Racket from Ben Greenman's work: https://racket.discourse.group/t/pre-release-shallow-and-optional-types/1303

Here's a working program:
```
#lang typed/racket
(: x (Vector Natural (U 'foo String) (Listof Real)))
(define x
  (vector 1 'foo '()))
(vector-set! x 1 "bar")
```

-Philip