9 ms·

Idris, a language that will change the way you think about programming (2015)

• framp 11y ago
  Great article and really interesting language! I wonder how Idris is going to be affected when Dependent types come to Haskell as well (announced at last ICFP)
  • jonsterling 11y ago
    it's nice for the haskell folks that they'll be getting some sort of dependent types, but suffice it to say that they will be of a very different sort than the Idris ones. Not to mention, there is hope of giving a semantics to Idris since it is based on a fairly routine variant of type theory, whereas I don't think there is any hope at all of understanding "which" type theory the Haskell folks shall have implemented.
  • lambdasquirrel 11y ago
    I think it will be a while, if ever, before we're able to handle passing types around as values, in Haskell, the way we do in Idris and Agda. Dependent typing isn't just some feature. It touches a whole other way of thinking about things. If you go all the way with Agda, you have significantly constrained recursion to the point that the language isn't turing-complete anymore, but in return you get termination checking and other nice things. As it turns out, most of the code we write doesn't need unbounded recursion. Seriously, can you think of the last time you wrote something like that? And I think that'll be a hard pill for people to swallow, much like how it was really hard to sell memory safety to C/C++ guys back in the day.
• ophelia 11y ago
  Is Idris related to Idris Elba, the British actor, by any chance?
  • jonathonf 11y ago
    Because an existing name (from all various of the world) wasn't around before some bloke on the telly?
  • andolanra 11y ago
    The story, if I recall correctly, is that the programmer Edwin Brady had a previous project that was a proof engine, and lacking a suitable name for it, named after an older British children's cartoon called Ivor the Engine.[^1] When it came time to name a newer project, he decided to name it after another character from the same show: Idris, the little red Welsh dragon. This, incidentally, is why the Idris language's logo is a stylized red wing. [^1]: Ivor the Proof Engine is here, although apparently not actively updated any more: https://github.com/edwinb/Ivor https://github.com/edwinb/Ivor
    • archgoon 11y ago
      Thank you, I had read the FAQ: http://docs.idris-lang.org/en/latest/faq/faq.html http://docs.idris-lang.org/en/latest/faq/faq.html but could not infer why a dragon from Ivor the engine had been chosen. That the author had previously written a proof engine makes all the sense now. :)
• jonathonf 11y ago
  Does anyone know whether Idris is a response to Haskell's 'Foldable' controversy? It looks like it was released in 2012 on hackage but I don't know how far back 'Foldable' was envisioned.
  • tome 11y ago
    It is not.
• brudgers 11y ago
  Idris homepage: http://www.idris-lang.org/ http://www.idris-lang.org/ Github: https://github.com/idris-hackers https://github.com/idris-hackers
