Hi,
I've recently been thinking a bit about static and dynamic types,
inspired by this article

https://buttondown.email/hillelwayne/archive/a-totally-polished-and-not-at-all-half-baked-take/

and also by Andrew K. Wright's work on "soft type system" for Scheme.

I did some googling, which mainly redirected me to the vivid discussions that were happening here in the 90s and early 2000.

(What happened to all those people?)

In one of the threads Jeffrey Mark Siskind noted that there are at least three type systems for Scheme: Wright's "soft system", the thing called "typed Scheme" (which as I believe now became "typed Racket") and the type system in Stalin.

I also ran into this, which claims to be based on the EOPL book:

http://eecs.ucf.edu/~leavens/typedscm/typedscm.html

(IIRC I was once reading Kent Dybvig's paper on the history of Chez, where he claimed that he also added static typing there at some point)

I'd be interested if anyone has any details about the type system in Stalin, or any other attempts of planting static types in Scheme.

Some googling pointed me to this SO question, which claims that Siskind "was planning to write a series of papers detailing aspects of the implementation, but never got around to doing that."

https://stackoverflow.com/questions/23309082/global-type-inference-in-the-scheme-compiler-stalinhttps://stackoverflow.com/questions/23309082/global-type-inference-in-the-scheme-compiler-stalin

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

I am also interested by this subject.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Amirouche Boubekki <amirouche.boubekki@gmail.com> wrote:

I am also interested by this subject.

I have once started to write some Hindley-Milner type inference code
for Scheme, based on EOPL I think. It contained inference rules for
most R4RS procedures, but I lost interest before finishing the program.
The greatest to-do is probably recursive types (i.e., letrec, named let).
It could already do things like

(sig '(define (length x)
(if (null? x)
0
(+ 1 (length (cdr x))))))
--> (-> list int)

If anyone is interested, I could probably dig up the code and put
it on my homepage or post it here.

--
Nils M Holm < n m h @ t 3 x . o r g > www.t3x.org

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Le dim. 12 juil. 2020 à 21:26, Paul Rubin a écrit :

If you want static types, why not use ML or Haskell directly, instead of trying to graft types onto Scheme?

It is not necessarily grafting static types. I want to have an easier
way to document code. In this regard, inferred types can help both to
generate documentation programmatically and help during development.
One thing, that is missing in Python optional or gradual typing is the annotation of possible exceptions. Neither types nor exceptions are
inferred from source, that is what I am trying to achieve.

I am not sure about error checking since I have no experience with it
(things like Racket contracts?). The system I am thinking about will rely
on SRFI-145 assumptions.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Maciek Godek <godek.maciek@gmail.com> writes:

https://buttondown.email/hillelwayne/archive/a-totally-polished-and-not-at-all-half-baked-take/

This is similar to Chris Smith's very good article "What To Know Before Debating Type Systems":

https://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/

I'd be interested if anyone has any details about the type system in
Stalin, or any other attempts of planting static types in Scheme.

I had thought Stalin (like many Lisp compilers) used types for
optimization (unboxing, specialization, etc.) but not so much for error checking. There is typed Racket as you mentioned, plus typed Clojure;
and moving further afield, the Erlang Dialyzer, Python 3's type
annotations used with the Mypy checker, and something similar that's
recently appeared for Ruby.

I've used Mypy and Dialyzer and found them helpful but impeded by the underlying language that prevented them from going further. I'd expect
the soft type systems for Racket and Clojure would be about the same
way.

If you want static types, why not use ML or Haskell directly, instead of
trying to graft types onto Scheme? See also, "Why calculating is better
than scheming", about Miranda, which was a forerunner of Haskell:

https://www.cs.kent.ac.uk/people/staff/dat/miranda/wadler87.pdf

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On Sunday, July 12, 2020 at 8:54:01 PM UTC+2, Nils M Holm wrote:

Amirouche Boubekki wrote:

I am also interested by this subject.

I have once started to write some Hindley-Milner type inference code
for Scheme, based on EOPL I think. It contained inference rules for
most R4RS procedures, but I lost interest before finishing the program.
The greatest to-do is probably recursive types (i.e., letrec, named let).
It could already do things like

(sig '(define (length x)
(if (null? x)
0
(+ 1 (length (cdr x))))))

list int)

If anyone is interested, I could probably dig up the code and put
it on my homepage or post it here.

Please do :)

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

W dniu niedziela, 12 lipca 2020 21:26:39 UTC+2 użytkownik Paul Rubin napisał:

https://buttondown.email/hillelwayne/archive/a-totally-polished-and-not-at-all-half-baked-take/

This is similar to Chris Smith's very good article "What To Know Before Debating Type Systems":

https://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/

I'd be interested if anyone has any details about the type system in Stalin, or any other attempts of planting static types in Scheme.

