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.
Idris, a language that will change the way you think about programming (2015)
51–60 of 101 posts
Re: Idris, a language that will change the way you think about programming (2015)
#52Re: Idris, a language that will change the way you think about programming (2015)
#53Earlier 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.
Re: Idris, a language that will change the way you think about programming (2015)
#54If 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)
Re: Idris, a language that will change the way you think about programming (2015)
#55Earlier 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…
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)
#56Earlier 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…
Re: Idris, a language that will change the way you think about programming (2015)
#57I 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)
#58Earlier 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... ;)
Re: Idris, a language that will change the way you think about programming (2015)
#59Re: Idris, a language that will change the way you think about programming (2015)
#60Earlier 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…
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).