Hacker News Reader

Comment by zimbatm | Hacker News Reader

I am not a fan of `cast` (also seen in other languages as well) as it leads to reductionist thinking.

There are usually more than one way to convert from one type to another. How is Float to Int rounded? Shouldn't String to Int return conversion errors? Just looking at `cast` means I have to learn what the language decided to default to.

View on HN

You should be able to write your own named implementation of Cast and explicitly use it when calling cast to have different casts with different semantics http://docs.idris-lang.org/en/latest/tutorial/interfaces.htm.... But yeah, you'd still have to see what the standard library implementation does

String to int returning 0 for an uncastable string seems like a terrible design. It should blow up. How otherwise can you tell between "0" and "ABC"?

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...

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.

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

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.

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`.

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

`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.

> these proofs are erased at compile time

are you certain about that? my understanding was that witness terms are indeed passed at runtime especially for non-total functions

Reply on news.ycombinator.com