4 ms·

I completely agree and I wish we could have the best of both worlds. I love Clojure and I love the compiler support with static typing in other languages. Cloj

I completely agree and I wish we could have the best of both worlds. I love Clojure and I love the compiler support with static typing in other languages. Clojure attempted to add static typing with the core.typed projects, but high-profile exits [0] from that framework have made clear that this is a problem that can only properly be implemented at the language level. If I could have a lisp with static types, I might not use anything else again. [0] https://circleci.com/blog/why-were-no-longer-using-core-typed/ https://circleci.com/blog/why-were-no-longer-using-core-type...

_yosefk 10y ago
Common Lisp has static types.
- groovy2shoes 10y ago
  And Racket. And Shen.
  - klibertp 10y ago
    Also Irken: http://www.nightmare.com/rushing/irken/irken/lang.html http://www.nightmare.com/rushing/irken/irken/lang.html
    - ZenoArrow 10y ago
      Irken looks interesting, thanks for the link.
- reikonomusha 10y ago
  But not good parametric polymorphism. Common Lisp's static types are "too static", and often unsafe.
  - junke 10y ago
    Ok for parametric polymorphism: the identity function in OCaml has type 'a -> 'a, whereas in SBCL it is "(function (T) T)". On the other hand, "(lambda (x) (if x 0 1))" is a function from T (anything) to the type BIT, not to some arbitrary integer type. Moreover: (lambda (x) (unless (minusp (if x 0 1)) (error "Oops"))) ... has type "(function (T) NIL)", meaning that the function does not return a value. That means that types are propagated so that the test can demonstrably always fail. A type in SBCL defines what is returned when execution terminates normally. So for example the type of `(lambda (x) (loop))` is "(function T NIL)", because it never returns (yes, I know you cannot always tell if it halts or not). The bottom type NIL should not be confused with NULL, the singleton type for the NIL value. In OCaml, exceptions are not visible by the type system and you can write: let f x = raise (Failure "NO") ... and still have the type 'a -> 'b So the kind of analysis that make sense in a language, as well as their soundness, is relative to the properties you want to check. Would you say that OCaml type system is unsound because it allows you to run code that can raise exceptions at runtime? I would love to see more precise type checking in OCaml, for example, and it probably already exists (I'am interested, if anybody has an example). But it probably makes little sense over there. The same goes for parametric polymorphism in Lisp. The most in-depth approach to bring parametric polymorphism in CL is LIL (https://common-lisp.net/~frideau/lil-ilc2012/lil-ilc2012.html https://common-lisp.net/~frideau/lil-ilc2012/lil-ilc2012.htm...), but since it is dynamic, people who view dynamic typing as a deficiency might see that as a restriction. You also claim that the type system is "unsafe". On the contrary, types being checked at runtime is a safe approach (buffer overflow, etc.) and plays well with the fact that everything can be redefined at runtime (maybe you don't like this aspect). In SBCL, type declarations are assertions. With the default optimization levels, that means that if they cannot be proved, they are checked at runtime (with the few caveats listed in SBCL man page). So if your input variable X is type as NUMBER and the function terminates normally, then you know that X effectively was of type NUMBER (that's a guarantee instead of an assumption). That result can be used in the following calls so that checking the type of X is not necessary anymore (if it is not modified in the meantime). The only case where types are trusted blindly instead of being checked, when necessary, is when you set the safety level to zero. This can be changed locally, not necessarily as a global switch.
    - 10y ago
deleted 10y ago
[deleted]

_yosefk 10y ago

Common Lisp has static types.

groovy2shoes 10y ago
And Racket. And Shen.
- klibertp 10y ago
  Also Irken: http://www.nightmare.com/rushing/irken/irken/lang.html http://www.nightmare.com/rushing/irken/irken/lang.html
  - ZenoArrow 10y ago
    Irken looks interesting, thanks for the link.
reikonomusha 10y ago
But not good parametric polymorphism. Common Lisp's static types are "too static", and often unsafe.
- junke 10y ago
  Ok for parametric polymorphism: the identity function in OCaml has type 'a -> 'a, whereas in SBCL it is "(function (T) T)". On the other hand, "(lambda (x) (if x 0 1))" is a function from T (anything) to the type BIT, not to some arbitrary integer type. Moreover: (lambda (x) (unless (minusp (if x 0 1)) (error "Oops"))) ... has type "(function (T) NIL)", meaning that the function does not return a value. That means that types are propagated so that the test can demonstrably always fail. A type in SBCL defines what is returned when execution terminates normally. So for example the type of `(lambda (x) (loop))` is "(function T NIL)", because it never returns (yes, I know you cannot always tell if it halts or not). The bottom type NIL should not be confused with NULL, the singleton type for the NIL value. In OCaml, exceptions are not visible by the type system and you can write: let f x = raise (Failure "NO") ... and still have the type 'a -> 'b So the kind of analysis that make sense in a language, as well as their soundness, is relative to the properties you want to check. Would you say that OCaml type system is unsound because it allows you to run code that can raise exceptions at runtime? I would love to see more precise type checking in OCaml, for example, and it probably already exists (I'am interested, if anybody has an example). But it probably makes little sense over there. The same goes for parametric polymorphism in Lisp. The most in-depth approach to bring parametric polymorphism in CL is LIL (https://common-lisp.net/~frideau/lil-ilc2012/lil-ilc2012.html https://common-lisp.net/~frideau/lil-ilc2012/lil-ilc2012.htm...), but since it is dynamic, people who view dynamic typing as a deficiency might see that as a restriction. You also claim that the type system is "unsafe". On the contrary, types being checked at runtime is a safe approach (buffer overflow, etc.) and plays well with the fact that everything can be redefined at runtime (maybe you don't like this aspect). In SBCL, type declarations are assertions. With the default optimization levels, that means that if they cannot be proved, they are checked at runtime (with the few caveats listed in SBCL man page). So if your input variable X is type as NUMBER and the function terminates normally, then you know that X effectively was of type NUMBER (that's a guarantee instead of an assumption). That result can be used in the following calls so that checking the type of X is not necessary anymore (if it is not modified in the meantime). The only case where types are trusted blindly instead of being checked, when necessary, is when you set the safety level to zero. This can be changed locally, not necessarily as a global switch.
  - 10y ago

deleted 10y ago

[deleted]