I always felt, as a C++ programmer, that Haskell was just restricting me, without providing me any real benefits (of course, other people's opinion can vary!) -- on the other hand, Idris provides tools I can see as useful, things like checking at compile time all file handles are correctly opened before use, and closed after use (that's a very simple example, but just one type of thing you can do)
There was some discussion previously on HN about this https://news.ycombinator.com/item?id=12350273
AFAIK that sounds like unique/linear types, which Idris doesn't provide at this point, it's an experimental/work in progress feature: http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...
There's a tutorial on just this sort of thing here: http://docs.idris-lang.org/en/latest/st/index.html
* It is necessary to open a file for reading before reading it
> Enforced by RAII, create file handle(variable) is equivalent to opening file
* Opening may fail, so the programmer should check whether opening was successful
> If opening file fails, exception is thrown when the handle is created, it is impossible to create/use an unopened handle.
* A file which is open for reading must not be written to, and vice versa
> Can be enforced with different types for reading and writing (ifstream vs ofstream).
* When finished, an open file handle should be closed
> fstream is automatically closed when variable goes out of scope.
* When a file is closed, its handle should no longer be used
> Here it's actually the other way around, the correct way to close a file is to get rid of the last handle refering to it.
> Hence a handle can't be used to write to a closed file since such a handle cannot exist in the first place.
Unfortunately C++ offers no way to track which exceptions any given function might throw and/or enforce that they are handled.
> fstream is automatically closed when variable goes out of scope.
That works for the simple case where the variable exists on the stack of a single function. C++ does not offer safety in the general case where you pass a handle to/from functions, store it in data structures and so on. (You have the option of runtime checks via shared_ptr etc, but at that point you have very little assurance the file ever actually gets closed).
Yes, object lifetime management is not provably safe in c++, due to lack of borrow checker, but that's a general problem for all types of objects, not specifically file management.
True, but introducing invisible partiality to essentially all functions is a pretty stiff cost.
> Yes, object lifetime management is not provably safe in c++, due to lack of borrow checker, but that's a general problem for all types of objects, not specifically file management.
Well, that's a question of language design philosophy. Object management is so much more frequent than any other kind of resource management that it may be worth treating as a special case, as most languages other than C++ do.
Be that as it may, the point is that the really cool thing about Idris is that its type system is powerful enough to let you implement borrow-checker-like functionality in "userspace" rather than needing it built into the language. In theory one could use that (in an Idris-like language with a different record feature, standard library and so on) to have Rust-style manual-but-safe memory management for all objects, though I suspect that might be too cumbersome to be practical.
You must track files by some type already right?
Also, you can already do half of what you described in Haskell. Just require the functions that work over open files to require an Open type which the open function would return.
Not quite. The problem is that values can be copied (AKA used "non-linearly"), for example:
open :: FilePath -> IO Open
readFile :: Open -> IO String
close :: Open -> IO Closed
main = do
-- Open a file handle
o <- open "/tmp/foo"
-- Close "o"
c <- close o
-- Try reading from "o"
s <- readFile o
With linear types, we can make "Open" and "Closed" linear. It's a type error to use a linearly-typed value more than once, which rules out the above double-usage of "o :: Open". It's also a type error to create a linearly-typed value and not use it at all; we can use this when designing an API, e.g. to make a function like:
withFile :: (Open -> (Closed, a)) -> IO a
> things like checking at compile time all file handles are correctly opened before use, and closed after use
Using distinct `Open` and `Closed` types, as you say, doesn't help at all with ensuring file handles are closed after use.
They also don't ensure that handles are correctly opened before use, as I showed with my example `open "/tmp/foo" >>= (\o -> close o >> readFile o >>= putStr)`.
I can't think of a way to ensure both of these things, without using linear or dependent types to track state machines in types.
I can think of ways to ensure one of these things:
- To ensure files are correctly opened, we can remove the ability to close them. My above example would then work correctly, since `close o` would be a no-op, and `readFile` would succeed.
- To ensure all handles get closed, we can remove the ability to open them.
Separating handles into `Open` and `Closed` varieties does nothing more than provide documentation hints to programmers; it cannot automatically check whether handles are used correctly, it requires programmers to consciously avoid language features (like using variables multiple times), be careful about the way they compose functions, and write test suites to check if things are working. In other words, it provides none of the benefits of static typing, and is more akin to documentation in a dynamically typed language.
-- Simon Peyton Jones
Although I understand why Idris is strict by default, there is a part of me that dies a little from that understanding :(
Haskell's laziness undoubtedly works and is useful; you might say it was Haskell's strictness that needed improving.
Just like other languages are strict by default, but can be made lazy via sequences, streams, generators,...
It is just a matter which defaults might be better for a given application.
Feel free to point if I've got any of the above wrong.
Update: Thanks for the replies, people.
In Haskell, the primary mechanism for inducing evaluation is the case expression (if/then/else and pattern matching are syntactic sugar for case).
Thunks (lazy expressions) in Haskell are created with let and then forced with case. It's very straightforward at the most basic level, there's just a lot of abstraction built on top of it that can obscure what's going on.
def foo(a: Bar)(b: a.Baz) = ...
During my time they were a big Haskell shop, working with Glasgow University (the G in ghc). There were also into custom research languages that nobody's ever heard of like Napier and, erm, S-Algol (again with Glasgow; the S stands for 'Scottish')...
I see that Idris generates real machine code. I see it goes through LLVM, so the code quality should be decent; but I see a reference that the binary needs to know where the compiler is, which makes me a bit worried about the needed dependencies.
Additionally, apart from the dependent types, does Idris fix some of the annoyances with Haskell --- modules, namespacing, field access, shudder strings?
- Idris' `String` type is not just a list of characters, here  you can see some relevant functions, I'm still trying to find the definition of `String` though.
- Functions can be overloaded in Idris, which enables declaring a field with the same name on different records.
I'm not sure what you mean with modules and namespacing though
Using LLVM requires that your code is in pretty decent shape before it goes in, really. LLVM is great for replacing your own actual instruction selection, scheduling and assembly, but you can't generate LLVM IR naively from a high-level language and expect LLVM to do anything sensible with it. You seem to basically need a language-specific IR and optimisation passes before you start to think about emitting LLVM. See Rubinius - it implemented a Ruby JIT using LLVM and is often slower than the standard Ruby interpreter!
I found the project fascinating. Of course this a completely different language to Idris, the only real relation is that it was also developed in St Andrews.
At the time I quite liked it, and did a lot of programming in the SunOS version (the one where they hadn't gotten around to writing the garbage collector). I know better now, of course.
Tell me, do you still cringe when you hear the phrase 'void and void are not compatible in this context'?
I wrote my own error messages which were hopefully a bit more useful than that :)
I'd love to see another Haskell-esque language get mainstream adoption. Especially one pushing programming in a new direction.
I love types, I just haven't had the chance to use Haskell in anything but toy applications, the learning curve was very steep but so far rewarding, and led me to miss it in when using the type system hacked onto Erlang/Elixir which is (obviously) lacking as a result. Although still a step forward over other languages. Looking forward to trying out Idris.
Edit: just noticed there's no Kindle version (yet?), that's too bad :(. Maybe MEAP has a licensing deal to exclusively sell the digital versions?
Can Idris be used as a Coq-style "proof assistant"? From reading http://docs.idris-lang.org/en/latest/reference/elaborator-re... , it looks like there was an older proof system that has recently been replaced by something new, and I can't tell if Idris can still be used as Coq replacement. Are there good tutorials on this?
EDIT: It seems like yes, it can be used for proofs? http://docs.idris-lang.org/en/latest/tutorial/theorems.html
And while we're at it, add some arrays, dictionaries and objects in a couple more code examples. That's all we ask for.
Thanks and kudos!
But I agree. A simple hello-world example adds a lot to a language's homepage.
Ruby's homepage, for example: https://www.ruby-lang.org/es/
Imagine C++ template programming with C++ syntax, sane error messages, and ability to use any C++ code.