ML과 Haskell의 부분 함수, 종료성, 타입 시스템, 부작용 처리 등에 대한 비판적 고찰
오늘 이 글의 제목을 뭐라고 붙여야 할지 잘 모르겠다.
모든 것이 전체 함수이거나, 전체 함수로 표현될 수 있다는 가정이 있다. 더 많은 함수를 전체 함수로 표현할 수 있게 해 준다는 이유로, 의존 타입(dependent typing)에 대한 과장이 뒤따른다.
haskellPrelude> let greet 1 = "hello"
haskellPrelude> greet 1
haskell"hello"
haskellPrelude> greet 2
haskell"*** Exception: <interactive>:2:5-21: Non-exhaustive patterns in function greet
haskellundefined
haskellPrelude> :t greet
greet :: (Eq a, Num a) => a -> [Char]
위에서 우리는 ghci 프롬프트에서 부분 함수를 하나 정의하고, 그 타입이 무엇인지 물어봤다.
돌아온 타입은 a -> [Char]이다. 이 타입은 그 함수가 부분 함수라는 사실을 전혀 말해 주지 않는다.
이걸 곰곰이 생각해 보면, 사실 이 프로그램을 “부분 매핑 + 그 이후의 전체 동작”으로 표현할 수 있다는 것을 알 수 있다.
haskellgreet_partial :: (Eq a, Num a) => a -> Maybe ()
haskellgreet_total :: () -> [Char]
이렇게 하면 입력 공간을 몇 가지 선택지로 좁혀 놓게 된다. 그리고 greet_partial 역시 이제 전체 함수가 된다. 결과에 실패 가능성을 포함시켰기 때문이다. Haskell도 같은 일을 할 수 있었지만, 하지 않는다. 아마도 시스템의 메모리가 부족해졌을 때 메모리 할당조차 실패할 수 있기 때문일 것이다. 이런 식으로 가면, 모든 함수의 결과 타입 뒤에 Maybe를 붙여야 할지도 모른다.
실무에서는, 타입만으로는 모든 제약을 표현할 수 없는 데이터 구조가 아주 많다. 그래서 우리는 항상 이런 식의 타입 불일치(type-disrepancy)를 갖게 된다. 프로그램이 실제로 실행되기 전에 모든 경우를 잡아내자는 기대는 비현실적이다. 많은 경우, 그 결정을 내리기 위한 정보가 컴파일 시점에는 존재하지 않기 때문이다. 그리고 어떤 경우에는, 나중에 데이터가 유실되거나 깨졌다는 사실을 알 수만 있다면, 그렇게 되는 것을 허용해도 괜찮은 상황도 있다.
우리는 실패를 다루는 제대로 된 수단이 필요하지, 모든 것이 전체 함수인 척할 필요는 없다. 이 점에서 Prolog가 더 잘하고 있다고 생각하지만, 그것도 완벽하진 않다. 어쩌면 이런 문제들은 아직 풀리지 않은 것일지도 모른다.
타입은 명제에 대응하고, 프로그램은 증명에 대응한다. 논리에서 명제와 증명은 서로 섞일 수 있는 하나의 언어를 공유한다. Haskell은 이것을 서로 잘 섞이지 않는 세 개의 하위 언어로 쪼개 놓았다.
case 패턴은 패턴 매칭 언어를 이룬다.이렇게 여러 개의 하위 언어를 줄줄이 이어 붙이면 마찰이 생기고, 프로그래밍을 더 쉽거나 더 좋게 만들지 못한다. 공정하게 말하자면, 이런 것들이 즉흥적으로 덧붙인 기능은 아니다. 이들은 단순형 식(lambda) 계산(s simply typed lambda calculus)에서 유도된 것이다.
Haskell은 단순형 람다 계산의 강한 정규화(strong normalization) 성질을 “팔아먹는다”. 그리고 그 대가로 표현력을 산다. 중요하지도 않은 것을 얻기 위해 언어의 온전함을 거래하는 셈이다.
만약 Haskell이 이런 나쁜 거래를 하지 않았다면, 지연(lazy)/엄격(eager) 평가 논쟁은 헛소리에 불과했을 것이다. Haskell이 제대로 설계되었다면, 어떤 평가 전략을 쓰더라도 종료했을 것이다.
여기 절대 종료하지 않는 작은 함수와, 그 함수에 대해 Haskell이 받아들이는 타입 주석이 있다.
haskellf x = if f (x + 1) >= 0 then x else 0
haskellf :: (Num a, Ord a) => a -> a
재귀는 타입 시스템의 건전성(soundness)을 망가뜨린다. 이 함수는 결코 값을 반환하지 못한다. 반환을 하지 않기 때문이다. 그런데도 이 함수는 입력으로 받은 값과 같은 종류의 값을 돌려준다고 주장한다.
이 시점에서, 언어가 가지고 있던 어떤 엄밀성도 사라진다. 무한 데이터 구조와 유한 데이터 구조는 서로 교환 가능하지 않다. 이 둘은 같은 구조가 되어서는 안 된다.
이건 나쁘다. 왜냐하면 이런 종류의 종료성 증명은 실제로 유용할 수 있기 때문이다. 특히, 많은 종료성 증명이 귀납(inductive) 증명과 공동 귀납(coinductive) 증명 두 부류로 나뉠 수 있을 것처럼 보이기 때문이다. 타입에 이 구분을 반영할 수 있다면, 무한 데이터 구조에 의존하는 소프트웨어에서 종료성을 보장하는 데 도움이 될 것이다.
고차 논리(higher-order logic)에서 타입 시스템의 핵심 목적은, 아무 가정 없이도 무엇이든 증명해 버릴 수 있게 만드는 역설(paradox)을 차단하는 것이다. 이는 종료성 증명과 연결되며, 그 때문에 타입 시스템이 유용하다.
전통적으로 타입 시스템은 타입 검사를 컴파일 시점으로 끌어올리거나, 애초에 언어에 타입 개념을 도입하는 데 쓰여 왔다. 하지만 타입의 1차 목적은 최적화나 값의 메모리 레이아웃을 선택하는 데 있지 않다. 타입 시스템의 요점은 Haskell이 실용적인 이유로 창밖으로 내던진(defenestrate) 그 부분들이다. 만약 그 결과로, 우리가 Haskell을 다른 언어들보다 더 높은 기준으로 대해야 한다고 믿지 않게 된다면, 그나마 괜찮을 것이다.
Curry–Howard 대응은 람다 계산이나 범주 이론 쪽을 편들지 않는다. 오히려 직관주의 논리(intuitionistic logic) 편을 든다. 원판(직관주의 논리)이 그대로 괜찮은데, 왜 온갖 곡예적인 관점을 새로 만들어 내야 할까?
Haskell이 부작용(side effect)과 가변 구조(mutable structure)에 관해 갖는 문제들을 부정해서도 안 된다. Haskell은 람다 계산의 증명을 인코딩한 것처럼 생각할 수 있다는 점에서 저수준 언어다. 하지만 그렇다고 해서 충분히 저수준인 것도 아니다.
아마 핵심 관찰은, 우리는 언제나 부분 함수를 가지게 된다는 것이다. 타입 시스템은 그것을 지워 버리려고 해서는 안 된다. 좋은 타입 시스템은, 우리가 원치 않는 상황을 막아 줄 것이다. 이런 관점에서 본다면, C 언어에서 잘못된 힙 관리 가능성을 제거해, 사용할 만한 타입이 붙은 저수준 언어를 얻을 수도 있을 것이다.
블로그 작성자: Henri Tuhola. 핀란드 출신의 독학 프로그래머이자 전자공학 애호가.
나는 프로그래밍, 프로그램 설계, 프로그래밍 언어 설계, 알고리즘, Steam OS, 게임 프로그래밍, Vulkan, 가상 현실, WebGL, DIY 전자공학, 인터넷, 정원 가꾸기, 피트니스를 즐긴다. 이 블로그는 내 모든 관심사의 단면을 보여 준다. (대부분은 프로그래밍 언어 연구와, 가끔 올라오는 프로그래밍 가이드들이다.)
나는 Lever 프로그래밍 언어의 작성자이기도 하다. 내가 만든 언어이지만, 그 후에 “동적 타입이 아닌 더 나은 언어를 만들 수 있겠다”는 생각을 하게 되었다.
보통 일주일에 한 번이나 두 주에 한 번 정도 블로그를 업데이트한다. 이메일이나 트위터로 피드백을 보낼 수 있다. 글에 대한 수정과 개선 제안을 환영한다.