6 ms·

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 libra

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 7y ago
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 7y ago
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 7y ago
  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 7y ago
    Is it really fair to call this an implementation of wc if it is just using a built in function for each case?
    - zeptomu 7y ago
      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.

seanmcdirmid 7y ago

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 7y ago

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 7y ago
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 7y ago
  Is it really fair to call this an implementation of wc if it is just using a built in function for each case?
  - zeptomu 7y ago
    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.