Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

IBM releases Elm-powered app

discourse.elm-lang.org

Post reply on HN
Print view View original

191–199 of 199 posts

Re: IBM releases Elm-powered app

#191

Post by quickthrower2 »

leshow wrote: post #129
hardwaresofton wrote: post #42

Earlier quoted context omitted.

I've always thought that Elm was like Purescript in the way that it was just another way to bring the good parts of Haskell (a good type system) into JS. I didn't consider elm's architecture as the main value proposition -- if you squint it looks just like every other data management model for component-based approaches these days -- flux, redux, etc all work in a similar way, +/- immutability. Hopefully people aren'…

Elm isn't a general purpose programming language. You can only write web-apps with it you can only use TEA (the elm architecture). In that way, the TEA really is it's main value proposition.

You can do more than that using ports, but it doesn't sit very naturally.

Re: IBM releases Elm-powered app

#192

Post by quickthrower2 »

deltron3030 wrote: post #37

What I find most interesting about Elm as a designer who also "codes", is that because of its bottom up frontend philosophy (types first instead of components first) it somehow assumes that the UI designer and coder is the same person, that there is no clear designer to developer handoff where you hand over a thought out design to implement. It's more the other way round, where you'd hand over what you've come up wit…

A designer can hand over a design to an elm programmer, who would then need to translate that into Elm. It's not hard to do and there are even HTML->Elm tools such as https://mbylstra.github.io/html-to-elm/ for example.

Re: IBM releases Elm-powered app

#193

Post by willtim »

bgorman wrote: post #188
willtim wrote: post #185

Earlier quoted context omitted.

Tests prove the presence of bugs not their absence. You should be writing more tests if you have no static type system, in order to find the bugs that you would otherwise prove don't exist.

A static type system like Elm doesn't fix logical bugs like wrong indexing, wrong predicate etc, it just finds issues with types. Types do not contain the real logic of your program. Types are somewhat useful for verifying data is passed around in the correct shape in a program, but to say it prevents most obvious errors is naive. Not to mention in Elm you will waste tons of time doing useless tasks like writing enco…

> A static type system like Elm doesn't fix logical bugs

Static type systems can absolutely catch logical bugs! Proof that a list is non-empty or that a reference is never null are simple examples.

> Types do not contain the real logic of your program.

Types can completely determine the logic of many parts of your program. In Haskell, I often don't have to write custom traversal code, it's selected for me based on the types.

> Types are somewhat useful for verifying data is passed around in the correct shape in a program

This is only the start of what types can do, try learning Haskell.

> but to say it prevents most obvious errors is naive.

No, naive is dismissing static type systems to the point that not even extra testing is done to compensate.

> Elm you will waste tons of time doing useless tasks like writing encoders/decoders and code that could be moved to macros in a more powerful language.

Elm's aim is to be a basic easy-to-learn language (no operator overloading etc). Personally, generic (polytopic) programming feels like a more elegant approach than macros. Haskell offers both.

Re: IBM releases Elm-powered app

#194

Post by yogthos »

willtim wrote: post #193
bgorman wrote: post #188

Earlier quoted context omitted.

A static type system like Elm doesn't fix logical bugs like wrong indexing, wrong predicate etc, it just finds issues with types. Types do not contain the real logic of your program. Types are somewhat useful for verifying data is passed around in the correct shape in a program, but to say it prevents most obvious errors is naive. Not to mention in Elm you will waste tons of time doing useless tasks like writing enco…

> A static type system like Elm doesn't fix logical bugs Static type systems can absolutely catch logical bugs! Proof that a list is non-empty or that a reference is never null are simple examples. > Types do not contain the real logic of your program. Types can completely determine the logic of many parts of your program. In Haskell, I often don't have to write custom traversal code, it's selected for me based on th…

Haskell was my first FP language, I used it for about a year, and worked with Scala briefly after. My experience is that you're really trading one set of problems for another in practice. Static typing can guarantee that you avoid a certain class of errors, but it often results in code that's longer and more difficult to understand opening opportunities for different kinds of errors. There is absolutely no empirical evidence to suggest that the trade off is strictly superior in practice.

