7 ms·

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

by SEMW 9y ago

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.html http://docs.idris-lang.org/en/latest/tutorial/interfaces.htm...

mbrock 9y ago
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 9y ago
If it could fail, wouldn't you want it to return an 'either' type, rather than an int?
- lodi 9y 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.
icen 9y ago
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 9y ago
Haskell definitely has runtime exceptions. It's only relatively pure.

by SEMW 9y ago

mbrock 9y ago

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 9y ago

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

lodi 9y 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.

icen 9y ago

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 9y ago

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