[SEMW]

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

[0] http://docs.idris-lang.org/en/latest/tutorial/interfaces.htm...

[mbrock]

In Haskell, such a function can definitely blow up.

    > :t read
    read :: Read a => String -> a
    > read "10" :: Int
    10
    > read "x" :: Int
    *** Exception: Prelude.read: no parse

Haskell functions are pure, but not necessarily total.

[empath75]

If it could fail, wouldn't you want it to return an 'either' type, rather than an int?

[lodi]

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.

[icen]

And this is the case in Idris, where `cast` is a member of the `Cast` interface, and there's an implementation of `Cast String Integer`.

`cast` is a function `String -> Integer`, instead of the (more sensible) `String -> Either Integer CastError`.

[sullyj3]

Haskell definitely has runtime exceptions. It's only relatively pure.