Static typing can catch inconsistencies at the cost of structuring your code in a way that the type checker can understand. This is often at odds with making it readable for the human. A proof only has value as long as the human reader can understand it. Here's a concrete example of what I'm talking about: https://github.com/davidfstr/idris-insertion-sort/blob/maste...

An insertion sort written in Idris has over 250 lines of code that you have to understand to know that it's implemented correctly. A python version would have about 10 lines or less. I'd have much easier time guaranteeing that the 10 lines do exactly what was intended than the 250 lines of type specifications. Of course, you could relax the type guarantees in Idris as well, but at that point you accept that working around the static checker has benefit and it's just a matter of degrees of comfort.

In general, the more constraints you specify via types the more of your program logic moves into type specifications. What this really means is that you're writing a metaprogram that emits your logic. However, there's no automated checker for that metaprogram that you wrote using the types. You still have to understand it to be correct in order to know that it's doing what you want it to. At this point you're basically living in a programmer version of the Plato's Cave.

The real question is not whether you can do something using a static type system or not. The discussion has to center around how that compares to alternative approaches such as testing, gradual typing, and runtime contracts.

Re: IBM releases Elm-powered app

#195

Post by cttet »

yakshaving_jgt wrote: post #182
cttet wrote: post #175

Earlier quoted context omitted.

The alternative is less Javascript logic written by the app developer (and instead use packages and APIs directly). Elm disguised as a beginner friendly language for web front-end, which is not true with the case of ports. Where you need to be fairly familiar with Javascript. The Elm community also advertise a lot on the advantage of development happiness of Elm over Javascript, and mention the Javascript fatigue a l…

> sometimes it requires even more Javascript experience than using just Javascript framework like React to build something that require a web api that's not in the tiny list that Elm provided. I don't understand. You're saying a codebase of 5% JavaScript demands more JavaScript experience than a codebase of 100% JavaScript. This seems self-evidently false. > If web development is not someone's main job and they are j…

> You're saying a codebase of 5% JavaScript demands more JavaScript experience than a codebase of 100% JavaScript.

A codebase of 100% Javascript does not usually mean 100% written by the app developer. If you are coding in react for some basic app, like some basic crud with react using existing backend with Firebase, it almost only require you to learn the some basics of react and Javascript syntax, and fill in the template. You can also use other modules by just follow their documentation when you need some extra functionality.

However in Elm Ports we are required to pass async messages for everything which is much harder. I am OK with the boilerplate for the JSON encoder and stuff, but I have to wrap around my head for how to write a port for lots of basic web APIs.

Port is hard even for people that familiar with Javascript. There are plenty of experienced Javascript programmers willing to dive into the source code of Elm to write native modules to avoid ports even. https://www.reddit.com/r/elm/comments/81bo14/do_we_need_to_m...

In addition, even the 5% of Javascript will eventually leads to the full Javascript stack, where Elm, without an official recommend JS stack, feels more like additional choice as a part of the JS fatigue. Beginners ends up looking up on browserfy/gulp/webpack etc and figuring out a way to integrate Elm in.

> Seems like the argument is Elm isn't ideal if you're not a programmer

I program daily for machine learning, and I have used many programming languages. But Javascript is not the language that I want to dive in too much, which it is the main reason I learn Elm. If your requirement of being a programmer is having a job as a software developer, then I am not. But I think a language with an aim of going into education and scientific computing shouldn't limit itself to that. https://www.youtube.com/watch?v=uGlzRt-FYto

I enjoy Elm. It is one of my favourite programming language. But I have not gotten anything done with it mainly because of ports. If I am pursuing a career in front-end related development, I would dive into Javascript and build stuff. I understand the decisions from Evan and friends and I am just thankful for Elm as it is, there is no right for me to demand anything anyway.

[edit: formatting]

Re: IBM releases Elm-powered app

#196

Post by [deleted] »

yogthos wrote: post #194
willtim wrote: post #193

Earlier quoted context omitted.

> A static type system like Elm doesn't fix logical bugs Static type systems can absolutely catch logical bugs! Proof that a list is non-empty or that a reference is never null are simple examples. > Types do not contain the real logic of your program. Types can completely determine the logic of many parts of your program. In Haskell, I often don't have to write custom traversal code, it's selected for me based on th…

