`cast` is a lower-level function that isn't really used for parsing strings. Idris has higher level concepts that are more appropriate for that purpose.
For that specific case, you could use an Idris "view" over the string that either gives you a proof that the string is numeric, or a proof that it isn't. Then you have a "stringToInt" method that requires such a proof as one of its parameters. This allows you to write the parsing code as efficiently as possible since you know you'll only work with valid inputs. It's now a compile-time error to forget to check if a string is numeric before attempting to parse it. Also once you obtain a proof of a certain property (in this case by running a runtime check, elsewhere by proving it statically), you can avoid duplicate checks by just passing around the proof object. And of course these proofs are erased at compile time, so the run time code will be similar to an ordinary 'int.TryParse()' method in c# or java, except without the ergonomic issues of using 'out' references or the possibility of accidentally using an uninitialized variable.
I haven't yet tried Idris (or even Haskell), so I could be misunderstanding, but surely in a pure language, a function with a type of String -> Int can't 'blow up', it can only output an Int? So if you want to tell the difference, you'd use something that outputs a (Maybe Int) rather than an Int, which'd be a wrapper around `cast` that does validation you want
Looking at the interfaces tutorial[0], it gives an example of something similar:
readNumber : IO (Maybe Nat)
readNumber = do
input <- getLine
if all isDigit (unpack input)
then pure (Just (cast input))
else pure Nothing
Yes, exactly. Here's the type signature for `cast`:
cast : Cast from to => from -> to
So if the types `from` and `to` are part of the `Cast` typeclass, then cast will always convert one into the other, without "failing". The standard library defines a handful of "sensible" casts like Int to Float, but you can't even attempt to cast a function to a String, or a List to an Int, since those aren't part of the `Cast` typeclass.
For an operation that can fail, like a parse method, a more appropriate return type is `Maybe Int`, or `Either String Int` (where the `String` is an error message).
Also Idris provides a dependently-typed way to connect the check (`all isDigit (unpack input)`) to the conversion itself (`cast input`), so that you can't write an invalid check or forget to include the check at all. See my reply to vosper above.
For that specific case, you could use an Idris "view" over the string that either gives you a proof that the string is numeric, or a proof that it isn't. Then you have a "stringToInt" method that requires such a proof as one of its parameters. This allows you to write the parsing code as efficiently as possible since you know you'll only work with valid inputs. It's now a compile-time error to forget to check if a string is numeric before attempting to parse it. Also once you obtain a proof of a certain property (in this case by running a runtime check, elsewhere by proving it statically), you can avoid duplicate checks by just passing around the proof object. And of course these proofs are erased at compile time, so the run time code will be similar to an ordinary 'int.TryParse()' method in c# or java, except without the ergonomic issues of using 'out' references or the possibility of accidentally using an uninitialized variable.