HN Theater @HNTheaterMonth

Not quite what you mean, but still, you might find interesting the talks on how to approach coding in languages like Idris, where the compiler is able to support the editor in type suggestions.

https://www.youtube.com/watch?v=DRq2NgeFcO0

> Right, but then you can't multi-thread merge()

Not sure If I understand what you mean. It would be both possible to call "merge" in parallel or to implement merge to do the work in parallel as well.

> Or else, you say that it's immutable, and when some thread changes the state, it produces a new map3, and the old one doesn't change. But then you have the problem of getting all the other threads updated to see the new version of map3.

Yes, but this "problem" is exactly the beauty of this style of programming. It forces you to make your data-flows explicit and hence easy to discover, understand and manipulate/change by other developers.

> And, by the way, I've worked on that router for TV stations. Modeling that matrix in a way that invalid states are unrepresentable is, um, extremely non-trivial...

I'm not saying it is trivial. But it is possible and depending on the programming language it is actually surprisingly easy. Not only that, with a good typesystem, you not only prevent invalid state from occurring, you even get a lot of support from your IDE due to the extra information it has.

Here's an example how that can look like for matrices and functions to manipulate them (like transpose): https://youtu.be/DRq2NgeFcO0?t=1137

The syntax might be alien to you, but I hope it still shows what's possible at compile-time before even running the program with modern languages today.

I really like the general idea of bridging the gap between graphical and text-based interfaces, abstracting away the differences and be able to use a mixture of both. In the realm of interactive programming (eg heavily ide assisted), people with some functional and statically typed programming background would be interested in this magnificent talk about idris2:

[Edwin Brady - Idris 2 - Type-driven Development of Idris]

https://www.youtube.com/watch?v=DRq2NgeFcO0

Every single one of your claims is addressed by the programming language Idris [1], which has dependent types. This is not to say that Idris is the only dependently typed language which solves these issues, only that it exists as a counterexample to your claims.

1. Idris does not have type inference at the top level, but it does infer types within the body of functions. It can even disambiguate identically-named functions with different types, something Haskell cannot do.

Moreover, Idris (and other dependently typed languages) can perform implementation inference, something which is much more powerful and useful to the programmer than type inference. It lets you work interactively with the Idris compiler whereby you specify a type and Idris creates a skeleton of the function for you, filled with holes that you replace with expressions. You can ask Idris what the type of a hole is and it will helpfully tell you the types of all other identifiers in scope. You can even ask Idris to attempt to fill in the hole for you, something it can usually do when there is only one possible expression with that type (occurs extremely often in practice).

Watch Edwin Brady's demo of Idris 2 [2] to see this form of interactive development in action. Note that although Idris 2 isn't finished yet, a great deal of these examples (such as zip) work in Idris 1.3.2 (the current release).

2. Idris lets you specify your program gradually. When problems arise, you can refine your types and Idris will guide you through all of the refactoring you need to do to enforce your new invariants.

3. Idris does not force all of your functions to be total, only the ones you want to use in types. Idris checks the totality of all your functions and can produce compilation errors based on totality annotations attached to your functions. In practice, It is not very hard to make every function in your program total, apart from the main loop.

4. Idris has modules and gives you powerful tools (such as views) that allow you to define a stable API at the module boundary. This means you can mess around with any of the types of private functions to your heart's content, without any visible change to the outside world. This is entirely the opposite of 'non local' Java exceptions.

5. Idris has extremely powerful tools for working with state and writing concurrent programs which preserve invariants that cannot otherwise be checked easily with other tools. As for OO, well, that's a concept so nebulous as to be almost incoherent at this point. In practice, Idris's interfaces can dispatch on as many parameters as you want, unlike most OO languages which only do single dispatch.

[1] https://www.idris-lang.org

[2] https://www.youtube.com/watch?v=DRq2NgeFcO0

⬐ tathougies

Type inference in idris works well if the types of the terms in question are non dependent. The moment you introduce complicated types, type inference suffers, which is expected because even idris cannot break the fundamental nature of logic.

⬐ 9q9

This is my point.

Adding dependent types comes with costs that you will always have to pay, even if you don't use the power of dependent types. If you verify with e.g. program logic in the few real-world cases where formal verification is financially viable, then you only pay the price when you do the verification.

⬐ 9q9

I'm not sufficiently familiar with Idris to comment -- I will learn Idris in the future, hopefully in December.

Be that as it may, I'm somewhat sceptical of implementation inference: after all, you need to give a spec, exactly the thing you typically do not have in large-scale software engineering. The spec emerges at the end and often the program is the spec itself. Moreover, as far as I gather, implementation inference works by program synthesis, and unless Brady has had a massive breakthrough here, that's an exponential search process, so it won't scale much beyond inferring small programs like the zip function. (Still I think implementation inference is a useful tool- but it's not magic.)

⬐ delish