Haskell was my first FP language, I used it for about a year, and worked with Scala briefly after. My experience is that you're really trading one set of problems for another in practice. Static typing can guarantee that you avoid a certain class of errors, but it often results in code that's longer and more difficult to understand opening opportunities for different kinds of errors. There is absolutely no empirical…

[deleted]

Re: IBM releases Elm-powered app

#197

Post by willtim »

yogthos wrote: post #194
willtim wrote: post #193

Earlier quoted context omitted.

> A static type system like Elm doesn't fix logical bugs Static type systems can absolutely catch logical bugs! Proof that a list is non-empty or that a reference is never null are simple examples. > Types do not contain the real logic of your program. Types can completely determine the logic of many parts of your program. In Haskell, I often don't have to write custom traversal code, it's selected for me based on th…

Haskell was my first FP language, I used it for about a year, and worked with Scala briefly after. My experience is that you're really trading one set of problems for another in practice. Static typing can guarantee that you avoid a certain class of errors, but it often results in code that's longer and more difficult to understand opening opportunities for different kinds of errors. There is absolutely no empirical…

Sorting (TimSort) was broken for many years in Python. It was good old-fashioned logic and theorem proving, not tests or runtime assertions, that got it fixed. There is merit in proving properties of any critical implementation, no matter how difficult. However the gist you referenced looks to be someone's learning effort, so hardly a model example.

Your view on the role of types is unfortunate if you think term logic is simply mirrored at the type level (Plato's Cave). The Curry-Howard correspondence tells us to think of types as logical propositions with terms as their proofs.

Re: IBM releases Elm-powered app

#198

Post by yogthos »

willtim wrote: post #197
yogthos wrote: post #194

Earlier quoted context omitted.

Haskell was my first FP language, I used it for about a year, and worked with Scala briefly after. My experience is that you're really trading one set of problems for another in practice. Static typing can guarantee that you avoid a certain class of errors, but it often results in code that's longer and more difficult to understand opening opportunities for different kinds of errors. There is absolutely no empirical…

Sorting (TimSort) was broken for many years in Python. It was good old-fashioned logic and theorem proving, not tests or runtime assertions, that got it fixed. There is merit in proving properties of any critical implementation, no matter how difficult. However the gist you referenced looks to be someone's learning effort, so hardly a model example. Your view on the role of types is unfortunate if you think term logi…

Sure, you can use formal methods to prove properties that are hard to test. The point you seem to have missed is that it takes a lot of effort to do that.

The reality is that in most cases there's a cost benefit analysis regarding how much time you can spend on a particular feature and the strength of the guarantees.

>The Curry-Howard correspondence tells us to think of types as logical propositions with terms as their proofs.

Hence my point that you end up writing a metaprogram that emits the logic. Ensuring that the metaprogram is correct is a manual process. The more complex the proof, the harder it becomes to understand.

Consider Fermat's conjecture. It's trivial to state it, it's trivial to test it to be correct for a given set of inputs. However, proving it for the general case is quite difficult, and only a handful of people in the world can follow that proof.

Re: IBM releases Elm-powered app

#199

Post by maxilulu »

yogthos wrote: post #198
willtim wrote: post #197

Earlier quoted context omitted.

Sorting (TimSort) was broken for many years in Python. It was good old-fashioned logic and theorem proving, not tests or runtime assertions, that got it fixed. There is merit in proving properties of any critical implementation, no matter how difficult. However the gist you referenced looks to be someone's learning effort, so hardly a model example. Your view on the role of types is unfortunate if you think term logi…

Sure, you can use formal methods to prove properties that are hard to test. The point you seem to have missed is that it takes a lot of effort to do that. The reality is that in most cases there's a cost benefit analysis regarding how much time you can spend on a particular feature and the strength of the guarantees. >The Curry-Howard correspondence tells us to think of types as logical propositions with terms as the…

> onsider Fermat's conjecture. It's trivial to state it, it's trivial to test it to be correct for a given set of inputs. However, proving it for the general case is quite difficult, and only a handful of people in the world can follow that proof.

This is a strawman, conventional static type system can't prove all general cases either and no body is saying that they do that. Yet, they being a superset of dynamic typing, they allow to have the same expesiveness as such by providing a bypass like 'Object' or 'any'.

Post reply on HN