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은 “파이프라인 점” 연산자를 제공합니다. 이 연산자는 파이프라인처럼 함수를 묶으면서도 타입의 이름을 사용해 네임스페이스를 결정합니다. “파이프라인 점”을 사용하면 앞의 예시를 [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인 타입을 사용합니다. 부분성은 이를 호출하는 함수로 “전염”되지 않습니다.

6.5.3. While 루프🔗

지역 가변성을 사용해 프로그래밍할 때는 if로 보호된 break와 함께 repeat를 쓰는 방식 대신 while 루프를 사용하면 편리할 수 있습니다:

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을 더 간단하게 쓰는 표기법일 뿐입니다.