[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.)

[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)?

[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]

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.

[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.