I had thought Stalin (like many Lisp compilers) used types for
optimization (unboxing, specialization, etc.) but not so much for error checking.

Still, I think that the design itself would be interesting.

There is typed Racket as you mentioned, plus typed Clojure;
and moving further afield, the Erlang Dialyzer, Python 3's type
annotations used with the Mypy checker, and something similar that's
recently appeared for Ruby.

My main motivation is not about type annotations, at least not most of the time.
I'd like to be able to define record types with typed fields, and without cluttering global namespace.

I've used Mypy and Dialyzer and found them helpful but impeded by the underlying language that prevented them from going further. I'd expect
the soft type systems for Racket and Clojure would be about the same
way.

If you want static types, why not use ML or Haskell directly, instead of trying to graft types onto Scheme? See also, "Why calculating is better
than scheming", about Miranda, which was a forerunner of Haskell:

https://www.cs.kent.ac.uk/people/staff/dat/miranda/wadler87.pdf

I've read that essay a while ago, but IIRC it contained some arguments of extremely poor quality IMO
("Lambda-calculus expressed in Miranda is less readable that Scheme, but we can make Scheme equally unreadable")

I've also digged into some old discussions here on comp.lang.scheme, and I recall someone making the point that "Scheme allows you to use any type system that you need".
(Other than that, I have to say that it was extremely funny to read old flame wars from today's perspective)

In this regard, I was most impressed by Mark Tarver's "Shen" programming language, which contains a type-level Prolog interpreter expressed in sequent calculus.

As to "not using ML or Haskell directly", the answer is quite simple: they have annoying, arbitrary syntax. (I mean, I like Haskell as a pen and paper notation, but s-expressions are much more convenient to work with in Emacs)

Besides, I don't know much about ML, but I've heard a lot of people complaining on Haskell's implementation of records, which is really a huge disappointment.

(I think that structures are one thing that's been done really well in C, and it contributed hugely to the success of that language)

Also, Haskell's laziness, which requires one to use weird monad tricks, can be annoying.

Anyway, after some digging, I found this:

http://www.cs.ucf.edu/~leavens/tech-reports/ISU/TR95-21/TR.pdf

which also contained reference to this:

https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=BBFF108E0789179A94941C14168D2BA9?doi=10.1.1.56.9923&rep=rep1&type=pdf

So there have been some fairly mature attempts in the 1990s

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Doesn't Kawa Scheme have some kind of type declarations? s7 has signatures and setters giving static and dynamic types. s7.html has a somewhat jumbled discussion
of these, and s7test.scm has many examples. s7's optimizer and lint.scm use the signatures a lot. Your record would probably be a "let" and you can set the types
of the record fields.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

[I missed this discussion before now - due to some misconfiguration on my part.]

Doesn't Kawa Scheme have some kind of type declarations?

Yes. In most places where you can declare an identifier NAME
you can instead write NAME ::TYPE, which declared NAME to have the specified TYPE.

For example:
(let ((i ::integer (length '(A B C))))
(+ i i))

This declares the variable i to have type integer.

This is used both for error-checking and optimization.
That i has type integer, implies (among other things) that
it has an implementation type, in this case a reference
to the JVM class gnu.math.IntNum, which affects code generation.
It can enable various optimization. For example the + in the example
above is implemented as a call to the static method gnu.math.IntNum.add,
rather than generic addition.

The end result is that you can write Scheme code that is as efficient
as well-written Java, which can run run very fast indeed on modern JVMs.

(Kawa makes little use of the "newer" "invokedynamic" features, so far.)

Type-checking is done statically as "optimistic typing". Consider:
(let ((VARIABLE ::TYPE VALUE)) ...)
If the compiler can prove that VALUE is an instance of TYPE, no run-time code is needed.
In some cases, the type of VALUE may be semantically a subtype of TYPE,
but the implementation type is not a subtype of the implementation type of TYPE.
In that case, the compiler insert conversion code. For example of VALUE is
an (unboxed native 32-bit) 'int' but TYPE is 'integer' then the compiler inserts
a call to "box" the VALUE.

If the compiler can prove that the type of VALUE does not overlap with TYPE, then the compiler reports a compile-time error.
Otherwise, the compiler generates a run-time cast/type-check.

The compiler does some flow analysis that works pretty well,
thought it could be made more sophisticated. (It currently doesn't
make use of Scheme type prediacte such as integer?.) The type-system
is a bit ad hoc, but catches many error, allows very efficient code,
and is relatively "light" in use.

Type-testing is integrated with the pattern system:

(if (? NAME ::TYPE VALUE)
(do-this-if-TYPE NAME)
(do-this-if-not-TYPE))

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

I ran into this today.
It's below 100 lines of code.

https://github.com/dys-bigwig/typing-scheme

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)