Agreeing with you: I'm only familiar with Idris insofar as I've watched talks on it, but my recollection is that its implementation inference is a search across pre-listed implementations. Edwin Brady says that that's surprisingly useful. I believe him and look forward to trying it out some time soon, but it is not as magical as we might guess.

⬐ chongli

Definitely give Idris a go. I'm working through the book Type-Driven Development with Idris [1] by Edwin Brady, the author of Idris, and I'm having a ton of fun with it. Idris is a lot more practical than I thought. It fixes some annoyances I had with Haskell, such as record naming (Idris lets you reuse record names in different types, it resolves ambiguity by type checking).

It's also eagerly evaluated (unlike Haskell), with a very simple Lazy annotation you can tack on to a type when you want laziness. I think most people will find this much easier to reason about than Haskell's laziness everywhere.

[1] https://www.manning.com/books/type-driven-development-with-i...

⬐ zeptomu

> [...] Idris is a lot more practical than I thought.

This may sound like a stupid question (but is probably necessary in a thread about the convergence of proof systems and static typed functional programming languages):

"How can i implement something like unix' wc?"

So just a program that counts lines (forget words and bytes for now) of a file. This means we need to support (at least in some kind of standard library) basic IO stuff like files, processes and environments. If the language talks about how "simple" (in terms of code/term length) it is to define a binary tree ... the integers >= 0 (the famous Nat = Zero | Succ Nat) example, or beware the Fibonacci sequence - most people won't be impressed.

Because that's what is associated with "programming language" (as compared to "proof assistents").

Sorry that sounds a bit like a rant, but after 5 minutes of searching I couldn't find an example how to read a file in Idris. The closest I found was: http://docs.idris-lang.org/en/latest/effects/impleff.html but it did not tell me how to open a file ...

⬐ seanmcdirmid

I don’t know about Idris, but the basic idea would be transform the file’s type from (a|b)* into (a* b)* a* where b is a newline and a is any non newline. Then your answer simply counts the first star of the transformed type (change that star to a counter exponent as you are forming the type).

⬐ zeptomu

Yeah ... but how does that look? A "naive" wc implementation (counting the character '\n') is <50 lines of code (if we have modern file IO in the standard library) in a practical PL.

But maybe there is a too big difference between the concept of "files" (as seen by OS developers that view them as a byte-blob in a hierarchical name system) and language designers that want to represent a file as a collection of lines (and probably would like your command line interpreter not allow to call "wc" on a file that contains non UTF8 encoded data) - but this is still a pretty big step for our current computation environment (where I can call programs by name that are also files).

For many people (including me) a "practical" programming language needs an implementation that can generate (compile) an executable or interpret a file representation of its source. Otherwise its a proof assistant.

Maybe we have to merge the concept of data in terms (no pun indented) of bytes (types?) in-memory and collections of bits and bytes that have a lifetime longer than the program (if it's not a daemon)?

⬐ seanmcdirmid

If you implement by manipulating the types directly, a few operations with a loop (just for counting lines mind you). Again, I’m not sure how this would be done in Agda, Idris, or COQ, and the system designing is a bit different from other type systems.

But also, any discrete one dimensional problem like wc is going to benefit from a type system with types that resembles regular expressions.

⬐ chongli

I'm still a beginner at Idris, but here's my attempt at a "naive" wc:

    module Main

    wordCount : String -> IO ()
    wordCount file = let lineCount = length $ lines file
                         wordCount = length $ words file
                         charCount = length $ unpack file in
                         putStrLn $  "Lines: " ++ show lineCount
                                 ++ " words: " ++ show wordCount
                                 ++ " chars: " ++ show charCount

    main : IO ()
    main = do (_ :: filename :: []) <- getArgs  | _ => putStrLn "Usage: ./wc filename"
              (Right file) <- readFile filename | (Left err) => printLn err
              wordCount file

It counts lines, words, and characters. It reports errors such as an incorrect number of arguments as well as any error where the file cannot be read. Here are the stats it reports on its own source code:

    $ ./wc wc.idr
    Lines: 14 words: 86 chars: 581

Hope that helps.

⬐ zeptomu

Wow, thanks for the response - that actually looks like Haskell and if its performance is not that abysmal (let's say slower than Python), that is pretty cool.

This actually looks quite reasonable - usage string included, I like it. Hats off to you, I will try to compile it to a binary now and do some benchmarking.

⬐ seanmcdirmid

Is it really fair to call this an implementation of wc if it is just using a built in function for each case?

⬐ zeptomu

These might be reasonable functions to implement in a standard library, so having them it makes sense to use them. I rather feared Idris does not have some IO abstraction (reading/writing) files at all. Maybe I am conflating languages and libraries here, but they often go hand in hand.

My practicability expectations for languages implementing dependent types are pretty low.

⬐ tosh

repository (published a few days before this talk at Curry-On 2019): https://github.com/edwinb/Idris2