• systems 11y ago
  "Indentation significant syntax" :( in my opinion, one of the worst ideas to plague many new languages brackets are really, seriously, honestly a better visual cue for grouping
  • codemac 11y ago
    Parenthesis are pretty bomb-diggity as well.
  • rotten 11y ago
    I think it depends on the way your brain works. Some people prefer tables full of numbers, other prefer data visualizations. Some people prefer compact, tight code with lots of symbols. Others prefer spatially organized code. While there are probably people on the extremes and people in the middle. My observations have found lots of people generally fall into two main camps. A number/symbol/dense data aesthetic group, and a visual/spatial group. Left-Right brain? I don't know. Neither is better or worse. It just depends on who you are and who you are working with.
  • wyager 11y ago
    Brackets are also noise. There is no objective best answer here. I vastly prefer indentation based grouping, but I respect that you don't.
  • Buttons840 11y ago
    Haskell allows the use of brackets and indentation to format code, but nobody uses brackets. Do you find Haskell hard to read? And if so, is it because of the indentation? I bring up Haskell because Idris is very similar to Haskell syntactically. These are functional languages, and there isn't a lot of code to chunk together with brackets. Functions are often just one line, and it's a bit cumbersome to make functions that require multiple lines. Do you believe brackets add to the readability of a one line function?
  • sgrove 11y ago
    Please, please don't let this be the top comment on Idris. I really want to hear from people who have experience with it in different regards. For example, what's the editing experience like compared to e.g. OCaml with emacs/Merlin? Is there anyone in a position to compare 1ML's approach to unifying type/value languages vs using dependent types?
• bojo 11y ago
  app : Vect n a -> Vect m a -> Vect (n + m) a That is pretty amazing if you ask me. I look forward to the day when we all use languages which save programmers from themselves.
  • vosper 11y ago
    As a Python programmer who doesn't understand this notation - what am I looking at, and what's amazing about it?
    • badsock 11y ago
      The "Vector m a" means that it's a vector (like a Python list) that can only be m elements long, and those elements can only be of type a. E.g. "Vector 3 Int" will always be a Vector with three integers in it. If you try to treat it like a vector of any other length it will refuse to compile (e.g. pass it to a function that requires that it have 4 or more elements). The whole line is the type declaration for a function (app) that takes a Vector of length m, and a Vector of length n, and produces a Vector of length (m+n). Which is to say, the compiler knows at compile time what length the resulting Vector will be, and will fail to compile if the function you've written doesn't - provably - always meet that requirement. From a Haskeller's perspective it's amazing because container types are famous loopholes for code that produces runtime errors. For instance, if you call the "head" function (returns the first element) on an empty list it will halt the program at run time with an error, despite the fact that it passed the type check (because an empty list and a full one have the same type). As someone who learned Haskell and subsequently have been writing a lot of Python, I keep a mental tally of how many of my bugs (some of which took ages to track down) would have been caught immediately by a type system like Haskell or Idris'. I'd say it's well over half. In Haskell those kind of errors are drastically reduced, but a few still slip through. Languages like Idris can catch even more of them, in a clever way, which is awesome.
    • corysama 11y ago
      You're gonna have to read the article to find out.
    • bsznjyewgd 11y ago
• athesyn 11y ago
  Bit disappointed it makes the assumption the reader knows Haskell, that lost me immediately.
  • skosch 11y ago
    You know what, I've found it immensely valuable to get acquainted with Haskell, even though I've never used it (and likely never will). The concepts are timelessly beautiful, simple to understand, and can feel enlightening to run-of-the-mill imperative/OOP programmers. What's more, it seems to me that Haskell syntax is the lingua franca when discussing anything related to data types and functional programming these days. Those ->'s are everywhere, it's useful to know what they stand for. Just skim a few chapters of learnyouahaskell.com; you won't regret it.
    • enraged_camel 11y ago
      I'm more of a "learn by building things" type of learner. What kinds of things can I build with Haskell? For example, I got into Ruby via Rails, because Rails lets you quickly prototype simple web apps. So I could go from "I wish I had an app that does X" to actually building it, deploying it and sharing it with others. What would a similar "learning flow" look like in Haskell? (doesn't have to be web-based) Put another way, when I come across a problem, how do I recognize it as the type of problem that is best solved using Haskell, vs. an imperative language?
      • Ixiaus 11y ago
        Warning: highly biased opinion incoming. I came from Python to Erlang / Scheme / Haskell and at this point I would answer your question, > What kind of things can I build with Haskell? With: Everything. We use Haskell in production at Plum for our REST APIs, job schedulers, web applications, AWS service interfaces, a static site compiler, DB modeling, command line utilities, etc... We also use it for two CLI utilities that are cross-compiled for the ARM9 on our IoT product. I consider Haskell to be superior to any of the dynamically typed languages when writing production-level code, it's cleaner, safer, easier to maintain, easier to refactor, and much more fun IMHO. [EDIT] I neglected the other part of your question, "What is the learning flow like?" Definitely a bit rougher than Python or Ruby, I will not lie, but don't be discouraged. It simply means you need to do a bit more studying up-front first before you can tinker without being caught at every turn by the straight-jacket. I would first go through Learn You a Haskell because it is pretty accessible and introduces the language basics well enough. Then study the type system. You must learn Haskell's type system and terminology before you can understand more advanced code.
