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

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

#41

Post by lambdasquirrel » Thu, Jan 07, 2016, 5:34 AM UTC

framp wrote: post #2

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)

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.

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

#42

Post by pdkl95 » Thu, Jan 07, 2016, 5:35 AM UTC

a3n wrote: post #27

kazinator wrote: post #16

Earlier quoted context omitted.

> There's nothing about braces that ensures visual cues to nested code. A machine can look at the braces and re-indent the code, so that you don't have to look at the braces. All while you rest assured that the meaning didn't change: I just popped it into Vim, selected all and hit =: int func() { while dosomething() { dosomething() dosomething() doanotherthing() } dosomething() } Some semicolons are expected so thing…

The braces didn't do anything for a human until indentations were added, whether by human or machine. If you lifted those braces out, you'd still know that the intent was (although in C it would be wrong :) The only thing I miss about braces is being able to jump to the end of a block easily. In python and similar that's a bit harder to do with an editor.

> The braces didn't do anything for a human until indentations were added

Having explicit delimiters (I don't care if it's {}, begin...end, or whatever) provide several benefits that I have often used.

1. (by far the most important) They trivialize the recovery of indentation that has been trashed by a bad/misconfigured/unfamiliar editor or coworker who inserted "\t" characters into the file. Just run indent-region or send the file through indent(1).

2. Moving code is easier. Just kill/yank it to where you want it and let indent-region or whatever re-indent as needed. Without delimiters I have to either re-indent manually or use an editor with a feature that changes a region's indent level. Even with such a feature, I still have to tell the editor "move this two levels deeper". With delimiters, I can leave that work to the editor.

3. The movement advantages you mentioned.

As for the extra work of having to close blocks (including the infamous LISP ")))))" motif), that's what features like electric-pair-mode is for.

Even better, delimiters can convey more information. Color cues have proven to be very effective at conveying important information; syntax highlighting is very popular, even when showing code outside an editor (such as inside a

 tag). I find extending these color cues to also show nesting[1] to be almost as useful as basic syntax highlighting. (I'm using rainbow-delimiters[2] in that screenshot).[1] https://i.imgur.com/xS4y6rT.png
[2] https://github.com/Fanael/rainbow-delimiters

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

#43

Post by catnaroek » Thu, Jan 07, 2016, 5:39 AM UTC

sgrove wrote: post #14

systems wrote: post #9

"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

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?

1ML doesn't really unify the type and value languages. First-class modules are syntactic sugar over System F-omega, which means that the elaboration/type-checking phase of 1ML duly splits modules into type and value components, which live in separate worlds.

Personally, I find 1ML's approach more pragmatic, or, at least, easier to digest for most programmers - including Haskell programmers. Dependent types are more powerful, but they aren't free from complications. For instance, unifying the type and value languages willy-nilly can cause trouble if you want your value language to be Turing-complete, because now type-level computation can diverge too! In a language based on System F-omega, type-level computation is guaranteed not to diverge, because its type level is the simply typed lambda calculus. Some use cases might warrant providing more powerful type-level computation facilities (e.g. calculating the shapes of multidimensional matrices), but it isn't clear to me that the full power of a Martin-Loef-style dependent type theory is needed.

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

#44

Post by orblivion » Thu, Jan 07, 2016, 5:40 AM UTC

rfw wrote: post #35

bojo wrote: post #17

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.

Unfortunately, the usefulness is limited – the size of all Vects must be known at compile time. While this does prevent a large class of bugs that arise from incorrect compile-time knowledge, the size of the class of runtime bugs affected by this is a lot smaller, as for each differently-lengthed Vect, a distinct instantiation of the Vect type needs to exist at compile-time.

I've never actually used such a feature, but my understanding is that this is not strictly true. I think that the compiler can generically understand that this function adds two vectors and their lengths.

I'll see if I can contrive an example. Supposing you have a list L1 of vectors of length 5. You also have a vector V1 with user input, with length x (unknown at compile time). You then make a new list L2 by taking each vector in L1 and append V1 to it. L2 is now a list of vectors of length (5 + x). Even though x is unknown at compile time, the compiler still knows that all vectors in L2 are of the same length. It can make restrictions based on this fact.

It seemed strange to me when I heard this concept, I thought the compiler would need to consider infinite possibilities, but apparently similar things are possible even in Haskell. For instance, you can define a list as a recursive type that holds a value of a Null type (not just a null value of the list type) or another List. Apparently it can still reason about this.

However, these are things I've heard. Hopefully someone with more experience can chime in and let me know if I'm right here.

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

#45

Post by tines » Thu, Jan 07, 2016, 5:56 AM UTC

bojo wrote: post #17

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.

As a C++ programmer, I'd like to ask how is this different in effect from

    template
    std::array app(std::array, std::array);

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

#46

Post by enraged_camel » Thu, Jan 07, 2016, 5:58 AM UTC

skosch wrote: post #37

athesyn wrote: post #18

Bit disappointed it makes the assumption the reader knows Haskell, that lost me immediately.

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 d…

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?

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

#47

Post by tikhonj » Thu, Jan 07, 2016, 6:00 AM UTC

nihils wrote: post #39

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.

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/Phase...

[2]: https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell

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

#48

Post by jonahx » Thu, Jan 07, 2016, 6:14 AM UTC

tines wrote: post #45

bojo wrote: post #17

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.

As a C++ programmer, I'd like to ask how is this different in effect from template std::array app(std::array , std::array );

operationally, i'm not sure if there is. it's certainly a lot prettier, though. i'd be curious if there's a deeper difference, too. it feels like there is, at least to me...

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

#49

Post by dllthomas » Thu, Jan 07, 2016, 6:17 AM UTC

rfw wrote: post #35

bojo wrote: post #17

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.

Unfortunately, the usefulness is limited – the size of all Vects must be known at compile time. While this does prevent a large class of bugs that arise from incorrect compile-time knowledge, the size of the class of runtime bugs affected by this is a lot smaller, as for each differently-lengthed Vect, a distinct instantiation of the Vect type needs to exist at compile-time.

Per my understanding, what's so exciting about this is precisely that you're wrong - it does not need to be known at compile time, but can prove symbolically that the resulting length will be X + Y. And of course, given that, it's not statically creating a distinct instantiation of the Vect type for every N at compile time!

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

#50

Post by Ixiaus » Thu, Jan 07, 2016, 6:17 AM UTC

enraged_camel wrote: post #46

skosch wrote: post #37

Earlier quoted context omitted.

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 d…

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 anot…

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.