As a Perl programmer, that name confuses me slightly.
Carp, a compiled Lisp with type inference and a borrow checker
41–50 of 112 posts
Re: Carp, a compiled Lisp with type inference and a borrow checker
#42Others might be interested in Henry Baker's Lively Linear Lisp
[0] HN Discussion. https://news.ycombinator.com/item?id=14248419
Re: Carp, a compiled Lisp with type inference and a borrow checker
#43The borrow checker is the reason to use Rust, in spite of its annoyances (clunky syntax, limited type inference, non-interactive programming, long compilation times, etc.), so it's always nice to see someone trying to provide the upsides of Rust without the downsides.
That being said, your website is disappointingly terse regarding how Carp recovers the advantages of Rust in the context of a Lisp derivative. What makes this particularly suspicious is the fact that, in the past, Lisp programmers have claimed to recover the advantages of other statically typed languages in a Lisp setting, but there have always been huge caveats, like “the system can be very easily circumvented, reducing the benefits of static typing to nothing”.
The main reason why I feel confident that Rust is a safe language isn't just the fact that rustc seems to catch many bugs in practice. That alone wouldn't distinguish it from the countless static analysis tools for C and C++ that have existed for decades. The main reason why, at least in my opinion, Rust is such a trustworthy language in spite of its ginormous complexity, is the fact that its core developers, in particular Niko Matsakis, do a terrific job of communicating the process by which Rust's features are conceived and designed. When you read Matsakis' blog [0], it becomes patently clear that Rust's developers take into account the kind of corner cases that in many other languages are only discovered months or years after the feature has been implemented [1][2].
Other languages that inspire similar confidence in me are:
(0) Standard ML. It has a formal proof of type safety.
(1) Pony. It has a formal proof of type safety.
(2) Haskell, as specified in the Haskell Report (i.e., without the crazy GHC-specific language extensions), because its type system is similar to Standard ML's, and there are no reasons to believe the differences introduce any type safety holes.
(3) OCaml, again without the crazy extensions (GADTs, first-class modules, etc.), for more or less the same reasons as Haskell.
Links:
[0] http://smallcultfollowing.com/babysteps/
[1] http://joyoftypes.blogspot.pe/2012/08/generalizednewtypederi...
Re: Carp, a compiled Lisp with type inference and a borrow checker
#44Very excited about Carp. In general I like the simplicity of Lisp but ironically I'm not a fan of dynamic typing. Carp may be a real innovation. A bit surprised though that the Carp C runtime functions are not namespaced. With names like `IO_println` there's a risk of clashes. Unless the compiler is doing some tricks to hide names?
The ”IO_” part is the namespace, so no clashes!
It's not enough :-) Ask the OCaml folks, they're going through this pain right now because their stdlib modules are called `Array`, `List`, and so on. They're planning to put them all under `Stdlib`, so e.g. `Stdlib.Array` and so on, but it's going to be a big effort with a lot of pain.
The main problem will arise when users create their own libraries; suppose some people create a `Option` libraries and then later you want to add a standard option type to Carp, it will be painful. Better to namespace your stuff under `Carp` from the beginning, so e.g. `Carp_IO_println`, `Carp_Option_map`, and so on.
Re: Carp, a compiled Lisp with type inference and a borrow checker
#45The borrow checker is the reason to use Rust, in spite of its annoyances (clunky syntax, limited type inference, non-interactive programming, long compilation times, etc.), so it's always nice to see someone trying to provide the upsides of Rust without the downsides. That being said, your website is disappointingly terse regarding how Carp recovers the advantages of Rust in the context of a Lisp derivative. What mak…
> in the past, Lisp programmers have claimed to recover the advantages of other statically typed languages in a Lisp setting, but there have always been huge caveats, like “the system can be very easily circumvented, reducing the benefits of static typing to nothing”.
It seems to me that the benefits of static typing only apply to accidental mistakes (e.g. using a pointer to a character as though it were an integer, or a pointer to a struct, or whatever), and thus that a system with deliberately-circumventable static typing is just fine.
Re: Carp, a compiled Lisp with type inference and a borrow checker
#46I realize that almost every language could be described as a subset of C++, but I read articles like this and think... Deterministic language that has type inference, C interop, and uses ownership to govern object lifetimes? We have that. It's C++11. auto with std::unique_ptr and std::move(). Only slightly serious. ;-)
So Carp could compile to that subset of C++. But C++11 isn't _just_ that. It is all of C++11. C++ would even more successful if it was easy to make a proper subset of it.
That's what the GSL was supposed to be
https://github.com/Microsoft/GSL
It seemed really cool. All compile time checks. I have no idea why it didn't take off
Re: Carp, a compiled Lisp with type inference and a borrow checker
#47This project looks really good. I would love to have a clojure inspired lisp that's fast and doesn't require the JVM.
Re: Carp, a compiled Lisp with type inference and a borrow checker
#48Earlier quoted context omitted.
I would argue the immutability is actually not a great thing in Erlang to be honest. It makes it hard to reason about what gets copied, what gets shared in the global heap which may be a source of contention, makes code unnecessarily verbose, etc. I think it's one of those features (like lazy evaluation in Haskell) that language practitioners tend to advocate without necessarily understanding what tradeoffs they are…
It actually makes reasoning easy. What gets copied: everything. What gets shared: nothing.
That's not true in a number of cases, and thankfully what you said isn't right or the BEAM would truly be a disaster.
Re: Carp, a compiled Lisp with type inference and a borrow checker
#49The borrow checker is the reason to use Rust, in spite of its annoyances (clunky syntax, limited type inference, non-interactive programming, long compilation times, etc.), so it's always nice to see someone trying to provide the upsides of Rust without the downsides. That being said, your website is disappointingly terse regarding how Carp recovers the advantages of Rust in the context of a Lisp derivative. What mak…
> in the past, Lisp programmers have claimed to recover the advantages of other statically typed languages in a Lisp setting, but there have always been huge caveats, like “the system can be very easily circumvented, reducing the benefits of static typing to nothing”. It seems to me that the benefits of static typing only apply to accidental mistakes (e.g. using a pointer to a character as though it were an integer,…
All mistakes are accidental. Seldom do people write a line of code thinking, "I'm making a mistake." If your language encourages people to casually write unsafe code, any time you spent on safety guarantees was wasted because those guarantees disappear in all of that code and all of the code that touches it. And that's a lot of space for mistakes.
Re: Carp, a compiled Lisp with type inference and a borrow checker
#50The borrow checker is the reason to use Rust, in spite of its annoyances (clunky syntax, limited type inference, non-interactive programming, long compilation times, etc.), so it's always nice to see someone trying to provide the upsides of Rust without the downsides. That being said, your website is disappointingly terse regarding how Carp recovers the advantages of Rust in the context of a Lisp derivative. What mak…
> in the past, Lisp programmers have claimed to recover the advantages of other statically typed languages in a Lisp setting, but there have always been huge caveats, like “the system can be very easily circumvented, reducing the benefits of static typing to nothing”. It seems to me that the benefits of static typing only apply to accidental mistakes (e.g. using a pointer to a character as though it were an integer,…
> It seems to me that the benefits of static typing only apply to accidental mistakes (e.g. using a pointer to a character as though it were an integer, or a pointer to a struct, or whatever), and thus that a system with deliberately-circumventable static typing is just fine.
Static typing is useful to enforce the integrity of abstractions across large systems. For instance, using (language-enforced) abstract data types, you can confidently say that a 50 KLOC program won't destroy the invariants of a complicated data structure, because the only place where this could hypothetically happen is a 1500 LOC module, and these 1500 LOC have been verified to the death. Elsewhere, the internal representation of this data structure isn't accessible. Before anyone claims this can be done using object-orientation: No. Object-orientation allows the creation of ill-behaved impostors that are indistinguishable from well-behaved objects unless you use expensive dynamic checks or even more expensive whole-program (and hence non-modular) analyses.
Static typing is also useful to enforce the exhaustiveness of case analyses. Disregarding memory safety issues, which are largely a nonproblem in high-level languages, the vast majority of bugs in computer programs arises from failing to identify corner cases or fully comprehend their complexity. Algebraic data types allow you to substitute ad hoc case analyses with induction on datatypes, for which mechanical exhaustiveness checks are possible, and, in fact, actually performed in practice.
Static typing is also useful as an aid to program verification. Program properties of interest can be classified in two groups: safety properties and liveness properties. Safety properties assert that “bad states are never reached”, and are largely covered by type soundness (for non-abstract types) and type abstraction a.k.a. parametricity (for abstract types). Liveness properties assert that “good states are eventually reached”, and, while types provide less support for verifying liveness properties than safety ones, at least induction on datatypes provides a easy-to-use tool to verify that non-concurrent (but possibly parallel) algorithms will terminate.
All of these benefits fly out of the window if static typing can be circumvented.