kmeredith (23) [Avatar] Offline
#1
String -> Nat
Ch 5 introduces:

readNumber : IO (Maybe Nat)
readNumber = do
    input <- getLine
    if all isDigit (unpack input)
    then pure (Just (cast input))
    else pure Nothing


However, it does not compile on v.0.9.19.1.

*IllegalCode> :r
Type checking ./IllegalCode.idr
IllegalCode.idr:2:12:
When checking right hand side of readNumber:
Can't cast from String to Nat
Holes: Main.readNumber


How can this be fixed?

Thanks
Edwin Brady (65) [Avatar] Offline
#2
String -&gt; Nat
Hi, sorry for slowness... You probably just need to upgrade to the latest version. I'm now putting version requirements at the top of each chapter, since there is some development of Idris going along side writing the book.
kmeredith (23) [Avatar] Offline
#3
String -&gt; Nat
Thanks. Using v 0.10.2 worked for me:

Idris> the Nat (cast "5")
5 : Nat


However, isn't there a risk of a run-time exception when trying to cast from String -> Nat?

Idris> the Nat (cast "foo")
if with block in Prelude.Interfaces.Prelude.Interfaces.Integer implementation of Prelude.Interfaces.Ord, method > (if intToBool (prim__eqBigInt 0
                           0)
then EQ
else if intToBool (prim__sltBigInt 0
                                   0)
       then LT
       else GT)
0
0
  then S (fromIntegerNat (prim__subBigInt 0 1))
  else 0 : Nat


In short, I'm concerned about an un-safe cast causing a run-time error.
Edwin Brady (65) [Avatar] Offline
#4
String -&gt; Nat
This is a good point - 'cast' is really just intended for lightweight casting, and rather than checking it'll return a default value (not sure why your example doesn't, I'll take a closer look...). This isn't written in the documentation for cast (at the moment) but it really should be.

It'd probably be a good idea to have something a bit more precise here, perhaps safe and unsafe variants of cast.
xaviervia (2) [Avatar] Offline
#5
String -&gt; Nat
Hi,

just for reference: I’m getting a runtime error as well. I’m not sure what the issue is smilie

The code is:

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
    then pure (Just (cast input))
    else pure Nothing


and the error I’m getting:

*5_1_Hello> :exec readNumber
main:When checking argument value to function Prelude.Basics.the:
        Type mismatch between
                IO (Maybe Nat) (Type of readNumber)
        and

                Integer (Expected type)


I just updated to Idris v1.0 and it still reproduces.

Thanks!
xaviervia (2) [Avatar] Offline
#6
String -&gt; Nat

I see that doing

:exec readNumber >>= printLn


works, but I’m pretty curious of why, since printLn only specifies that it's input should implement Show:

printLn : Show ty => ty -> IO ()


In my mind this means that it does not add more information to cast that it did not already have, since cast is supposed to output Nat, not just any type that has an implementation for Show