프로그래밍 언어의 타입 시스템에 별칭 추론을 맡기지 마세요

AI 요약

Futhark는 배열 전체를 복사하지 않고 원소 하나를 바꾸는 갱신을 지원합니다. A with [i] = v는 의미상 새 배열을 만들지만, 실제 비용은 배열 크기와 무관하게 원소 하나에 비례해야 합니다. 이를 보장하려면 기존 배열 A를 메모리에서 직접 갱신해야 하므로, 갱신 뒤에는 이전 A를 다시 읽지 못하게 해야 합니다. Futhark는 이를 값의 소비(consumption)로 표현하고, 같은 메모리를 가리킬 가능성이 있는 변수까지 별칭(alias)으로 추적합니다.

소비와 별칭 추적

예를 들어 let B = A라면 A와 B는 별칭입니다. 한쪽을 소비하면 다른 쪽도 더는 사용하지 못해야 합니다. 조건식의 결과처럼 실행 시점에 어느 값이 선택될지 모르는 경우에는 가능한 별칭을 모두 추적합니다. if ... then A else B의 결과는 A와 B 모두의 별칭으로 취급합니다. 실제 실행에서 둘 중 하나만 선택되더라도, 타입 검사가 소비된 값을 다시 읽는 코드를 허용하면 안전하지 않기 때문입니다.

Futhark는 소비 효과를 함수 매개변수 타입에 표시합니다. *a -> b는 인자 a를 소비하고, a -> b는 인자를 관찰만 합니다. 반환 타입의 별표는 다른 뜻으로, 결과가 새 값인지 나타냅니다. a -> *b는 새 결과를 반환하고, a -> b는 결과가 인자와 별칭일 수 있음을 뜻합니다. 매개변수와 반환 타입에 같은 별표를 쓰지만 의미는 다릅니다. 저자는 이를 고유성 타입(uniqueness types)이나 아핀 타입(affine types)과 동일시하지 않고, 특정 순서의 효과를 금지하면서 별칭을 전파하는 체계로 설명합니다.

함수와 추상 타입에서 생기는 문제

함수 결과가 전역 변수와 별칭이 될 수 있다면, 호출 지점의 함수 타입만으로 그 별칭을 알아낼 수 없습니다. 그래서 최상위 함수는 인자 외의 값, 특히 전역 변수나 클로저에 든 값과 별칭인 결과를 반환하지 못하게 합니다. 튜플을 새 결과로 반환한다고 선언할 때는 구성 요소끼리도 서로 별칭이 아니어야 합니다. 같은 배열을 튜플의 두 칸에 넣는 함수는 이 조건을 만족하지 못합니다.

고차 함수에서는 함수 자체의 클로저가 결과와 별칭이 될 수 있습니다. 예를 들어 함수 인자 p를 두 번 호출해 배열을 얻는다면, 두 결과가 p가 캡처한 같은 배열을 가리킬 수 있습니다. 이를 놓치지 않도록 지역 함수와 람다는 범위 안의 변수를 캡처할 수 있게 두되, 함수 호출 결과가 함수 값 자체와도 별칭이 될 수 있게 추적합니다. 최상위 함수는 클로저 별칭을 허용하지 않는 규칙을 유지합니다.

추상 타입은 내부 표현이 숨겨져 있어 별칭 추적이 특히 어렵습니다. 모듈 인터페이스의 타입 obj가 실제로는 서로 별칭인 두 배열의 튜플일 수 있습니다. 소비 함수가 튜플의 한 배열만 갱신하면 다른 배열까지 바뀔 수 있지만, 추상 타입을 쓰는 쪽에서는 그 관계를 알 수 없습니다. 이를 해결하려고 저자는 별칭 집합에 이름뿐 아니라 ‘자기 별칭 가능성’을 나타내는 self 항목을 넣는 방안을 제시합니다. 자기 별칭이 포함된 값은 소비하지 못하게 하고, 추상 타입의 비신선(nonfresh) 결과에는 이 항목을 추가합니다. 그러면 문제가 되는 소비가 호출 지점에서 거부됩니다.

매개변수성으로 별칭을 더 정밀하게 추론

id : a -> a 같은 다형 함수는 타입 매개변수 a의 내부를 알 수 없으므로, 입력을 그대로 반환하는 것 말고는 결과를 만들기 어렵습니다. 따라서 결과 별칭은 입력 별칭과 같다고 추론할 수 있습니다. 저자는 이처럼 매개변수성(parametricity), 즉 다형 함수가 타입 인자를 들여다볼 수 없다는 성질을 이용해 별칭 정보를 추론하려 합니다. apply 같은 고차 함수도 결과가 함수 인자나 적용 대상에서 왔다는 정보를 활용할 수 있습니다. 다만 두 호출 결과를 튜플로 반환하는 apply2처럼, 매개변수성만으로 결과끼리 별칭이 없다고 단정할 수 없는 경우도 있습니다.

1.0 전 설계 방향

