Note
์ด ๊ธ์ Lean ๊ณต์ ๋ฌธ์์ ์๊ฐ๋ Functional Programming in Lean์ ์์ฑ์๊ฐ ์ฝ๊ธฐ ์ํ ๋ชฉ์ ์ผ๋ก Kagi Translate๋ฅผ ํตํด 1์ฐจ๋ก ๊ธฐ๊ณ ๋ฒ์ญ ํ ๋ณด์ํ ๊ธ์
๋๋ค.
์๋ฌธ๊ณผ์ ์ฐจ์ด๊ฐ ์์ ์ ์์ผ๋ฉฐ ์ ์ ๋ด์ฉ์ ํญ์ ์๋ฌธ์ ํตํด ํ์ธ ๋ฐ๋๋๋ค.
์๋ฌธ์ด Creative Commons Attribution 4.0 International License๋ฅผ ๊ธฐ๋ฐ์ผ๋ก ๋ฐฐํฌ๋ ๊ฒ์ ์กด์คํ์ฌ ์ด ๊ธ ๋ํ CC BY 4.0 ํ์ ๋ฐฐํฌํฉ๋๋ค.
์๊ฐ
Lean์ ์์กด ํ์
์ด๋ก ์ ๊ธฐ๋ฐ์ผ๋ก ํ๋ ๋ํํ ์ ๋ฆฌ ์ฆ๋ช
๊ธฐ ์
๋๋ค. ์๋ Microsoft Research์์ ๊ฐ๋ฐ๋์์ผ๋, ํ์ฌ๋ Lean FRO์์ ๊ฐ๋ฐ์ด ์งํ๋๊ณ ์์ต๋๋ค. ์์กด ํ์
์ด๋ก ์ ํ๋ก๊ทธ๋จ๊ณผ ์ฆ๋ช
์ ์ธ๊ณ๋ฅผ ํ๋๋ก ๋ฌถ์ด์ฃผ๊ธฐ ๋๋ฌธ์ Lean์ ํ๋ก๊ทธ๋๋ฐ ์ธ์ด์ด๊ธฐ๋ ํฉ๋๋ค. Lean์ ์ด๋ฌํ ์ด์ค์ ํน์ฑ์ ์ง์งํ๊ฒ ๋ฐ์๋ค์ด๋ฉฐ, ๋ฒ์ฉ ํ๋ก๊ทธ๋๋ฐ ์ธ์ด๋ก ์ฌ์ฉํ๊ธฐ์ ์ ํฉํ๋๋ก ์ค๊ณ๋์์ต๋๋ค. ์ฌ์ง์ด Lean์ Lean ์์ฒด๋ก ๊ตฌํ๋์ด ์์ต๋๋ค. ์ด ์ฑ
์ Lean์ผ๋ก ํ๋ก๊ทธ๋จ์ ์์ฑํ๋ ๋ฒ์ ๊ดํ ๊ฒ์
๋๋ค.
ํ๋ก๊ทธ๋๋ฐ ์ธ์ด๋ก์์ Lean์ ์์กด ํ์
์ ๊ฐ์ง ์๊ฒฉํ ์์ ํจ์ํ ์ธ์ด์
๋๋ค. Lean์ผ๋ก ํ๋ก๊ทธ๋๋ฐํ๋ ๋ฒ์ ๋ฐฐ์ฐ๋ ๊ณผ์ ์ ์๋น ๋ถ๋ถ์ ์ด๋ฌํ ๊ฐ ์์ฑ์ด ํ๋ก๊ทธ๋จ ์์ฑ ๋ฐฉ์์ ์ด๋ค ์ํฅ์ ๋ฏธ์น๋์ง, ๊ทธ๋ฆฌ๊ณ ์ด๋ป๊ฒ ํจ์ํ ํ๋ก๊ทธ๋๋จธ์ฒ๋ผ ์๊ฐํ ์ ์๋์ง๋ฅผ ์ตํ๋ ๊ฒ์ผ๋ก ๊ตฌ์ฑ๋ฉ๋๋ค. ์๊ฒฉ์ฑ ์ Lean์ ํจ์ ํธ์ถ์ด ๋๋ถ๋ถ์ ์ธ์ด์ ์ ์ฌํ๊ฒ ์๋ํ๋ ๊ฒ์ ์๋ฏธํฉ๋๋ค. ์ฆ, ํจ์์ ๋ณธ๋ฌธ์ด ์คํ๋๊ธฐ ์ ์ ์ธ์๊ฐ์ด ์์ ํ ๊ณ์ฐ๋๋ค๋ ์๋ฏธ์
๋๋ค. ์์์ฑ ์ ํ๋ก๊ทธ๋จ์์ ํ์
์ ๋ช
์๋์ง ์๋ ํ, Lean ํ๋ก๊ทธ๋จ์ด ๋ฉ๋ชจ๋ฆฌ ์์น ์์ , ์ด๋ฉ์ผ ์ ์ก, ํ์ผ ์ญ์ ์ ๊ฐ์ ๋ถ์ ํจ๊ณผ(side effect)๋ฅผ ๊ฐ์ง ์ ์์์ ์๋ฏธํฉ๋๋ค. Lean์ด ํจ์ํ ์ธ์ด๋ผ๋ ๊ฒ์ ํจ์๊ฐ ๋ค๋ฅธ ๊ฐ๋ค๊ณผ ๋ง์ฐฌ๊ฐ์ง๋ก ์ผ๊ธ ๊ฐ์ฒด์ด๋ฉฐ, ์คํ ๋ชจ๋ธ์ด ์ํ์ ํํ์์ ํ๊ฐ์์ ์๊ฐ์ ์ป์์์ ๋ปํฉ๋๋ค. Lean์ ๊ฐ์ฅ ๋
ํนํ ํน์ง์ธ ์์กด ํ์
์ ํ์
์ ์ธ์ด์ ์ผ๊ธ ๊ตฌ์ฑ ์์๋ก ๋ง๋ค์ด, ํ์
์ด ํ๋ก๊ทธ๋จ์ ํฌํจํ๊ฑฐ๋ ํ๋ก๊ทธ๋จ์ด ํ์
์ ๊ณ์ฐํ ์ ์๊ฒ ํฉ๋๋ค.
์ด ์ฑ
์ Lean์ ๋ฐฐ์ฐ๊ณ ์ถ์ง๋ง ๋ฐ๋์ ํจ์ํ ํ๋ก๊ทธ๋๋ฐ ์ธ์ด๋ฅผ ์ฌ์ฉํด ๋ณธ ์ ์ ์๋ ํ๋ก๊ทธ๋๋จธ๋ค์ ๋์์ผ๋ก ํฉ๋๋ค. Haskell, OCaml, F#๊ณผ ๊ฐ์ ํจ์ํ ์ธ์ด์ ์ต์ํ ํ์๋ ์์ต๋๋ค. ๋ฐ๋ฉด, ์ด ์ฑ
์ ๋๋ถ๋ถ์ ํ๋ก๊ทธ๋๋ฐ ์ธ์ด์์ ๊ณตํต์ ์ผ๋ก ์ฐ์ด๋ ๋ฃจํ, ํจ์, ๋ฐ์ดํฐ ๊ตฌ์กฐ์ ๊ฐ์ ๊ฐ๋
์ ๋ํ ์ง์์ ๊ฐ์ถ๊ณ ์๋ค๊ณ ๊ฐ์ ํฉ๋๋ค. ์ด ์ฑ
์ด ํจ์ํ ํ๋ก๊ทธ๋๋ฐ์ ๊ดํ ์ข์ ์
๋ฌธ์๊ฐ ๋ ์๋ ์์ง๋ง, ํ๋ก๊ทธ๋๋ฐ ์ ๋ฐ์ ๊ดํ ์
๋ฌธ์๋ก๋ ์ ํฉํ์ง ์์ต๋๋ค.
Lean์ ์ฆ๋ช
๋ณด์กฐ๊ธฐ๋ก ์ฌ์ฉํ๋ ์ํ์๋ค๋ ์ธ์ ๊ฐ๋ ๋ง์ถคํ ์ฆ๋ช
์๋ํ ๋๊ตฌ๋ฅผ ์์ฑํด์ผ ํ ๋๊ฐ ์ฌ ๊ฒ์
๋๋ค. ์ด ์ฑ
์ ๊ทธ๋ถ๋ค์ ์ํ ๊ฒ์ด๊ธฐ๋ ํฉ๋๋ค. ์ด๋ฌํ ๋๊ตฌ๋ค์ด ์ ๊ตํด์ง์๋ก ํจ์ํ ์ธ์ด์ ํ๋ก๊ทธ๋จ๊ณผ ๋ฎ์๊ฐ์ง๋ง, ๋๋ถ๋ถ์ ํ์ง ์ํ์๋ค์ Python์ด๋ Mathematica ๊ฐ์ ์ธ์ด์ ์ต์ํฉ๋๋ค. ์ด ์ฑ
์ ๊ทธ ๊ฐ๊ทน์ ๋ฉ์์ค์ผ๋ก์จ ๋ ๋ง์ ์ํ์๊ฐ ์ ์ง๋ณด์ ๊ฐ๋ฅํ๊ณ ์ดํดํ๊ธฐ ์ฌ์ด ์ฆ๋ช
์๋ํ ๋๊ตฌ๋ฅผ ์์ฑํ ์ ์๋๋ก ๋์ธ ๊ฒ์
๋๋ค.
์ด ์ฑ
์ ์ฒ์๋ถํฐ ๋๊น์ง ์์๋๋ก ์ฝ๋๋ก ๊ตฌ์ฑ๋์์ต๋๋ค. ๊ฐ๋
์ ํ๋์ฉ ๋์
๋๋ฉฐ, ๋ท๋ถ๋ถ์ ์๋ถ๋ถ์ ๋ด์ฉ์ ์์งํ๊ณ ์๋ค๊ณ ๊ฐ์ ํฉ๋๋ค. ๋๋ก๋ ์์ ์งง๊ฒ ๋ค๋ฃจ์๋ ์ฃผ์ ๋ฅผ ๋์ค์ ๋ ๊น์ด ์๊ฒ ํ๊ณ ๋ค๊ธฐ๋ ํฉ๋๋ค. ์ฑ
์ ์ผ๋ถ ์น์
์๋ ์ฐ์ต ๋ฌธ์ ๊ฐ ํฌํจ๋์ด ์์ต๋๋ค. ํด๋น ์น์
์ ์ดํด๋ฅผ ๊ณต๊ณ ํ ํ๊ธฐ ์ํด ํ์ด๋ณผ ๊ฐ์น๊ฐ ์์ต๋๋ค. ๋ํ ์ฑ
์ ์ฝ์ผ๋ฉด์ ๋ฐฐ์ด ๋ด์ฉ์ ์ฐฝ์์ ์ด๊ณ ์๋ก์ด ๋ฐฉ์์ผ๋ก ํ์ฉํ๋ฉฐ Lean์ ์ง์ ํ๊ตฌํด ๋ณด๋ ๊ฒ๋ ์ ์ตํฉ๋๋ค.
Lean ์์ํ๊ธฐ
Lean์ผ๋ก ์์ฑ๋ ํ๋ก๊ทธ๋จ์ ์์ฑํ๊ณ ์คํํ๊ธฐ ์ ์, ๋จผ์ ์ปดํจํฐ์ Lean์ ์ค์นํด์ผ ํฉ๋๋ค.
Lean ๋๊ตฌ ๋ชจ์์ ๋ค์๊ณผ ๊ฐ์ด ๊ตฌ์ฑ๋ฉ๋๋ค:
elan์ rustup์ด๋ ghcup๊ณผ ์ ์ฌํ๊ฒ Lean ์ปดํ์ผ๋ฌ ํด์ฒด์ธ์ ๊ด๋ฆฌํฉ๋๋ค.
lake๋ cargo, make, ๋๋ Gradle๊ณผ ์ ์ฌํ๊ฒ Lean ํจํค์ง์ ๊ทธ ์์กด์ฑ์ ๋น๋ํฉ๋๋ค.
lean์ ๊ฐ๋ณ Lean ํ์ผ์ ํ์
์ ๊ฒ์ฌํ๊ณ ์ปดํ์ผํ๋ฉฐ, ํ์ฌ ์์ฑ ์ค์ธ ํ์ผ์ ๋ํ ์ ๋ณด๋ฅผ ํ๋ก๊ทธ๋๋จธ ๋๊ตฌ์ ์ ๊ณตํฉ๋๋ค.
๋ณดํต lean์ ์ฌ์ฉ์๊ฐ ์ง์ ์คํํ๊ธฐ๋ณด๋ค๋ ๋ค๋ฅธ ๋๊ตฌ์ ์ํด ํธ์ถ๋ฉ๋๋ค.
- Visual Studio Code๋ Emacs์ ๊ฐ์ ์๋ํฐ์ฉ ํ๋ฌ๊ทธ์ธ์
lean๊ณผ ํต์ ํ์ฌ ๊ด๋ จ ์ ๋ณด๋ฅผ ํธ๋ฆฌํ๊ฒ ๋ณด์ฌ์ค๋๋ค.
Lean ์ค์น์ ๊ดํ ์ต์ ์ง์นจ์ Lean ๋งค๋ด์ผ์ ์ฐธ์กฐํ์๊ธฐ ๋ฐ๋๋๋ค.
ํ์ดํฌ๊ทธ๋ํผ ๊ด๋ก
Lean์ ์
๋ ฅ์ผ๋ก ์ ๊ณต๋๋ ์ฝ๋ ์์ ๋ ๋ค์๊ณผ ๊ฐ์ ํ์์ผ๋ก ํ์๋ฉ๋๋ค:
def add1 (n : Nat) : Nat := n + 1
#eval add1 7
์์ ๋ง์ง๋ง ์ค(#eval๋ก ์์ํ๋ ์ค)์ Lean์๊ฒ ๋ต์ ๊ณ์ฐํ๋๋ก ์ง์ํ๋ ๋ช
๋ น์
๋๋ค.
Lean์ ์๋ต์ ๋ค์๊ณผ ๊ฐ์ ํ์์ผ๋ก ํ์๋ฉ๋๋ค:
8
Lean์ด ๋ฐํํ๋ ์ค๋ฅ ๋ฉ์์ง๋ ๋ค์๊ณผ ๊ฐ์ ํ์์ผ๋ก ํ์๋ฉ๋๋ค:
Application type mismatch: The argument
"seven"
has type
String
but is expected to have type
Nat
in the application
add1 "seven"
๊ฒฝ๊ณ ๋ ๋ค์๊ณผ ๊ฐ์ ํ์์ผ๋ก ํ์๋ฉ๋๋ค:
declaration uses 'sorry'
์ ๋์ฝ๋
๊ด์ฉ์ ์ธ Lean ์ฝ๋๋ ASCII์ ํฌํจ๋์ง ์๋ ๋ค์ํ ์ ๋์ฝ๋ ๋ฌธ์๋ฅผ ์ฌ์ฉํฉ๋๋ค.
์๋ฅผ ๋ค์ด, ๊ทธ๋ฆฌ์ค ๋ฌธ์ ฮฑ, ฮฒ ๋ฐ ํ์ดํ โ๋ ๋ชจ๋ ์ด ์ฑ
์ ์ฒซ ๋ฒ์งธ ์ฅ์ ๋ฑ์ฅํฉ๋๋ค.
์ด๋ฅผ ํตํด Lean ์ฝ๋๋ ์ผ๋ฐ์ ์ธ ์ํ์ ํ๊ธฐ๋ฒ๊ณผ ๋ ์ ์ฌํด์ง ์ ์์ต๋๋ค.
๊ธฐ๋ณธ Lean ์ค์ ์์ Visual Studio Code์ Emacs ๋ชจ๋ ๋ฐฑ์ฌ๋์(\) ๋ค์ ์ด๋ฆ์ ์
๋ ฅํ์ฌ ์ด๋ฌํ ๋ฌธ์๋ฅผ ์
๋ ฅํ ์ ์์ต๋๋ค.
์๋ฅผ ๋ค์ด, ฮฑ๋ฅผ ์
๋ ฅํ๋ ค๋ฉด \alpha๋ฅผ ์
๋ ฅํฉ๋๋ค.
Visual Studio Code์์ ๋ฌธ์๋ฅผ ์
๋ ฅํ๋ ๋ฐฉ๋ฒ์ ์์๋ณด๋ ค๋ฉด ํด๋น ๋ฌธ์ ์์ ๋ง์ฐ์ค๋ฅผ ์ฌ๋ ค ํดํ์ ํ์ธํ์ธ์.
Emacs์์๋ ํด๋น ๋ฌธ์ ์์ ์ปค์๋ฅผ ๋๊ณ C-c C-k๋ฅผ ์ฌ์ฉํ์ธ์.
์ ์ ์๊ฐ
David Thrane Christiansen ์ 20๋
๋์ ํจ์ํ ์ธ์ด๋ฅผ ์ฌ์ฉํด ์์ผ๋ฉฐ, ์์กด ํ์
์ ์ฌ์ฉํ ์ง๋ 10๋
์ด ๋์์ต๋๋ค. ๊ทธ๋ Daniel P. Friedman๊ณผ ํจ๊ป ์์กด ์๋ฃํ ์ด๋ก ์ ํต์ฌ ์์ด๋์ด๋ฅผ ์๊ฐํ๋ The Little Typer ๋ฅผ ์งํํ์ต๋๋ค. ์ฝํํ๊ฒ IT ๋ํ๊ต์์ ๋ฐ์ฌ ํ์๋ฅผ ๋ฐ์์ผ๋ฉฐ, ์ฌํ ์์ Idris ์ธ์ด์ ์ฒซ ๋ฒ์งธ ๋ฒ์ ์ ์ฃผ์ ๊ธฐ์ฌ์๋ก ์ฐธ์ฌํ์ต๋๋ค. ํ๊ณ๋ฅผ ๋ ๋ ํ์๋ ๋ฏธ๊ตญ ์ค๋ฆฌ๊ฑด์ฃผ ํฌํ๋๋์ Galois์ ๋ด๋งํฌ ์ฝํํ๊ฒ์ Deon Digital์์ ์ํํธ์จ์ด ๊ฐ๋ฐ์๋ก ์ผํ์ผ๋ฉฐ, Haskell Foundation์ ์์ ์ด์ฌ๋ฅผ ์ญ์ํ์ต๋๋ค. ์งํ ๋น์ ๊ทธ๋ Lean Focused Research Organization ์ ์์๋์ด ํํ์์ผ๋ก Lean ํ๋ก์ ํธ์ ๋งค์งํ๊ณ ์์ต๋๋ค.
๊ฐ์ฌ์ ๊ธ
์ด ๋ฌด๋ฃ ์จ๋ผ์ธ ๋์๋ Microsoft Research์ ์๋์๋ ์ง์ ๋๋ถ์ ์งํ ๋ฐ ๋ฌด๋ฃ ๋ฐฐํฌ๊ฐ ๊ฐ๋ฅํ์ต๋๋ค. ์งํ ๊ณผ์ ์์ ๊ทธ๋ค์ Lean ๊ฐ๋ฐํ์ ์ ๋ฌธ ์ง์์ ์ ๊ณตํ์ฌ ์ ์ง๋ฌธ์ ๋ตํด์ฃผ๊ณ Lean์ ๋ ์ฌ์ฉํ๊ธฐ ์ฝ๊ฒ ๋ง๋ค์ด ์ฃผ์์ต๋๋ค. ํนํ Leonardo de Moura๋ ์ด ํ๋ก์ ํธ๋ฅผ ์์ํ๊ณ ์ ๊ฐ ์ฒซ๋ฐ์ ๋ ์ ์๊ฒ ๋์์ฃผ์์ผ๋ฉฐ, Chris Lovett์ CI ๋ฐ ๋ฐฐํฌ ์๋ํ๋ฅผ ๊ตฌ์ถํ๊ณ ํ
์คํธ ๋
์๋ก์ ํ๋ฅญํ ํผ๋๋ฐฑ์ ์ฃผ์์ต๋๋ค. Gabriel Ebner๋ ๊ธฐ์ ๊ฒํ ๋ฅผ ๋งก์๊ณ , Sarah Smith๋ ํ์ ์ ์ธ ์
๋ฌด๊ฐ ์ํํ ๋์๊ฐ๋๋ก ํ์จ์ฃผ์์ผ๋ฉฐ, Vanessa Rodriguez๋ ์์ค ์ฝ๋ ํ์ด๋ผ์ดํธ ๋ผ์ด๋ธ๋ฌ๋ฆฌ์ ํน์ ๋ฒ์ ์ iOS์ฉ Safari ๊ฐ์ ๊น๋ค๋ก์ด ์ํธ์์ฉ ๋ฌธ์ ๋ฅผ ์ง๋จํ๋ ๋ฐ ๋์์ ์ฃผ์์ต๋๋ค.
์ด ์ฑ
์ ์ฐ๋ ๋ฐ๋ ํ์ ๊ทผ๋ฌด ์๊ฐ ์ธ์๋ ๋ง์ ์๊ฐ์ด ์์๋์์ต๋๋ค. ์ ์๋ด Ellie Thrane Christiansen์ ํ์๋ณด๋ค ๋ ๋ง์ ๊ฐ์ฌ ๋ถ๋ด์ ๋๋งก์ ์ฃผ์์ผ๋ฉฐ, ์๋ด์ ํ์ ์ด ์์๋ค๋ฉด ์ด ์ฑ
์ ์กด์ฌํ ์ ์์์ ๊ฒ์
๋๋ค. ๋งค์ฃผ ํ๋ฃจ์ฉ ์ถ๊ฐ๋ก ์ผํ๋ ๊ฒ์ด ๊ฐ์กฑ๋ค์๊ฒ ์ฝ์ง ์์ ์ผ์ด์์์๋, ์งํ ๊ธฐ๊ฐ ๋์ ์ธ๋ด์ฌ์ ๊ฐ๊ณ ์ง์งํด ์ค ๊ฐ์กฑ๋ค์๊ฒ ๊ฐ์ฌ์ ๋ง์์ ์ ํฉ๋๋ค.
Lean์ ๋๋ฌ์ผ ์จ๋ผ์ธ ์ปค๋ฎค๋ํฐ๋ ๊ธฐ์ ์ ์ผ๋ก๋ ์ ์์ ์ผ๋ก ์ด ํ๋ก์ ํธ์ ์ด๋ ฌํ ์ง์ง๋ฅผ ๋ณด๋ด์ฃผ์์ต๋๋ค. ํนํ Sebastian Ullrich๋ ์๋ฌ ๋ฉ์์ง ํ
์คํธ๋ฅผ CI์์ ํ์ธํ๊ณ ์ฑ
์ ์ฝ๊ฒ ํฌํจํ ์ ์๋๋ก ์ง์ ์ฝ๋๋ฅผ ์์ฑํ ๋, ์ ๊ฐ Lean์ ๋ฉํํ๋ก๊ทธ๋๋ฐ ์์คํ
์ ์ตํ๋ ๋ฐ ํต์ฌ์ ์ธ ๋์์ ์ฃผ์์ต๋๋ค. ์๋ก์ด ๊ฐ์ ํ์ ๊ฒ์ํ ์ง ๋ถ๊ณผ ๋ช ์๊ฐ ๋ง์ ์ด์ ์ ์ธ ๋
์๋ค์ด ์ค๋ฅ๋ฅผ ์ฐพ์๋ด๊ณ , ์ ์์ ๊ฑด๋ค๋ฉฐ, ๋ฐ๋ปํ ๊ฒฉ๋ ค๋ฅผ ๋ณด๋ด์ฃผ์์ต๋๋ค. ํนํ ๋ฌธ์ฒด์ ๊ธฐ์ ์ ์ธ ๋ฉด์์ ๋ง์ ์ ์์ ์ฃผ์ Arien Malec, Asta Halkjรฆr From, Bulhwi Cha, Craig Stuntz, Daniel Fabian, Evgenia Karunus, eyelash, Floris van Doorn, Frantiลกek Silvรกลกi, Henrik Bรถving, Ian Young, Jeremy Salwen, Jireh Loreaux, Kevin Buzzard, Lars Ericson, Liu Yuxi, Mac Malone, Malcolm Langfield, Mario Carneiro, Newell Jensen, Patrick Massot, Paul Chisholm, Pietro Monticone, Tomas Puverle, Yaรซl Dillies, Zhiyuan Bao, ๊ทธ๋ฆฌ๊ณ Zyad Hassan์๊ฒ ๊ฐ์ฌ์ ์ธ์ฌ๋ฅผ ์ ํ๊ณ ์ถ์ต๋๋ค.
Read more โ