Question about the IO monad

Stream: general

[Dhruv Bhatia]

I haven't used lean since Lean3 and have been trying to get back into it. I'm currently trying to relearn how monads work and was playing around with some toy code which is throwing errors at me, but I can't for the life of me understand how to fix it:

def main : IO Unit := do
  IO.println "enter a line of text:"
  let stdin ← IO.getStdin
  let input ← stdin.getLine
  let some fifth ← input[6]? | IO.println "input not long enough"
  IO.println fifth

I think it's pretty clear what I want the code to do - it should read in a user entered line of text, and then attempt to print it's 5th character, provided it is long enough to have a 5th character.

The error shows up at input[6]?and says

type mismatch
  input[6]?
has type
  Option ?m.280 : Type
but is expected to have type
  IO ?m.274 : Type

I suppose the error is caused because bind wants to take in an IO (Option String), not an Option String, which, fair enough. But if that's the case, does that mean I can never nest the Option monad into the IO monad? I saw this in the lean manual:

def showUserInfo (getUsername getFavoriteColor : IO (Option String)) : IO Unit := do
  let some n ← getUsername | IO.println "no username!"
  IO.println s!"username: {n}"
  let some c ← getFavoriteColor | IO.println "user didn't provide a favorite color!"
  IO.println s!"favorite color: {c}"

and I thought: "a-ha! If I just write a function of type String -> IO (Option String) that takes a string and optionally returns it's 5th character, maybe I can fix this". Here's what I tried:

def fifth (str : String) : IO (Option String) := do
  IO.println s!"input: {str}" -- this is just to demonstrate that it is using the IO monad
  return (str[6]?) -- this is the part I really care about

def main : IO Unit := do
  IO.println "enter a line of text:"
  let stdin ← IO.getStdin
  let input ← stdin.getLine
  let some f ← fifth input | IO.println "Input not long enough"
  IO.println f

However, while now main has no complaints, inexplicably str[6]? also throws an error:

failed to synthesize instance
  GetElem String Nat String (?m.358 str x✝)

which I have no clue how to interpret! If someone could please explain what I can do to make this code do what I want, I would really appreciate it! Thanks :)

[Eric Wieser]

In your first example, you want let some fifth := _ not let some fifth ← _; the latter is for when you need to run a monad, but that's not what you have here

[Dhruv Bhatia]

Just tried

def main : IO Unit := do
  IO.println "enter a line of text:"
  let stdin ← IO.getStdin
  let input ← stdin.getLine
  let (some fifth) := input[6]? | IO.println "Input not long enough"
  IO.println fifth

but there's still an error! At input[6]? it says

failed to synthesize instance
  GetElem String Nat ?m.244 ?m.245

which seems like a similar error to my second example above. Any idea what's going on here?

[Arthur Adjedj]

The String type doesn't have the necessary type-classes to use the foo[n] notation. You could either use the function input.get? ⟨6⟩, or add an instance for the notation. Such a notation would look something like this:

instance : GetElem String Nat Char (fun xs i => i < xs.1.length) where
  getElem xs i h := xs.data[i]

[Dhruv Bhatia]

Wow! I guess I never considered the possibility that this instance didn't already exist! Thanks for the help, this fixed it!

[Kim Morrison]

This is a bit sad. Does anyone know an explanation for why there isn't such an instance? Seems like something newcomers will try!

[Mario Carneiro]

Two things: (1) I think it should not take character positions, it should be a byte offset like everything else in the string API (this design is I think borrowed from Rust). But: (2) We don't currently have any way of determining whether a byte position is valid. This would need to be implemented in the C code.

[Mario Carneiro]

indexing by character position is slow because it requires counting up from the bottom of the string. As such I think it's okay that it has the relatively long spelling s.get (s.nextn 0 i)

[Mario Carneiro]

I believe Rust deliberately omits the str[i] indexing syntax though, because this issue with some positions not being valid is a footgun. It's almost never okay to just pick a number and index into the string there, and this is why String.Pos doesn't allow numerals other than 0

[Kim Morrison]

I wonder if we could do something crazy like provide a dummy deprecated GetElem instance, so s[37]? always returned ? or something, but in doing so gave a message explaining what one should be doing.

[Mario Carneiro]

I would love this as an API designer

[Mario Carneiro]

like an erroring version of @[deprecated]

[Eric Wieser]

Does @[deprecated] work on instances?

[Mario Carneiro]

not really

[Mario Carneiro]

the thing that triggers the deprecation check is the ident parser

[Mario Carneiro]

so if you didn't write it directly you won't get a deprecation message

[Mario Carneiro]

which is kind of a problem when you are trying to use deprecation to find and convert all uses

[Mario Carneiro]

we should probably have a backup deprecation linter as an environment linter

[Yaël Dillies]

Is this related to deprecation not triggering when the lemma is used through dot notation?

[Mario Carneiro]

yes, but I think it does trigger in that case?

[Yaël Dillies]

I've encountered a few cases where it didn't this week, but I wouldn't be able to tell you where :thinking:

[Mario Carneiro]

just tested, still broken (on lean4 master too)

[Eric Wieser]

Can't the deprecation linter inspect the infotree somehow?

[Mario Carneiro]

it's not actually a linter, that's the thing

[Mario Carneiro]

it's the elab itself that does the check and pretends to be a linter

[Mario Carneiro]

I'm not exactly sure why it was implemented this way. Maybe @Sebastian Ullrich knows

[Mario Carneiro]

(this is also the source of another bug, mentioned in a TODO in the code: if the identifier is ambiguous and is resolved by the types, it may be too late to take back the deprecation warning if the second attempt is successful and the first attempt is to a deprecated constant)

[Mario Carneiro]

@[deprecated] def A.foo := 1
def B.foo := "hello"
open A B

#check (foo : String)
-- B.foo : String
-- `A.foo` has been deprecated

[Sebastian Ullrich]

It was probably easier to implement it this way but I wasn't involved

[Mario Carneiro]

I was thinking it might predate the linter system

[Mario Carneiro]

do you think it would be reasonable to (submit a PR to) convert it to a linter (and maybe add some other features to it in the process)? There were several independent suggestions for improvement just now here and in the other thread

[Sebastian Ullrich]

Gathering these in an RFC would be a good first step