6.5. Additional Conveniences🔗

6.5.1. Pipe Operators🔗

함수는 보통 인수보다 앞에 쓴다. 프로그램을 왼쪽에서 오른쪽으로 읽을 때 이는 함수의 출력을 가장 중요하게 보는 관점을 만든다. 함수에는 달성할 목표, 즉 계산할 값이 있고, 이 과정에 필요한 인수를 받는다. 하지만 어떤 프로그램은 출력을 만들기 위해 입력을 연속적으로 다듬는 관점에서 이해하는 편이 더 쉽다. 이런 상황을 위해 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. Infinite Loops🔗

do 블록 안에서 repeat 키워드는 무한 루프를 도입한다. 예를 들어 "Spam!" 문자열을 계속 출력하는 프로그램은 이를 사용할 수 있다:

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

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

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

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 Loops🔗

지역 가변성을 사용해 프로그래밍할 때 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의 더 간단한 표기일 뿐이다.