Live data from Hacker News

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

crufter.com

51–60 of 101 posts

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

#51
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.

Working in Haskell, I don't feel like it's "saving me from myself" so much as giving me tools I can use to save myself.

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

#52
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).

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

#53

Earlier quoted context omitted.

Not quite. Types can depend on runtime values. This can in effect _force_ the programmer to perform the required validation when accepting foreign data.

Not only that but you can arbitrarily encode constraints. Want to check something silly like whether there's an even number of elements in a list? Yea you can do that, and pass it along. I can do stuff like, okay, I know the max size of the files we're going to accept is 1mb.

Almost arbitrarily - they must be computable... ;)

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

#54

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)

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.

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

#55
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…

I am very much the same way. What I eventually did to get a foothold on the language was power through the first few chapters of 'learn you a haskell', and read 'haskell the hard way' and then sat down and typed out a tutorial implementing the Kaleidoscope teaching language in Haskell [2].

It was slow at first, and there was a lot of "now what's this arrow doing here?", but I would go back to the books when I had questions and eventually things started making sense. That won't work for everyone, but maybe it will work for you too?

The folks in #haskell are generally pretty helpful, and delightfully easy to troll.

[2]: http://www.stephendiehl.com/llvm/ [1]: http://yannesposito.com/Scratch/en/blog/Haskell-the-Hard-Way...

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

#56
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…

Algebraic data types and pattern matching are great for compilers, interpreters, static analyzers, and basically anything dealing with implementation of programming languages. That said, Haskell can pretty much do anything that other languages can these days, so it might be fun doing something you're already familiar with (say, IRC bot) and reimplementing it in a new way.

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

#57
post #52

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).

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.

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

#58

Earlier quoted context omitted.

Not only that but you can arbitrarily encode constraints. Want to check something silly like whether there's an even number of elements in a list? Yea you can do that, and pass it along. I can do stuff like, okay, I know the max size of the files we're going to accept is 1mb.

Almost arbitrarily - they must be computable... ;)

From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.

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

#60
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…

Haskell can actually make a pretty good imperative language (and you can put together little imperative sub-languages as well). That aside...

There's a reasonable perspective that says the type of problem that's best solved in a language is a problem for which there's good library support. For that, I'd probably recommend scanning https://github.com/Gabriel439/post-rfc/blob/master/sotu.md

But in my experience, where Haskell really shines is sketching out operations on some type that I know I'm going to get wrong - substantially or subtly - my first many tries. When I go to fix it, the compiler helps me find everything I need to change in tandem, and feel ahead to find inconsistencies in my model before I get there in the code. One example of this kind of problem is compilers - where we parse into an AST, transform the AST, and then produce other things from the AST. As development goes on, the AST evolves, and you have a lot of help knowing what needs to change to match and what you can ignore. I've recently been doing this for SQL (though with the goal of analyzing the queries, not producing an executable).

Post reply on HN