12 ms·
Notes on Idris (2017)
- icebraining 8y agoa simple program took 25 seconds or more to build This is surprising, I haven't had that experience, although I've been using the JavaScript backend instead, maybe it's much faster? It takes a few seconds, but not that much, and I'm on mere X220. Like the author, I also struggle to write clean code in it. I've been writing a personal project to learn functional programming, Idris, Lambda and DynamoDB, and it's been going slowly. Reading the book, and embracing the suggested development method (type, define, refine) has been helpful, and I'm enjoying the whole process, despite a couple of snags with the JS interface.
- iainmerrick 8y agoI was nodding along until I hit that point too. 25 seconds for a simple program??!? That would be a complete dealbreaker.
- fiddlerwoaroof 8y agoIt’s not as bad as it sounds because you don’t have to compile your program while you write it. Rather, you send the program to a repl and the type checker tells you about problems. You can even run the total parts pretty quickly in the repl. The only issue is that the language server seems to have a memory leak or something that leads to it taking a huge amount of memory and getting sluggish over the course of an extended development session.
- gameswithgo 8y ago>The only issue is that the language server seems to have a memory leak or something that leads to it taking a huge amount of memory and getting sluggish over the course of an extended development session. that is not good advertising!
- fiddlerwoaroof 8y agoI'm sort of hoping someone here will tell me that I'm doing it wrong. Because, this has always been the showstopper for me.
- iainmerrick 8y agoThe language sounds very interesting otherwise, so I’d like to hear of any fixes or workarounds too.
- edwinb 8y agoThere are various reasons why Idris is slow, but it generally comes down to it being because the current system is the result of lots of experimentation about how to even implement a dependently typed language in the first place, and what it should look like. It needs quite a bit of re-engineering - I prioritised ease of playing with features over efficiency. The good news is that I'm working on a new version, taking into account the many things I know now that I didn't when starting on version 1. Don't hold your breath though, it might take a while... In the end, it's a research project, and our job isn't so much to make a good product as to get people excited about the ideas. Mostly we do this by trying to be obviously having lots of fun. But I'd still like a better implementation, because then we can have even more fun.
- moistoreos 8y agoDoes Haskell do this?
- fiddlerwoaroof 8y agoDo what? The memory leaks? No, GHC is an extremely solid system. There are various editor integrations for Haskell that make it easy to bounce between coding and experimenting in the REPL, though.
- moistoreos 8y agoyes, memory leaks. thanks for answering my question my dude.
- star-castle 8y ago2015 MacBook Pro, compiling his 'first cut at it' example: # time idris -o Foo Foo.idr real 0m31.683s user 0m30.646s sys 0m0.876s
- alexashka 8y agoI've also bought and worked through the book. It's excellent. My conclusion was that Idris is an academic language (lack of libraries), followed by realizing that the parts of Idris that I like, are almost all covered by Haskell extensions. For me, Idris is a great peek into what Haskell should/could be, if extensions were better documented and the synergy between them, explained to mere mortals.
- pjmlp 8y agoFor me it was also very interesting read, and I also reached a similar conclusion. Such language features are still too complex for the regular kind of software development many of us do, as the whole team has to fully grasp it.
- moosefish 8y agoAny thoughts on Agda? I've always thought that since it's embedded in Haskell, even though it's less 'practical' than Idris it would benefit from the extensive libraries that Haskell brings to the table.
- Zalastax 8y agoUsually, Agda programs would not use Haskell libraries very much, even though they could. The reason seems to be that it is an unstable language and we are still figuring out how to do dependent types correctly. To me, working in Agda is like working in a very powerful version of Haskell, but for most people it's more about working in a research language. Idris and Agda are quite similar: don't build a company on them, but expect really cool ideas to spawn from them. Dependent types is really an awesome idea.
- fiddlerwoaroof 8y agoI’ve often thought Idris would be useful for expressing the core business logic of your program, and the you’d use the Haskell or JS backend to do the user-facing parts.
- KirinDave 8y agoI've got a few network services working with Idris and they run okay. The compilation time grows so quickly you can't use it for very large projects though. Honestly, Haskell dependent-typing is SO MUCH MORE COMPLEX than Idris's "well what if I just write a function that takes a type?" approach, it's not even funny. Even the author of singleton says it's a rough landscape. Haskell's going to get much closer with QuantifiedConstraints in ghc 8.6, in that it'll simplify a lot of this work, but it's still years out from the simplicity and library unification.
- ainar-g 8y agoRecently I talked with my cousin, who is also a software engineer, about dependent types, contract programming, invariants, and all that. Among other things I've told him about "type-safe printf" that you can write in Idris. He then asked me, why are there only purely functional languages with this feature. I had no actual answer. So, does anybody know, why there still isn't a "C/Go/Java with dependent types"? There is support for runtime checking via invariants in e.g. D, but no pre-compile-time checker. Another question, is there (probably commercial) software that allows you to augment your code with invariant annotations and then check them as a pre-compilation step?
- alexashka 8y agoDependent types are a solution in search of a problem. Widespread adoption comes from an easy to use, backed by big name, solution to a problem people have been having. Typescript is a good example - it came with VS Code integration out of the box, and some decent tutorials. It solves the problem of catching dumb type mismatch bugs at compile time, gives jump-to-definition, auto-complete and doesn't cost anything, it's opt-in. Those are killer usability features! Dependent types give type theorists a place to try interesting things. That's about it so far. Regarding invariant annotations - people call those tests :)
- nine_k 8y agoMaybe the typical "pedestrian" problems, like lists having non-zero length, or numbers being in a given range, can be checked statically with simpler means that full-on dependent types? E.g. safe resource deallocaion problem can be seen as a dependent-type problem (only let an initialized resource into a deallocator), but is usually solved with sort-of linear types, or even simpler (though more crude) means.
- dnomad 8y agoIt's not clear that dependent types even are types. Does a zero-length list offer a different methods than a list that contains some elements? Does the compiler magically eliminate the 'remove()' method and then add it back when you add some elements? The entire domain is highly dubious and the people researching it are often of ill repute.
- kqr 8y agoSlightly unrelated but if all you do is stick around in do notation, you will not see why Haskell is the greatest imperative language. That starts happening once you break out of the traditional notation.
- cannam 8y agoCan you expand on that?
- kqr 8y agoI wish I could. Honestly! It's just that while I have experienced it firsthand, I have not spent enough time thinking about it and tinkering with it to be able to succinctly and accurately put into words what it is about. Some loose thoughts that may or may not make sense: - In Haskell, effectful computations (such as prints, variable updates, and so on) are first-class values (like integers, strings, and so on). This is the big idea. - When effectful computations are first-class values, you can store them in data structures like lists. You can associate them with keys in maps. You can even stick them in priority queues. - When effectful computations are first-class values, you can pass them around as arguments, or send them off as return values. - When effectful computations are first-class values, you can transform their results, you can chain them together and you can create branches in them. - When effectful computations are first-class values, you can perform them, then perform then again, then perform them 12 times, then discard them. Or discard them first and never perform them. - When effectful computations are first-class values, you have decoupled "describing the action" from "executing the action". You can handle the effectful computation without being afraid of performing the effect. - When description is decoupled from execution, you can abstract over the flow of control. You can have a loop that doesn't always increment its counter, because the incrementing operation is specified in a list somewhere instead. - Abstracting over the flow of control can be about as confusing as it is dynamic and powerful. It can also be the most clear and obvious solution to some problems. - Effectful computations as first-class values is a little like functions as first-class values: when you have tried it, you've found it's so convenient that you'd like to have it everywhere. (It's also a little like first-class functions in the sense that you can emulate first-class effects with first-class functions, but it easily becomes unwieldy.) - Effectful computations as first-class values is even a little like Lisp metaprogramming. In Lisp, the flow of control can be rewired dynamically, because the code itself is a Lisp data structure. In Haskell, the flow of control can be rewired dynamically, because statements don't have to be executed the second you see them. - The do notation, when used the traditional way, pulls a curtain over how effectful computations are first-class values. Computations in do notation are (to a first approximation) executed as soon as they are seen, because do notation was designed to intentionally hide the ways in which Haskell is a more powerful imperative language. Sorry if that made things even more confusing than it cleared up. ---- Here's the most basic concrete example I can think of: repeated = do { putStrLn "Hello"; putStrLn "Hello"; } Huh, the same action is performed two times. I guess I should put it in a variable. somewhatDRY = do { let greet = putStrLn "Hello"; -- not executed when put into variable greet; -- executed once here greet; -- and again here } Oh, the user wanted to specify how many greetings to print. countGreetings number = do { let greetings = -- infinite list of prints, repeat (putStrLn "Hello"); -- none of which is executed let enough = -- we take the first few prints, take number greetings; -- still without executing any sequenceA_ enough; -- now we execute just the first ones } Huh, I guess I don't even need the do notation anymore. countGreetings number = let greetings = repeat (putStrLn "Hello") enough = take number greetings in sequenceA_ enough ---- In these examples I used sequenceA_, which is a plain library function that takes a list of effectful computations and returns a single effectful computation. The effect of the returned computation is the same as if all the effectful computations in the list was called one after the other. I mention it's a plain library function because you wouldn't be able to define such a function – not even in the standard library – if effectful computations weren't first-class values... ---- I wrote a comment in the example saying "now we execute just the first ones". That's a lie, actually. Because like any effectful computation, also the return value of countGreetings is a first-class value. Meaning we could assign the return value of countGreetings to a variable, or stick it in a list, and so on, and nothing would be executed. In order to avoid uncomfortable déjà vu, I'll In order to avoid uncomfortable déjà vu, I'll just leave off here and conclude that when effectful computations are first-class values, there is, in a sense, two phases when the code is run. First there's an evaluation phase, where effectful computations are constructed and passed around. Then there's an execution phase, which actually executes these effects. If your effectful computation isn't hit by the execution phase, it will never be executed – no matter how many times the evaluation phase goes over it.