1. Forum
  2. Usenet
  3. COMP.LANG.SCHEME

  • Static typing in Scheme

    From Maciek Godek@21:1/5 to All on Wed Jul 8 14:46:26 2020
    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)
  • From Amirouche Boubekki@21:1/5 to All on Sun Jul 12 08:55:41 2020
    I am also interested by this subject.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Nils M Holm@21:1/5 to Amirouche Boubekki on Sun Jul 12 18:53:57 2020
    Amirouche Boubekki <[email protected]> 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)
  • From Amirouche Boubekki@21:1/5 to All on Sun Jul 12 12:50:49 2020
    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)
  • From Paul Rubin@21:1/5 to Maciek Godek on Sun Jul 12 12:26:36 2020
    Maciek Godek <[email protected]> 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)
  • From Amirouche Boubekki@21:1/5 to Nils M Holm on Sun Jul 12 12:51:37 2020
    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)
  • From Maciek Godek@21:1/5 to All on Sun Jul 12 14:59:18 2020
    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)
  • From Bill@21:1/5 to All on Mon Jul 13 10:30:18 2020
    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)
  • From PerBothner@21:1/5 to All on Mon Jul 13 21:48:08 2020
    [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)
  • From Maciek Godek@21:1/5 to All on Fri Jul 17 04:10:11 2020
    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)