• blt 11y ago
  I recently had some murky thoughts on my ideal Matlab replacement, and it would have a feature like this. It would be huge for array-oriented programming: func train_model(X: [n d], y: [n 1]) So many lines of code are spent verifying that the sizes of two function arguments are compatible.
  • jdminhbg 11y ago
    You can do this in Julia now, with many of the affordances you'd expect from Matlab. function train_model(X::Array{Float64,d}, y::Array{Float64,1})
  • shele 11y ago
    Other example: Fixed size matrix multiplication in https://github.com/SimonDanisch/FixedSizeArrays.jl https://github.com/SimonDanisch/FixedSizeArrays.jl depends on element type T and dimensions MxN and NxR: function *{T, M, N, R}(a::Mat{M, N, T}, b::Mat{N, R, T})
• solomatov 11y ago
  If you are interested in Idris, you might also be interested in agda, which is another dependently typed programming language: https://en.wikipedia.org/wiki/Agda_(programming_language) https://en.wikipedia.org/wiki/Agda_(programming_language)
  • nv-vn 11y ago
    Other interesting ones to look at are F* (a joint effort from Microsoft Research and INRIA to create an ML-like dependently typed language) and ATS (a low-level, fast dependently typed language meant to replace C). What's cool about both of these is that they put emphasis on allowing imperative programming despite being dependently typed and seeming very functional.
• farhanhubble 11y ago
  Thanks for the link. I was looking into liquid Haskell and refinement types and thought that it's a great idea but rued the fact that it wasn't built into the language. I am definitely going to try Idris for one of my projects.
• nihils 11y ago
  This is actually perfect for a library on algebraic structures I've been trying to make in Haskell. For example, how does one distinguish between elements in the Dihedral group of order 10 vs. Dihedral group on order 16 when obstensibly, they have the same representation. For now, I think Haskell programmers use type-level arithmetic libraries, but this is a much better solution.
  • tikhonj 11y ago
    Haskell is actively moving in the direction of adding dependent types too. I believe phase 1[1] of the plan[2] is slated for GHC 8.0 (the upcoming release), and I'm sure the rest of it will follow soon. It's pretty exciting! [1]: https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase... [2]: https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell
• vzaliva 11y ago
  I would suggest to use Python or some other mainstream language instead of Haskell in example to contrast to Idris. People who know Haskell most likely be already familiar with dependent types and for people not familiar with Haskell syntax could be confusing (as some comments indicate).
  • cantankerous 11y ago
    Many mainstream languages like Python don't even have a syntactic notion of types. The best you could really do is say that Idris would get you some typing reification that you might do in those languages at no cost, but it would seriously sell short the power of dependent types like you see in Idris.
• Ace17 11y ago
  I don't get it. Is it just about rediscovering std::array?
  • dllthomas 11y ago
    Can you append a std::array<int, x> and a std::array<int, y> to get a std::array<int, x+y> with x and y chosen at runtime?
    • Ace17 11y ago
      Of course not. In my understanding, the article was about static type checking, though.
      • dllthomas 11y ago
        It is! That's what is so cool about it! Idris lets you write an append that will work for any X and Y chosen at runtime, but will check that the result must have length X + Y at compile time.
• muhuk 11y ago
  But does it allow specifying vectors that has no less than three and no more than seven items? Or vectors with even number of items? More importantly can we possibly implement church numerals in Haskell? /rhetorical
  • dllthomas 11y ago
    "But does it allow specifying vectors that has no less than three and no more than seven items? Or vectors with even number of items?" Yes.
• MichaelBurge 11y ago
  I haven't used Idris, but it sounds like someone I might want. I really want a tool that lets me mix and match operational code with proofs. It's common now to write a unit test while debugging something, less common to write a randomized property tester, and rare to see a theorem prover being used. It would be fantastic if I could casually throw in a proof while debugging a hard problem.