I don't get it. Is it just about rediscovering std::array?
Can you append a std::array and a std::array to get a std::array with x and y chosen at runtime?
Idris, a language that will change the way you think about programming (2015)
61–70 of 101 posts
Re: Idris, a language that will change the way you think about programming (2015)
#62app : 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 );
My recollection of C++ (possibly outdated since 11 or 14, though that would - pleasantly - surprise me) is that template parameters must be picked at compile time. With Idris, you can pick X and Y at runtime and still get compile time checking.
Re: Idris, a language that will change the way you think about programming (2015)
#63Is Idris related to Idris Elba, the British actor, by any chance?
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'…
Thank you, I had read the FAQ:
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. :)
Re: Idris, a language that will change the way you think about programming (2015)
#64Earlier quoted context omitted.
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 utilitie…
> With: Everything.
This may be nitpicking but certain classes of programs cannot be realistically built with Haskell. Anytime you need to tightly control latency (soft realtime) won't really work since you have both a garbage collector and lazy evaluation. Memory constrained systems are pretty tough as well since you don't really get insight into allocation/deallocation, which also makes structuring your data into a particular memory layout tricky compared to C(++) for instance.
Not to say that Haskell isn't awesome. It should probably be used for more systems. It just can't be the "hammer" to make every problem into a nail.
Re: Idris, a language that will change the way you think about programming (2015)
#65app : 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 );
Because with dependent typing, the length can be specified at runtime and you still get static checking.
There's also a huge difference between untyped templates and strongly typed generics, but in this particular case the difference is somewhat subtle.
Re: Idris, a language that will change the way you think about programming (2015)
#66Re: Idris, a language that will change the way you think about programming (2015)
#67app : 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 Python programmer who doesn't understand this notation - what am I looking at, and what's amazing about it?
One thing that no one touched on:
In reading Haskell (and apparently Idris) types, a name that starts with a lower case letter is an unbound type variable - sort of like a template parameter in C++. The `a` in each of the Vect's must be the same type but it can be any type (picked at the call site, for any given call).
Re: Idris, a language that will change the way you think about programming (2015)
#68Earlier quoted context omitted.
Can you append a std::array and a std::array to get a std::array with x and y chosen at runtime ?
Of course not. In my understanding, the article was about static type checking, though.
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.
Re: Idris, a language that will change the way you think about programming (2015)
#69Earlier quoted context omitted.
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 utilitie…
> With: Everything. This may be nitpicking but certain classes of programs cannot be realistically built with Haskell. Anytime you need to tightly control latency (soft realtime) won't really work since you have both a garbage collector and lazy evaluation. Memory constrained systems are pretty tough as well since you don't really get insight into allocation/deallocation, which also makes structuring your data into a…
This depends on what you mean by "with". As you say, you can't sit down, bang out some ordinary Haskell code, and expect GHC to give you an executable that will do real-time as well as you can in C.
That said, it's perfectly possible to write a DSL that handles scheduling, uses GHC's type machinery to track memory use and execution time, and have GHC generate a program that will generate C code that meets hard real-time guarantees. In fact, someone wrote it, it's available on hackage (https://hackage.haskell.org/package/atom) and my understanding is that it's used in production for control software in the auto industry.
Re: Idris, a language that will change the way you think about programming (2015)
#70Earlier quoted context omitted.
There's nothing about braces that ensures visual cues to nested code. Significant whitespace does precisely that. And eliminates brace placement arguments. int func() { while dosomething() { dosomething() dosomething() doanotherthing() } dosomething() } def func(): while dosomething(): dosomething() dosomething() doanotherthing() dosomething()
I've never used a language where space indentation was used over curly brackets. So question for those who have... When doing so, wouldn't copying and pasting code around potentially cause a lot of accidental issues? Are there some negatives and side effects of the indentation style? Just curious.
Yeah, but you get used to the quirks of your language+editor. Shifting a block right or left isn't hard with a good editor.