Do people here find this sort of thing appealing?

I do! But I already bought into Typed FP, and was blown away by this talk. "Tell more things about your program to the compiler and it'll do amazing things!"

I rather dislike Haskell and Idris. I find the notation obfuscating, inelegant, and cumbersome. The whole point of types is to prevent errors, but they get so concerned with type checking that they forget it is about expression. If you wanted to declare a pointer to a pointer of an array of records, Modula-2 offered that in the 70's, with the ability to turn off type checking when you needed to break the rules for some low-level purpose. I wish people would read Prof. Wirth's work, or spend 10 minutes with modula-2 to see a prior high-water mark in modularization and type protection. The majority of errors in graphical interactive programming nowadays are related to drawing and event handling, and many languages have neither a database nor a graphical model in the language, so for my purposes of the future of coding, they represent the past of terminal-based languages that are actually retrograde in their effect. Sorry to be such a wet blanket on this line, but you're talking to a guy who heard John Backus in person in 1973 talk about his functional language. FP is not new, and one should be cautious about thinking FP is a magical cure. We all want composability, and reusable parts. I believe there are only 2 unsolved problems in computer science: 1) how to achieve re-usable parts, and 2) how to make debugging go down from 85% of the effort to a more modest fraction.

Happy to replace "the" with "a" future ... tastes differ and reasonable people can disagree on things like this.

Hi @Miles Sabin - welcome! While I don't consider myself in the 'typed FP' camp, FP definitely comes up in this slack and spurs interest - just search for Elm, Hazel, Lamdu or even 'FP'. So it is not out of place at all. As for Edward's response - I don't think it is appropriate or conducive to good discussion. There are much better ways to disagree.

@Miles Sabin, I’m a fan of Haskell, but not a fan of its tooling situation (I’m working with Haskell right now). I’m looking forward to watching this talk, but I think it shows some of the things I believe are possible with a language like Haskell or Idris, namely inferring the implementation from the type definition

Yup, exactly that.

here’s a thought that crossed my mind. someone could parse the entire hackage and look for all the type transitions. maybe they could discover some interesting patterns. maybe this could be fed to a machine learning algorithm that would then suggest patterns while you code

In a sense that's what Edwin is demonstrating, albeit only with what's available in the current scope.

ok. one more reason to watch the video 🙂

Although it doesn't offer multiple choices. I don't quite know what it does if there are multiple choice. Given the misfire that he rules out with the linear type annotation in the segment I linked to I suspect it picks the first solution found.