정적 및 동적 타이핑

정적 타이핑은 프로그램 실행 전에 타입을 검사하는 반면, 동적 타이핑은 실행 중에 타입을 검사합니다. 점진적 타이핑은 이 둘을 하나의 언어 내에서 결합하고자 합니다.

Definition

정적 타이핑은 컴파일 시점에 타입 제약 조건을 검증하여 잘 정의된 타입의 프로그램이 실행 전에 수용되도록 합니다. 동적 타이핑은 타입 검사를 런타임으로 연기하며, 부적절한 타입의 값에 연산이 적용될 때 오류를 발생시킵니다.

Scope

이 주제는 타입 검사가 언제, 어떻게 발생하는지에 대한 스펙트럼을 다룹니다. 즉, 컴파일 시점에 잘못된 타입의 프로그램을 거부하는 정적 검사, 런타임에 타입 오류를 감지하는 동적 검사, 그리고 이 둘이 공존할 수 있도록 하는 점진적 또는 선택적 타이핑을 포함합니다. 각 방식의 보장, 유연성, 성능 영향과 함께 타입 검사 규율의 건전성(soundness)에 대해서도 다룹니다.

Core questions

• 정적 검사가 미리 방지할 수 있지만 동적 검사가 방지할 수 없는 오류 유형은 무엇입니까?
• 동적 타이핑은 어떤 유연성을 제공하며, 그 대가는 무엇입니까?
• 점진적 타이핑은 타입이 지정된 코드와 타입이 지정되지 않은 코드를 어떻게 건전하게 혼합할 수 있습니까?
• 정적 타입 규율의 건전성은 어떻게 확립됩니까?

Key theories

점진적 타이핑

Siek과 Taha는 프로그램의 일부는 정적으로 타입이 지정되고 다른 일부는 동적으로 타입이 지정될 수 있도록 허용하는 타입 시스템을 정의했으며, 경계에서의 안전한 상호작용을 규율하는 일관성 관계를 포함합니다.

정적 타입 건전성

Wright와 Felleisen의 진행-보존(progress-and-preservation) 방법은 건전한 정적 타입 시스템이 잘 정의된 타입의 프로그램이 '멈춘 상태(stuck states)'에 도달하지 않음을 보장한다는 것을 보여주며, 정적 검사의 안전성을 형식화합니다.

Clinical relevance

정적 타이핑과 동적 타이핑의 선택은 개발자 워크플로우, 도구, 신뢰성에 영향을 미칩니다. 동적 언어 위에 계층화된 것과 같은 점진적 및 선택적 타이핑 시스템은 팀이 기존의 대규모 코드베이스에 정적 보장을 점진적으로 추가할 수 있도록 합니다.

History

초기 언어들은 정적 타이핑(Algol, Pascal, ML)과 동적 타이핑(Lisp, Smalltalk) 계보로 나뉘었습니다. 생산성 측면에서 동적 언어가 인기를 얻으면서 연구자들은 이 두 접근 방식을 조화시키려 노력했습니다. Siek과 Taha의 2006년 점진적 타이핑(gradual typing)과 동시대의 선택적 타입(optional types)에 대한 연구는 동적 언어 위에 구축된 널리 사용되는 점진적 타입 시스템으로 이어졌습니다.

Debates

점진적 타이핑의 비용과 건전성

연구자들은 건전한 점진적 타이핑이 타입이 지정된/지정되지 않은 경계에서 엄청난 런타임 검사 비용을 피할 수 있는지, 그리고 건전하지 않은 '선택적' 타이핑이 더 나은 실용적인 절충안인지에 대해 논쟁합니다.

Key figures

• Benjamin Pierce
• Jeremy Siek
• Walid Taha
• Matthias Felleisen

Seminal works

• pierce2002
• siek2006
• wright1994

Frequently asked questions

정적 타이핑이 항상 동적 타이핑보다 낫습니까?

어느 한쪽이 보편적으로 더 낫다고 할 수는 없습니다. 정적 타이핑은 더 많은 오류를 조기에 잡아내고 도구 사용을 돕는 반면, 동적 타이핑은 유연성과 빠른 프로토타이핑을 제공하므로, 올바른 선택은 프로젝트의 신뢰성과 민첩성 요구 사항에 따라 달라집니다.

점진적 타이핑이란 무엇입니까?

점진적 타이핑은 단일 프로그램이 정적으로 타입이 지정된 부분과 동적으로 타입이 지정된 부분을 혼합할 수 있도록 하며, 경계에 런타임 검사를 삽입하여 타입이 지정된 코드는 보장을 유지하고 타입이 지정되지 않은 코드는 유연성을 유지하도록 합니다.