6.5. 추가 편의 기능🔗

6.5.1. 파이프 연산자🔗

함수는 일반적으로 인자보다 앞에 작성됩니다. 프로그램을 왼쪽에서 오른쪽으로 읽을 때, 이는 함수의 출력이 가장 중요하다는 관점을 촉진합니다—함수에는 달성해야 할 목표(즉, 계산해야 할 값)가 있으며, 이 과정을 돕기 위해 인자를 받습니다. 하지만 일부 프로그램은 입력을 점진적으로 정제하여 출력을 만들어내는 방식으로 설명하는 편이 이해하기 더 쉽습니다. 이러한 상황을 위해 Lean은 F#에서 제공하는 것과 유사한 파이프라인 연산자를 제공합니다. 파이프라인 연산자는 Clojure의 스레딩 매크로가 유용한 상황과 동일한 상황에서 유용합니다.

파이프라인 E₁ |> E₂는 E₂ E₁의 축약형입니다. 예를 들어, 다음을 평가하면:

"(some 5)"#eval some 5 |> toString

결과는 다음과 같습니다:

"(some 5)"

이러한 강조점의 변화가 일부 프로그램을 더 읽기 편하게 만들 수는 있지만, 파이프라인은 많은 구성 요소를 포함할 때 진정한 진가를 발휘합니다.

다음 정의를 사용하면:

def times3 (n : Nat) : Nat := n * 3

다음 파이프라인:

"It is 15"#eval 5 |> times3 |> toString |> ("It is " ++ ·)

다음과 같은 결과를 냅니다:

"It is 15"

더 일반적으로, 일련의 파이프라인 E₁ |> E₂ |> E₃ |> E₄는 중첩된 함수 적용 E₄ (E₃ (E₂ E₁))의 축약형입니다.

파이프라인은 반대 방향으로 작성할 수도 있습니다. 이 경우에는 데이터 변환의 주체를 앞에 두지는 않지만, 중첩된 괄호가 많아 독자가 이해하기 어려운 경우에는 적용 단계를 명확히 할 수 있습니다. 앞의 예제는 다음과 같이 동등하게 작성될 수 있습니다:

"It is 15"#eval ("It is " ++ ·) <| toString <| times3 <| 5

다음의 축약형입니다:

"It is 15"#eval ("It is " ++ ·) (toString (times3 5))

점 앞에 있는 타입의 이름을 사용하여 점 뒤에 있는 연산자의 네임스페이스를 해석하는 Lean의 메서드 점 표기법은 파이프라인과 유사한 목적을 수행합니다. 파이프라인 연산자 없이도 List.reverse [1, 2, 3] 대신 [1, 2, 3].reverse라고 쓸 수 있습니다. 하지만 파이프라인 연산자는 점으로 연결된 함수를 여러 개 사용할 때도 유용합니다. ([1, 2, 3].reverse.drop 1).reverse는 [1, 2, 3] |> List.reverse |> List.drop 1 |> List.reverse로도 쓸 수 있습니다. 이 방식은 표현식이 단지 인자를 받는다는 이유만으로 괄호로 묶어야 하는 상황을 피할 수 있게 해 주며, Kotlin이나 C# 같은 언어에서 메서드 호출을 연쇄하는 편의성을 되살립니다. 하지만 이 경우에도 여전히 네임스페이스를 직접 제공해야 합니다. 마지막으로 편의를 위해, Lean은 파이프라인처럼 함수를 묶어 주지만 네임스페이스를 해결하는 데 타입의 이름을 사용하는 “파이프라인 점(pipeline dot)” 연산자를 제공합니다. "파이프라인 점(pipeline dot)"을 사용하면 이 예제를 [1, 2, 3] |>.reverse |>.drop 1 |>.reverse와 같이 다시 작성할 수 있습니다.

6.5.2. 무한 루프🔗

do-블록 내에서, repeat 키워드는 무한 루프를 도입합니다. 예를 들어, "Spam!" 문자열을 스팸으로 반복 출력하는 프로그램은 이를 사용할 수 있습니다:

def spam : IO Unit := do
  repeat IO.println "Spam!"

repeat 루프는 for 루프와 마찬가지로 break와 continue를 지원합니다.

feline의 구현에 있는 dump 함수는 재귀 함수를 사용해 영원히 실행됩니다:

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

이 함수는 repeat를 사용하면 크게 단축할 수 있습니다:

def dump (stream : IO.FS.Stream) : IO Unit := do
  let stdout ← IO.getStdout
  repeat do
    let buf ← stream.read bufsize
    if buf.isEmpty then break
    stdout.write buf

spam과 dump는 그 자체로 무한히 재귀하지 않기 때문에 둘 다 partial로 선언할 필요가 없습니다. 대신, repeat는 ForM 인스턴스가 partial인 타입을 사용합니다. 부분성(partiality)은 호출하는 함수에 "전염"되지 않습니다.

6.5.3. While 루프🔗

지역 가변성을 사용하여 프로그래밍할 때, while 루프는 if로 보호된 break를 사용하는 repeat의 편리한 대안이 될 수 있습니다:

def dump (stream : IO.FS.Stream) : IO Unit := do
  let stdout ← IO.getStdout
  let mut buf ← stream.read bufsize
  while not buf.isEmpty do
    stdout.write buf
    buf ← stream.read bufsize

내부적으로 while은 repeat의 더 간단한 표기법일 뿐입니다.