Would be nice to see a dependently-typed strict functional programming language that didn't require a GC or a C runtime. Are there any plans for this with Idris?
Function programming with no garbage collector is tough. There is a formalisation for dealing with this, called linear logic, which allows you to statically determine object lifetimes; but it's, um, a bit awkward. Such as, every value must be produced once and consumed once, so if you want to look at a variable, you need to produce a new variable with the same value (which must be consumed later).
The seminal linearly typed language is Linear Lisp, which is almost incomprehensible, and also a proof-of-concept which doesn't do anything useful. Classic paper here:
The closest thing to a modern language that uses them exclusively (Rust doesn't, by the way) is LinearML, which was an experimental toy, now abandoned. Tutorial here, which may be interesting:
In what way is Rust's use of affine lifetimes insufficient to implement "function programming with no garbage collection"? Genuine question, given my previous interest :)
In Rust you're allowed to look at values without consuming them, which pure linear typing doesn't support (it requires exactly one producer and exactly one consumer).
Also, in my experience, most Rust programs tend to stash stuff in reference-counted boxes whenever calculating lifetime gets complex; which is reasonable enough (C++ does the same thing), but it is basically garbage collection, and I'd like to find an expressive, functional, non-GCd language which doesn't require this.
We have plans to implement a framework for writing high performance, GC free programs in Lean (http://leanprover.github.io/). We have spent the last year addressing shortcomings of the previous version and will be shipping a new version early next year. The new features include a high performance proof automation framework, a native compiler, a profiler, a debugger, an incremental build system, a documentation tool, an FFI, including a bunch of goodies I am probably forgetting. We will be demoing Lean this year at POPL (http://popl17.sigplan.org/track/POPL-2017-Tutorials#program), and hope to cut a release ASAP.
You could look at ATS. I don't know a huge amount about it but I know it's a very high-performance bare-metal language with dependent types, or at least, more expressive types than Haskell/ML.
(Caveat: I've never written ATS, and although I've written in Coq and Idris, every time I look at ATS code it looks like complete gibberish).
Most of the ATS examples begin with something which looks like ML, but as the types are made more and more strict they end up looking like incredibly verbose C.
To make things worse, I don't think ATS has any inference either, so all of this must be written explicitly. Idris, Agda, Coq, etc. can infer types and values, if they're unambiguous.
For example:
Definition Prime p := forall n m, n * m = p -> n = 1 \/ m = 1.
All of these variables have type nat, which Coq can infer from the use of "*" and "=".
I’ve been working sporadically on a strict stack-based functional language called Kitten, with the goals of avoiding GC and libc. No plans for dependent types, but you might like to keep an eye on it anyway: https://github.com/evincarofautumn/kitten
