3 ms·
> "Write a program to sort the words you find in the input file" That's as trivial to write in a dependently typed language as it is in, say, Python (leaving a
by Tainnor 4y ago
> "Write a program to sort the words you find in the input file"
That's as trivial to write in a dependently typed language as it is in, say, Python (leaving aside the fact that you don't like monads), e.g. Idris:
main : IO ()
main = do
Right contents <- readFile "myfile.txt"
let theLines = lines contents
let sorted = sort theLines
-- do something with sorted
Of course, that doesn't use any dependent types, but nobody says that you have to use dependent types for a program so trivial you're unlikely to screw anything up.
(And also: the standard library could have instead defined the functions "lines" such that it does use a dependent type. In that case, almost nothing about the program would change, except you would now write "let (n * theLines)" because the length is now part of the return value.)
Dependent types are for where it makes sense to encode invariants, e.g.
matMult : Matrix k m -> Matrix m n -> Matrix k n
And of course, that function works for matrices of arbitrary dimensions, so the argument "we can't know the size of the matrices at compile time" doesn't apply.