|
|
|
|
|
by lodi
3296 days ago
|
|
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. |
|