For anyone wondering what Idris is, it's pretty much Haskell with dependent types. That is, it's easy to encode thing like "vector of length n" in the type system, so you can go from
concat :: Vec -> Vec -> Vec
to
concat : Vec n -> Vec m -> Vec (n+m).
Yes, but it turns out you can do some cool things with dependent types.
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)
Your example (and more) can be achieved by linear types which are coming to Haskell: "The patch is currently under 1000 lines long. We are targeting a merge by the time of the 8.4 release of GHC." http://blog.tweag.io/posts/2017-03-13-linear-types.html
As I understand it, one selling point of Idris' type system is that it's actually simpler than haskell as it's based on a single very generic concept that covers a wide range of applications, rather than a sum of specialized things.
While dependent type inference is more difficult, you get program inference in exchange. That's not a bad tradeoff because I'd rather write the spec (type) and have the computer fill in the boring bits, rather than the other way around.
I remember seeing an Edwin Brady talk (it featured a now-possibly-famous Brexit joke) in which the compiler almost inferred ... I think it was either zip or a fold.
I've seen this over and over but it's false. Adding dependent types do not negatively affect type inference for the non-dependent fragment in any shape or form. On the contrary, Agda/Coq type inference is far more powerful than in Haskell. While Agda/Coq do not have let generalization, that is by purely a design decision and not some kind of limitation.
Highly generic code yields complicated signatures, so even if it's good style to add those signatures for top level declarations, it's really good to have the compiler help you figure out what that signature is.
> 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)
Tracking state (sort of like Typestate) is not part of the type system, but you can encode it in the type system. So far, I've found this much more usable in practice than linear types, but I expect future work on linear types will change this, especially now that they're coming to GHC.
C++ (if not used as C with classes) is built around RAII and will also enforce file handles to be opened before use and automatically closed when leaving scope (no longer in use).
Now std::ifstream isn't 100% idiomatic RAII (because constructor sets error state instead of throwing and it also provides open/close-methods) but generally you should be able to encode a safe file handle into the c++ type system. Here is how i would compare it to what idris describes in https://media.readthedocs.org/pdf/idris/latest/idris.pdf
* 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.
> If opening file fails, exception is thrown when the handle is created, it is impossible to create/use an unopened handle.
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).
Checked exceptions would be neat but still, if you don't catch the exception it will be propagated further up the chain, so the claim that it is impossible to create an unopened file handle still holds :)
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.
> Checked exceptions would be neat but still, if you don't catch the exception it will be propagated further up the chain, so the claim that it is impossible to create an unopened file handle still holds :)
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.
But you either have to use unique ptr (then passing the pointer around is a pain), or shared ptr (then you pay a runtime cost of counting). In idris the type system deals with these things better.
I'm not sure that is quite a simple example actually. Sounds kind of complex to prove that all file handles are closed after use (how soon after use?) in the general sense, especially when they're opened dynamically.
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.
> 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
putStr s
This program will type-check, since "o" has type "Open", so it's a valid input to "close" and to "readFile". The problem is that the type system has no idea that calling (the IO action returned by) "close o" makes subsequent uses of "o" invalid, even though it still has type "Open".
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
The only way to call this function is to provide it with a function of type `Open -> (Closed, a)`. If we've encapsulated our implementation details, then the only way to write a function which returns a `Closed` is to have it call `close :: Open -> Close`. Since values of type `Open` can't be re-used, this must either be its argument or the return value of some call, e.g. `readFile :: Open -> (Open, String)` or `writeFile :: String -> Open -> IO Open`, which in turn require an `Open` argument, and so on; forcing a chain of operations, culminating in a `close`.
Yes, but your approach doesn't actually solve any of the requirements:
> 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.
Yes, but not because laziness was a technical failure, but for something more resembling PR reasons. Haskell's laziness by default ends up being a large stumbling block for many developers not used to thinking in that way.
Although I understand why Idris is strict by default, there is a part of me that dies a little from that understanding :(
It's not so much a PR failure, as an ergonomics issue -- making laziness the default makes it too easy for people to create performance problems for themselves.
Haskell's laziness undoubtedly works and is useful; you might say it was Haskell's strictness that needed improving.
What does strict mean in this context? I don't know too much about these concepts. I think lazy means only evaluated when needed, like in generators (using Python as an example, which I know - I don't know Haskell or Idris). And I thought (from what little I've read), that the opposite of lazy evaluation was eager evaluation. So in Python at least, an example of eager vs. lazy would be returning a list vs. returning a generator from a function. For the former (list), the whole list would have to be created/populated and then returned (thereby occupying memory for the duration of its use), whereas for the latter (generator), items from it would only be yielded on demand, e.g. one at a time, when next() is called, or when the generator is iterated over, and so would not use as much memory as needed for the sum of the sizes of the items in the list. So where does strict fit in here?
Feel free to point if I've got any of the above wrong.
Strict evaluation is a synonym for eager evaluation.
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.
Most, possibly all, of what you do in Idris can be encoded into Scala, but working with type-level functions become very cumbersome. The compiler doesn't understand that a type-level function is a function, so every time you apply a function to a type and need to know the result is the same as itself you have to summon evidence that this is so (which also sends compile times through the roof). Higher-kinded types get treated differently for equality unless you encode them as members of wrapper types. You end up having to write all your type-level stuff in a kind of continuation-passing style and defining intermediate types to represent each step of your algorithm.
Idris' dependent types are more powerful, though @edwinb would probably be the one to explain the differences in detail (he gave a talk awhile back on Scala vs. Idris).
no. in idris you can declare a functions that takes integers less than five, and if you write code that can eve theoretically allow that function to get called with 5 or greater you get a compiler error. things like that
Another way to think of it is that types are first class. Here's an example I found of returning a type, although I forget where I found it. It's a version of a sample on the Rust page, but it now handles floats if necessary: https://paste.fedoraproject.org/paste/UTrEje4Czbiq8C0u1oJOnF...
There are other differences too. The syntax is very very close, but how it handles things like evaluation is different. Don't assume that just because they look the same that they are.
Hey, this is out of the University of St.Andrews! I went there!
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 [1] 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!
RE S-Algol, it actually stands for St Andrews Algol. I developed a javascript transpiler as my final year project (2016) which is incomplete but there are some working examples here: https://goo.gl/TjbwML .
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.
I could have sworn it was 'Scottish', because that meant that the language wasn't entirely St.Andrews' fault, but it was nearly twenty years ago...
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'?
Aha that's probably wishful thinking I'm afraid. The language seemed very old fashioned to me (features like being able to choose the first index of an array) but I can appreciate it was good for its time.
I wrote my own error messages which were hopefully a bit more useful than that :)
The linked book has a freely available chapter 13 available that shows how to create state machines with dependent types. Of course its easy in any language, but with Idris you can ensure at compile time that all state transitions in a program are valid.
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?
That's what happen for every Manning publication. Only the paperback version is available on amazon. On the other hand, if you buy it on manning, you'll get a pdf and an epub version.
Congratulations on the big milestone! This really appeals to the same part of my brain that likes (to varying degrees) Haskell, Rust and TypeScript.
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?
Look guys, I love to see new languages every single day, I am a fan of language design but for the love of god, can you post at least a HelloWorld program in the front page?
And while we're at it, add some arrays, dictionaries and objects in a couple more code examples. That's all we ask for.
Did you not look at the examples section, the documentation, the tutorial, or notice that there's a several-hundred page book on software development in Idris? There's no shortage of code examples.
My understanding of the promise of Idris is that anything you _want_ to put into the type definitions for your application, you _can_ put into the type definitions.