작성자는 안전성 문제를 해결하되 타입 언어나 모듈 언어는 확장하지 않고, *를 신선한 결과 표시로 유지하는 쪽에 기울어 있습니다. 그 선택을 따르면 표준 라이브러리의 많은 함수 반환 타입에 별표를 더해야 합니다. 다형 함수에는 매개변수성을 이용해 별칭 정보를 더 정밀하게 추론하는 방안을 검토합니다. 타입 검사기의 간단한 버그를 고치는 일에서 시작했지만, 그 수정이 기존의 제네릭 코드에 영향을 주면서 인터페이스 표현과 사용 편의성까지 다시 검토하게 됐다고 설명합니다. 글은 1.0 출시 전에 안전성 문제를 정리하되, 이런 요구가 없다면 다른 언어 설계자에게 별칭 추론을 타입 시스템에 넣는 싸움을 권하지 않는다는 경고로 끝납니다. Futhark는 메모리 할당이 없어야 하는 성능 요구 때문에 이 기능을 필요로 하며, 보통은 참조 횟수가 1일 때만 메모리를 재사용하는 방식이 더 적절할 수 있다고 덧붙입니다.

Reddit 반응

• @u/initial-algebra — 교집합 타입(intersection types)이나 제한 양화(bounded quantification)를 쓰면 타입 시스템 확장을 비교적 작게 유지하면서 표현력을 높일 수 있다고 봅니다. apply2에 더 정밀한 타입을 줄 수 있고, 신선성 표기 *a도 제한 양화로 나타낼 수 있다는 제안입니다. 다만 어느 방식이든 프로그래머가 그 정보를 명시해야 할 수 있습니다.
  • @u/TreborHuang — 최상위 타입과 하위 타입 없이 교집합 타입만 단순 타입 람다 계산에 더해도 강한 정규화(strong normalization)가 가능한 항을 전부 타입화할 만큼 표현력이 큽니다. 제한 없이 쓰면 지나치게 강력하다고 여길 수도 있습니다. 교집합 타입은 람다 계산의 필터 모델(filter models)이라는 의미론적 체계와도 동등합니다.
  • @u/Athas — 제안된 apply2 타입으로는 두 번째 결과의 타입 c를 어디서 얻는지 모르겠다고 질문합니다. 두 함수를 인자로 받는 형태라면 매개변수성으로 더 정밀한 별칭을 추론할 수 있지만, 프로그래머가 그 차이를 명시해야 한다고 설명합니다. 글에서 다루지 않은 별칭 정보의 내부 표현도 고민 중이며, 소스 코드에는 드러내지 않더라도 함수 안에서 지역적으로 추론되는, 구문 기반 타입 체계를 원한다고 덧붙입니다.
• @u/_supercuco — 소비는 바인더나 매개변수의 성질이고 신선성은 타입의 성질인데, 두 개념을 현재처럼 결합하면 문제가 생긴다고 주장합니다. 반환 타입에 *를 붙여 신선성을 표현하려면, 호출자가 어떤 인자를 넘겼는지와 무관하게 그 결과가 신선하다는 보장이 필요하다는 지적입니다. 완전한 선형성(linearity)을 도입하거나 반환 타입의 신선성 표기를 없애야 한다는 선택지를 제시합니다.
  • @u/Athas — 매개변수의 *와 반환 타입의 *는 표기만 같을 뿐 서로 다른 개념이며, 함수 화살표의 효과를 제어한다고 답합니다. 신선성 반환 타입 자체보다, 신선성 표시가 없는 반환 결과의 별칭을 추론하는 과정에서 문제가 생긴다고 설명합니다.
  • @u/_supercuco — M1 예제가 타입 검사를 통과하는 것은 잘못이라고 재차 주장합니다. 결과 타입에 신선성을 표시한다면 그 결과가 신선하다는 데 필요한 가정도 타입에 드러나야 하며, 런타임 가정으로 타입을 정교하게 만들 수는 없다는 의견입니다.
  • @u/Athas — mk는 신선한 결과를 선언하지 않았으므로 해당 결과를 신선하다고 추론하는 문제가 아니라고 설명합니다. 제안한 self 별칭 규칙을 적용하면 M1.mk 호출 결과를 소비하는 표현식이 거부됩니다. 선형 타입 언어로 바꾸지 않고도 안전성을 보장하는 방안을 찾고 있다고 덧붙입니다.
• @u/brucejbell — 자신의 언어도 기본적으로 값 중심이며, 변경 가능한 자원은 이전 값의 수명을 끝내는 방식으로 다룬다고 소개합니다. 자원 전달에는 빌림(borrow)과 소유권 이전 모드를 두고, 별칭을 보수적으로 추적합니다. 새 결과나 인자에 의존하지 않는 결과를 표시하는 문법과 copy 연산도 두었으며, 복사가 별칭 전파를 막는 간단한 방법이라고 설명합니다.
• @u/Additional-Cup3635 — 함수 타입이 함수의 사용 조건을 완전히 설명해야 한다는 원칙이 이 문제의 큰 난점이라고 봅니다. 구현을 일정 깊이까지 인라인하거나 다형 함수는 단형화 뒤에 검사해 신선성을 확인하는 방법을 제안합니다. 타입 언어를 복잡하게 만들지 않고도 구현을 보고 검사할 수 있다는 주장입니다.
  • @u/proudHaskeller — 그러면 컴파일 결과가 예측하기 어려워지고, 개발자가 코드가 갑자기 깨지는 일을 피하려고 불필요한 복사를 방어적으로 넣게 될 수 있다고 반박합니다.
• @u/proudHaskeller — mk와 consume을 다형성이나 모듈 없이 단형 함수로 작성해도 같은 문제가 생길 것 같은데, 왜 단형 코드에서는 문제가 막히는지 질문합니다.

원문: Futhark 블로그 / 번역·요약: Trawling