PS Trying to find types of the following should also be done when
evaluating type systems:

(vector 1 'foo '())

#0=(#0#)

(syntax (let ((x 1)) (+ x x)))

Am Do., 10. Nov. 2022 um 08:06 Uhr schrieb Marc Nieper-Wißkirchen
<xxxxxx@gmail.com>:
>
> Starting by trying to describe types for what's already in Scheme
> sounds like a good idea.  I would start with the basics:
>
> Be creative and try to think of what should be the types of the
> following expressions:
>
> +
>
> 0
>
> #i0
>
> (<operator> <operand> ...)
>
> (<keyword> <datum> ...)
>
> call/cc
>
> (lambda (x)
>   "converts seconds to minutes"
>   (/ x 60))
>
> (raise (make-assertion-violation))
>
> (case-lambda
>   [() 42]
>   [(x) (when (symbol=? 'x 'german) "zweiundvierzig"])
>
> (let* ()
>   (define-record-type pair (fields x y))
>   make-pair)
>
> (values 1 2 3)
>
> values
>
> "string"
>
> (string-copy "string")
>
> Am Mi., 9. Nov. 2022 um 23:54 Uhr schrieb Lassi Kortela <xxxxxx@lassi.io>:
> >
> > Scheme is a dynamically typed language and should stay that way.
> >
> > Nevertheless, static types are irresistible in some of the application
> > areas that are of the greatest personal interest to me.
> >
> > The most important one is code sharing. Useful software systems involve
> > a lot of unimaginative work implementing well known algorithms, formats,
> > and protocols. Language enthusiasts often act like there are good
> > reasons to have 100 slightly different variations of this stuff but I
> > don't buy any of those reasons. I want less variety and more re-use.
> >
> > When thinking of code re-use, we should think first about execution
> > models. A dynamic language can support virtually the same execution
> > model as a static language. I think this should be exploited by writing
> > most of the unexciting code in the static language, then translating to
> > the dynamic one by throwing away the type restrictions. (Likewise code
> > can be written in a language with macros, and the expanded code
> > translated into a language without macros that has a similar execution
> > model.)
> >
> > Observe that the converse does not work: translating a dynamic language
> > into a static one is a scruffy Artificial Intelligence problem. Any
> > formalism you could invent to solve it would itself be a type system.
> >
> > The reason I didn't quit Scheme after a few months as I initially
> > expected is that it's still the best core for algorithmic programming.
> > You get the lambda calculus with an arbitrarily extensible syntax that
> > can be used to add types, constraints, and whatever else you need on the
> > side. For as long as we'll represent programs as trees and not as more
> > general graphs, this is where it's at.
> >
> > So if we add types to Scheme, that gives a language which translates
> > easily enough into any language with a lambda calculus based execution
> > model and either dynamic types or compatible static types.
> >
> > This ties into a big and evolving web I have in my mind about how to
> > organize the social and technical aspects of programming for maximum
> > productivity in the next decade or two. There's much more to be said on
> > that later. For now, I'd like to remark that no one has the moral
> > authority to step up and say "this is the kind of type system that
> > Statically Typed Scheme (TM) should have". A standardized, dynamically
> > typed language has dynamic types, and any static complement is just
> > someone's opinion.
> >
> > That being said, it would be a tragedy if different groups of people go
> > off and over time make 3 or 5 different type systems for Scheme with no
> > possibility of code re-use between them.
> >
> > I'd like to make an attempt to avoid that fate early by surveying the
> > kinds of type systems available, with a view to finding equivalences and
> > automatic conversions between them. We should find ways to express
> > algorithms and interfaces that solve practical problems in Scheme, such
> > that the same surface syntax can automatically be turned into the
> > dynamically type Scheme we have now as well as any nascent typed
> > flavors. Ideally the surface syntax will be something as similar as
> > possible to dynamic Scheme, which would make it painless to copy/paste
> > code between them. Type inference the gateway.
> >
> > Personally I like my type systems the way I like my memory management:
> > invisible. To that end, I'll pursue simplicity with maximum inference.
> > If others are inspired to look into something heavier like effects or
> > dependent types, that's fine. We should find ways to interface our work.
> > There still is the https://github.com/pre-srfi/static-scheme repo which
> > I kind of bowed out of since the proposed system got too complex for me.
> > Maybe some of you will want to run with that and see where it goes.
> >
> > But I didn't fully realize back when we started the repo that "Typed
> > Scheme" should intrinsically be a network of type systems with
> > translation pathways between them, sharing as much surface syntax and
> > nomenclature as possible. If memory serves, we started a kind of rivalry
> > about what kind of type system would "win", but there should be no winner.
> >
> > The way to start the long trek toward types is bottom up: Find practical
> > problems, then say "here's how I would express this using my favorite
> > type system". Compare solutions. As the first order of business, we
> > should write types for the procedures in RnRS and the most popular SRFIs.
> >
> > While these "Typed Schemes" will take a decade to mature into something
> > canonical, I think the problem is urgent because it may guide the
> > evolution of dynamic Scheme. My ideal is not the "gradual typing" found
> > in Common Lisp and Racket, but "twin typing" where there are separate
> > dynamic and static languages, and the surface syntax is as compatible as
> > possible to the point that you hardly have to care which one you're
> > using at any given time.
> >
> > Comments are welcome, but above all, please help me write down type
> > signatures for the Scheme canon. There are bound to be many surprises,
> > both pleasant and vexing.