Type strategy for Scheme
Lassi Kortela
(09 Nov 2022 22:54 UTC)
|
Re: Type strategy for Scheme
Marc Nieper-Wißkirchen
(10 Nov 2022 07:07 UTC)
|
Re: Type strategy for Scheme
Marc Nieper-Wißkirchen
(10 Nov 2022 07:42 UTC)
|
Re: Type strategy for Scheme
Peter Bex
(10 Nov 2022 08:05 UTC)
|
Re: Type strategy for Scheme
Philip McGrath
(10 Nov 2022 08:54 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(10 Nov 2022 09:49 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(10 Nov 2022 09:08 UTC)
|
Re: Type strategy for Scheme
Marc Feeley
(10 Nov 2022 23:34 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(11 Nov 2022 19:17 UTC)
|
Re: Type strategy for Scheme
Marc Feeley
(11 Nov 2022 21:34 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(12 Nov 2022 21:58 UTC)
|
Re: Type strategy for Scheme Marc Nieper-Wißkirchen (12 Nov 2022 22:52 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(12 Nov 2022 23:14 UTC)
|
Re: Type strategy for Scheme
Marc Nieper-Wißkirchen
(13 Nov 2022 09:41 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(13 Nov 2022 11:59 UTC)
|
Re: Type strategy for Scheme
John Cowan
(13 Nov 2022 19:52 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(13 Nov 2022 20:22 UTC)
|
Re: Type strategy for Scheme
Marc Nieper-Wißkirchen
(13 Nov 2022 20:35 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(13 Nov 2022 21:41 UTC)
|
Re: Type strategy for Scheme
Marc Feeley
(14 Nov 2022 00:03 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(14 Nov 2022 09:36 UTC)
|
Re: Type strategy for Scheme
Marc Feeley
(14 Nov 2022 16:27 UTC)
|
Re: Type strategy for Scheme
Lassi Kortela
(14 Nov 2022 19:58 UTC)
|
Re: Type strategy for Scheme
John Cowan
(13 Nov 2022 20:40 UTC)
|
Re: Type strategy for Scheme
Marc Nieper-Wißkirchen
(13 Nov 2022 20:42 UTC)
|
Re: Type strategy for Scheme
Panicz Maciej Godek
(20 Nov 2022 21:59 UTC)
|
Re: Type strategy for Scheme
Per Bothner
(20 Nov 2022 22:58 UTC)
|
So are you looking for some ML dialect with parentheses? This is a serious question. I wonder how much such a Scheme would differ from ML. Am Sa., 12. Nov. 2022 um 22:58 Uhr schrieb Lassi Kortela <xxxxxx@lassi.io>: > > > For #2 it is important to widen the notion of a type. A type is theoretically a set of possible values. This means that a range of values, like 0..9, and even a singleton, like 42, are types. With this point of view on types, type analysis subsumes constant folding so that the type of (* x y) is the singleton type 42 when x has the singleton type 6 and y has the singleton type 7. Moreover, if x and y are known to have type 0..9 then the overflow check on (* x y) can be eliminated because the result is of type 0..81, something that is important for performance. > > > It would be more correct to say that the length of a vector is part of its type, but most languages’ static type systems are not powerful enough to express that type (so that in reality any “type error” on the index must be detected at run time). > > Yes, you could put all static invariants into the type system. As far as > I can tell this is the main idea behind dependent types. > > It's less clear what to do about things like a resizable vector. In > Smalltalk and CLOS you can even change the class of an object at > runtime. Common Lisp has a (satisfies p) type where p is a predicate > function, so you can do runtime checks. That aspect is more expressive > than what can be done in a static type system. > > > It would be more correct to say that the length of a vector is part of its type, but most languages’ static type systems are not powerful enough to express that type (so that in reality any “type error” on the index must be detected at run time). > > The cognoscenti make a distinction between "types" and "classes" for > these kinds of debates. I can't tell whether it's a legitimate point or > a misdirection to conceal the downsides of their favorite type systems. > > > A statically typed Scheme will probably impose lots of constraints on what can be expressed, to the point of hampering the typical Scheme programming style. Take lists for example. Some say that lists are the “universal data structure” because all kinds of information can be represented in them: > > > > ;; lists of primes… should be fairly easy to statically type (but is it a list of integers, or a list of numbers, or a list of positive exact integers?): > > '(2 3 5 7 11 13) > > > > ;; poker hand… not so easy to statically type (mixes symbols and integers): > > '((spades king) (clubs 7) (hearts ace) (hearts 7) (clubs queen)) > > A ML or Haskell coder would replace the inner lists with tuples (or use > records, which are essentially named tuples). We don't have tuples in > Scheme and Lisp since we don't really need them. A tuple is like > first-class multiple values; SRFI 195 (Multiple-value boxes) comes close. > > Python is a dynamic language which has an explicit tuple type but it's > hard to demonstrate the importance of the type to dynamic programmers. > It looks a bit out of place. "Why does Python have two list types, one > that is a normal list and one that is weirdly inconvenient?" > > > ;; an s-expression to pass to eval: > > '(if (< x 0) (abs x) (string-length "hello!")) > > > > I could go on and on with other examples of this idiom we take for granted in Lisp/Scheme programming (representing complex data with lists). > > The major failing of static types is that everything must be known in > advance. You'd need to enumerate every possible kind of Scheme datum in > a union type at compile time. > > This is alleviated by bolting on an extra layer to the type system > (typeclasses, modules, traits, interfaces, etc.) at the cost of > increased complexity and slower compilation. > > > Of course you could design a Scheme subset where these things would no longer be allowed, but I think it would be so crippling that it would be of little use for practical use in Scheme code. > > > Could you explain how this issue could be addressed? > > Static typing is more of a burden than a help without type inference and > correctness and exhaustiveness checking. If you make the type system > more permissive and expressive, it can do less of all these good things. > > No one seems to have resolved this fundamental tension satisfactorily. > Racket, Common Lisp, and Python opted to use "gradual typing". > Everything is dynamic by default and you can add type hints, but > "well-typed" code is not enforced. > > In Scheme we have a similar tension in macros. `define-macro` lets you > use everything in normal Scheme but does not help with safety. Hygienic > macros offer varying levels of help, but the easier it is to be safe, > the more the macro language deviates from normal Scheme. Syntax-rules is > safest, but it's a completely different language. Type systems are > similar: Hindley-Milner without any add-ons is rock solid, fast, and > simple, but it's like coding in a straitjacket. Like syntax-rules, you > have to unlearn old habits and it can't express everything. > > I expect that the most satisfying solution is to have a separate dynamic > and static language (the latter H-M based) with similar surface syntax > and good interop. Many Lispers will probably think gradual typing is the > only acceptable option. We should try both.