Why is this function not failing

Stream: new members

[Jafar Tanoukhi]

I am new to functional programming and lean in general, i decided to start learning by reading the "functional programming with lean" book and now im translating an interpreter i made in java to lean as my first project
I wrote this parsing function (that only handles three tokens now) but im not sure why it does not hit a stack overflow even with a huge text input.
Why i believe it should is because i believe this is pushing a new frame to the stack for every character in the content string.
Heres the code :

def parseChar : (word : Char) -> Option Token
| '!' => some Token.BANG
| '=' => some Token.EQUAL
| '>' => some Token.GREATER
| _ => none

partial def parseContent (content : String) : List Token :=
  let rec parseHelper (content : List Char) (tokens : List Token) : List Token :=
    match content with
    | [] => tokens
    | c :: cs =>
      match parseChar c with
      | some Token.BANG => parseHelper cs (Token.BANG :: tokens)
      | some Token.EQUAL => parseHelper cs (Token.EQUAL :: tokens)
      | some Token.GREATER =>
        match cs with
        | '=' :: rest => parseHelper rest (Token.GREATER_EQUAL :: tokens)
        | _ => parseHelper cs (Token.GREATER :: tokens)
      | _ => parseHelper cs tokens
  parseHelper content.toList []

[Ted Hwa]

If I read the code correctly, the function is tail-recursive so the compiler can optimize it to not use the stack at all for the recursive calls.

[Jafar Tanoukhi]

Oh i did find something about tail recursion when i was trying to figure out what's happening before asking here. Can you point out how is this tail recursive ? Im not sure i understand what is tail recursion in general, is it a functional programming thing?

[Ted Hwa]

All of your recursive calls are in the form parseHelper ... with no further operations (if instead, it was something like f (parseHelper ...), then it would not be tail-recursive because there would be another operation f after the recursive call). Therefore, the stack is not needed because when we return from the recursive call, there is nothing left to do, so we do not need to restore the previous values from the stack.

Tail-call optimization can be applied in any language but it is particularly important in functional programming languages because they tend to use recursion a lot more than other languages.

[Jafar Tanoukhi]

Ahhh ok that makes sense, thanks for this explanation

[Ted Hwa]

See also: https://lean-lang.org/functional_programming_in_lean/programs-proofs/tail-recursion.html#tail-and-non-tail-positions

[Jafar Tanoukhi]

Also, i would like to ask another question, i've been told the usage of partial is bad practice and i should not have to use it, but without the partial keyword here, lean shouts at me that the function does not terminate. From that i understand i need to write code in a way that proves to lean that this recursion terminates but i am not sure how to do it in my code.

[Jafar Tanoukhi]

Ted Hwa said:

See also: https://lean-lang.org/functional_programming_in_lean/programs-proofs/tail-recursion.html#tail-and-non-tail-positions

Oh thanks for this, i will check this out

[pandaman]

I could convince Lean to accept your definition without partial. Somehow Lean seems to forget cs is smaller at the offending branch.

def parseContent (content : String) : List Token :=
  let rec parseHelper (content : List Char) (tokens : List Token) : List Token :=
    match content with
    | [] => tokens
    | c :: cs =>
      match parseChar c with
      | some Token.BANG => parseHelper cs (Token.BANG :: tokens)
      | some Token.EQUAL => parseHelper cs (Token.EQUAL :: tokens)
      | some Token.GREATER =>
        match cs with
        | '=' :: rest => parseHelper rest (Token.GREATER_EQUAL :: tokens)
        | cs => parseHelper cs (Token.GREATER :: tokens) -- introduce cs again
      | _ => parseHelper cs tokens
  parseHelper content.toList []

[Jafar Tanoukhi]

Oh this is pretty cool but i dont understand, why does it work, isn't matching with _ and with cs the same ?

[Mark Fischer]

Well, the only difference from a proof perspective is that you know the re-introduced cs doesn't start with =. Which shouldn't matter.

Something I noticed is that if you use a dependent match, then lean can see the termination. So this is accepted:

def parseContent (content : String) : List Token :=
  let rec parseHelper (content : List Char) (tokens : List Token) : List Token :=
    match content with
    | [] => tokens
    | c :: cs =>
      match parseChar c with
      | some Token.BANG => parseHelper cs (Token.BANG :: tokens)
      | some Token.EQUAL => parseHelper cs (Token.EQUAL :: tokens)
      | some Token.GREATER =>
        match _h : cs with
        | '=' :: rest => parseHelper rest (Token.GREATER_EQUAL :: tokens)
        | _ => parseHelper cs (Token.GREATER :: tokens)
      | _ => parseHelper cs tokens
    termination_by content.length
  parseHelper content.toList []

[Jafar Tanoukhi]

hmmm, i didn't know about dependent matches, this looks pretty interesting, i will look into it

[Jafar Tanoukhi]

Thanks