타입 시스템의 기초와 프로그래밍 언어 분류 정리

타입 시스템은 계산하는 값의 종류에 따라 프로그램 구문을 분류하여 특정 오류 동작이 없는지 자동으로 검사하는 구문 방식입니다.

-Benjamin.C.Pierce,Types and Programming Languages(2002)

들어가기 앞서

항상 프로그래밍 언어를 이야기하다보면 사람들이 '정적타이핑(Static Typing)' '동적 타이핑(Dynamic Typing)'을 언급하며 이야기하는 것을 볼 수 있다.

보통 타이핑(Typing)은 개발자들이 언어를 선택할 때 자주 고민하는 주제이다.

우선 간단하게 정적 타이핑 과 동적 타이핑이 무엇인지 이야기를 해보자

들어가기 앞서 알아두면 좋을 기초지식

값(Value)과 타입(Type)

• 값은 프로그램이 계산하는 구체적인 데이터 (32, "hello", true)

• 타입은 그 값들의 집합에 붙이는 이름이자 허용 연산의 명세 (int, string, bool)

• 타입이 없으면 32 + "hello" 같은 연산이 의미 있는지 판단할 기준이 없다

컴파일(Compile)과 런타임(Runtime)

• 소스코드 → 컴파일러 → 기계어/바이트코드 → 실행

• 컴파일 타임: 실행 전, 코드를 번역하는 단계. 이 시점에 검사 가능한 것은 구조적 규칙이다

• 런타임: 실제로 프로그램이 실행되는 단계. 값이 메모리에 올라와 있다

• 타입 검사를 어느 단계에서 하느냐가 정적/동적의 핵심 분기점이다

인터프리터(Interpreter) 언어와의 관계

• 컴파일 단계 없이 소스를 직접 실행하는 언어(Python, Ruby)는 컴파일 타임 자체가 없거나 매우 짧다

• 그래서 동적 타이핑과 인터프리터 언어가 자주 함께 나오지만, 이 둘은 독립적인 개념이다

• TypeScript는 정적 타이핑이지만 최종 실행은 JavaScript 인터프리터가 한다

(동적 타이핑과 정적 타이핑 Kolja Wilcke https://x.com/01k 의 그림)

타이핑의 기본 개념 정리

타이핑(Typing System)은 변수,함수, 데이터의 타입을 어떻게 관리하는지를 정의하는 규칙이다.

타입 시스템의 주요 목적은 다음과 같다

-오류 방지:잘못된 타입의 데이터 사용을 미리 방지

-코드 안정성:프로그램의 동작을 더 예측 가능하게 함

-최적화 가능:타입 정보를 활용해 컴파일러가 최적화 가능

특히 정적 타이핑 (Static Typing)과 동적 타이핑(Dynamic Typing)의 차이는 타입을 언제 검사하느냐에 따라 구분된다.

정적 타이핑(Static Typing)

-컴파일(Compile-Time)에 타입을 검사하는 방식

-변수나 함수의 타입이 미리 선언되며, 컴파일 시점에서 타입 오류를 잡을 수 있다.

- 대표적 언어 : C,C++,Java,C#,TypeScript,Kotlin

int age = "32"; // 컴파일 오류가 발생. 문자열을 정수형 변수에 할당할 수 없음

장점으로는 타입오류를 미리 방지하여 안정성이 높다

단점으로는 코드 작성시 타입을 미리 선언해야하기에 초기 개발속도가 느릴 수 있다.

동적 타이핑(Dynamic Typing)

-런타임(RunTime)에 타입을 검사하는 방식

-변수의 타입을 미리 선언할 필요 없이, 실행중에 타입이 결정됨.

-대표적 언어:Python,JavaScript,Ruby,PHP

age = 32 #정수형
age = "Thirty-two" # 문자열로 변경 (가능)

장점으로는 유연한 코딩 가능, 개발 속도가 빠름

단점으로는 타입 오류가 실행중에 발생할 수 있어 디버깅이 어려울 수 있다.

한 줄로 요약하자면, 정적 타이핑은 특정 종류의 오류가 없음을 증명하는 것이고, 동적 타이핑은 그 오류를 런타임에 감지하는 것이다.

그렇다면 시작은 어떨까?

우선, 우리는 람다 계산(λ-calculus)부터 알아야한다.

들어가기전에 알아두면 좋을 지식

• 변수(Variable): $x$- 값을 담는 자리 (Parameter)

• 추상화(Abstraction): $λx.M$ - 함수 정의 (Function Definition / Lambda Expression)

• 적용(Application): $MN$ - 함수 호출 (Function Call)

기본 정수론 문제 중에는, nnn개의 양의 정수에 대해 효과적으로 계산 가능한 함수 fff를 찾는 형태로 정리할 수 있는 문제가 있다.

여기서 f(x1,x2,...,xn)=2f(x_1, x_2, ..., x_n) = 2f(x1​,x2​,...,xn​)=2가 되기 위한 필요충분조건이 특정 정수론 명제의 참 여부를 결정하는 경우를 의미한다.

-알론조 처치 An Unsolvable Problem of Elementary Number Theory(1936)

람다 계산(λ-calculus)

람다 계산(λ-calculus)은 프로그래밍의 시작점에 선 논문들 중 하나이다. 

논문에서 알론조 처치는 새로운 형식 체계인 람다 계산법을 처음으로 공식적으로 제시했다. 

여기서 처치는 람다 계산법을 이용하여 계산 가능성(Computability) 라는 직관적인 개념을 수학적으로 엄밀하게 정의했고,

이것이 튜링 기계(Turing Machine)과 함께 계산 가능성을 정의하는 강력하고 영향력 있는 형식 체계 중 하나로 인정 받고 있다.

이 논문에서 핵심 결과는 당대 수학계의 어려운 문제였던 결정 문제(Entscheidungsproblem)이 해결 불가능하다는 것을 보여준다.

이 논문은 함수형 프로그래밍에 근간 익명함수(Anonymous Function),고차 함수(Higher-Order Function), 함수 적용(Function Application)과 같은 개념을 내포하고 있다.

람다 계산법은 아주 어렵지만, 많은 수학자들과 컴퓨터 과학 책을 저술한 저자들의 말을 요약하자면 이렇다

-함수를 가장 기본적인 연산으로 간주한다.

-변수,추상화,적용이라는 3가지 규칙만으로 튜링 완전(Turing-Complete)을 표현한다.

하지만 여기서 람다 계산법은 타입 개념이 없었고, 무타입 람다 계산은 후대 프로그래밍 언어 이론, 특히 함수형 언어와 계산 모델의 기초 중 하나가 되며,

'무엇이든' 입력 받을 수 있는 동적 모델이었다.

즉 람다 계산법의 초기 형태는 타입이 없었기에 유연했고,

이후 이 논문은 동적 타이핑(Dynamic Typing)의 이론적 배경 중 하나로써 작용하게 된다.

*튜링 완전성(Turing Completeness): 튜링 완전성을 가진 체계는 튜링 기계로 풀 수 있는 모든 계산문제를 풀 수 있다는 뜻.

**튜링 기계(Turing Machine): 앨런 튜링이 고안한 추상적인 기계로 컴퓨터도 이 구조를 따른다.람다 계산(λ-calculus)

A FORMULATION OF THE SIMPLE THEORY OF TYPES

(1940, Alonzo Church)

이후 4년 후 알론조 처치는 람다 계산에 '타입(Type)'을 추가하는 시스템을 제안한다.

이를 통해 각 변수와 함수의 입력/출력 타입을 정하는 '타입 시스템' 개념이 처음 등장했고,

이 연구가 훗날 정적 타이핑(Static Typing)형식의 뼈대가 된다.

자, 이제 우리는 정적 타이핑과 동적 타이핑의 역사적 시작을 보았다.

이제 람다 계산식이 무엇인지 보자

다만 그전에 앞서 조금 쉽게 중학교 수학을 이용해 이해를 해보자

중학교 수학을 이용한 람다식 이해

f(x) = x + 2 (이름이 있는 함수)

이것을 람다 표현식으로 바꿔보자

λx. x + 2 (이름이 없는 '익명' 함수)

λx. x + 2는 “x를 입력으로 받아 2를 더하는 함수”를 뜻한다.

f(3) = 3 + 2 = 5
(λx. x + 2) 3 = 3 + 2 = 5   -- 적용 결과는 같다

학교에서 배우던 수학에서는 함수에 반드시 f나 g같은 이름을 붙여야 하지만, 람다 계산에서는 함수 자체가 값(Value)이기 때문에 이름 없이도 연산에 참여할 수 있다.

우리가 중학교때 처음 배우던 x,y 처럼 값을 넣는 개념으로 이해해보자

공통점

x, y 같은 수학 변수도 입력을 받는 역할을 함. λx. x + 2의 x도 입력을 받는 변수처럼 동작함. 즉, 어떤 값이 주어졌을 때, 그 값이 대입되어 함수가 계산됨.

차이점

x, y는 단순한 변수지만, 람다(λ)는 "함수를 정의하는 역할"도 수행함.

λx. x + 2 자체가 하나의 "익명 함수(Anonymous Function)"로 동작할 수 있음.

눈썰미 좋은 독자들은 알겠지만 람다(λ)는 x를 입력 변수로 선언하는 표현 일뿐이며, λx는 "지금부터 $x$를 입력으로 쓸게" 라는 표현이다.

조금 더 구체적으로 설명하자면 λ는 '익명 함수(Anonymous Function)'을 표현하는 기호이며,

람다 표현식은 단순히 어떠한 값을 입력으로 받아 특정 연산을 수행한 후, 결과를 반환하는 함수이다!

(기초적인 람다 계산을 도와주는 플레이 그라운드 예제)

자, 이제 어느정도 기초를 이해했으니, 이제 실제 람다 계산을 해보자

타입이 없는 람다 계산(Untyped-λ-Calculus)

λx. x (정체 함수, identity function)
λx. λy. x + y (두 값을 더하는 함수)->타입이 없기 때문에 어떤 값도 전달 가능하지만 타입 오류를 잡을 수 없다!

여기서 x + y는 이해를 돕기 위한 의사 표기(pseudonotation)다.

순수 람다 계산에는 숫자도, 덧셈 연산자도 존재하지 않는다.

실제로는 숫자 2조차 λf. λx. f (f x) 형태의 함수로 표현하며, 이를 Church Encoding이라 부른다.

실제 논문을 찾아볼 독자는 이 점을 염두에 두자.

타입이 없기 때문에 어떤 값이든 전달할 수 있지만, 그만큼 타입 오류를 사전에 잡을 수 없다.

타입이 있는 람다 계산(typed-λ-Calculus)

λx: Int. x + 1 // 정수형을 입력받아 1을 더하는 함수
λx: Bool. if x then 1 else 0 // 불리언 값을 받아 정수로 변환

->변수에 타입을 명시함으로써, 잘못된 타입의 값이 들어오면 계산 전에 오류를 감지할 수 있다!

의사 표기가 아닌 실제 표기

-- 의사 표기 (pseudonotation)
λx: Int. x + 1

-- 실제 표기 1: 기본 연산을 함수로 선언한 STLC 방식
λx: Nat. succ x
-- succ : Nat → Nat  (후계 함수, successor function)
-- succ x 는 x + 1 에 해당한다
-- 순수 람다 계산에는 + 연산자가 없으므로, succ 을 원시 함수로 선언해 사용한다

-- 실제 표기 2: Church Encoding 방식 (가장 순수한 형태)
λf: Nat → Nat. λx: Nat. f x
-- 숫자 1은 λf. λx. f x 로 표현한다
-- succ 조차 없애고 함수 적용 횟수로 숫자를 표현한다

-- 의사 표기 (pseudonotation)
λx: Bool. if x then 1 else 0

-- 실제 표기: Church Boolean 방식
true  = λt: T. λf: T. t   -- true는 두 입력 중 첫 번째를 반환하는 함수
false = λt: T. λf: T. f   -- false는 두 입력 중 두 번째를 반환하는 함수

λx: (T → T → T). x (λf: Nat → Nat. λn: Nat. f n) (λn: Nat. n)
-- x가 true이면 succ 에 해당하는 함수, false이면 항등 함수를 반환한다

-Lisp는 하루만에 배울 수 있습니다. 하지만 당신이 포트란을 알고 있다면 3일이 걸릴겁니다.-Marvin Minsky

그리고 이 개념들은 어셈블리어에서 진화한 최초의 고급 언어들에서 구현 되는데, 그것이 바로 FORTRAN과 Lisp이다.

1) 포트란(FORTRAN) -정적타이핑의 시작

1957년 과학계산을 위해 발명된 최초의 고수준(High-Level) 언어

특징

-정적 타입 시스템을 채택

-컴파일 시점에 타입검사를 수행

2)Lisp -동적 타이핑의 시작

1958년: 존 매카시(John McCarthy)가 개발한 함수형 프로그래밍 언어

특징

-동적 타입 시스템을 채택

-런타임에 타입 검사를 수행

언어의 역사를 이해하면 끝이 없기때문에 단순 요약하면,

정적 타이핑은 포트란에서 컴파일 시 타입 검사하는 방식으로 구현됐고,

동적 타이핑은 런타임에서 타입을 동적으로 결정하고, 실행도중 타입을 변경하는 식으로 구현이 됐다.

물론 사족을 달자면 포트란에서 도입된 타입 시스템은 엄격한 타입 시스템이 아니고,

엄격한 정적 타이핑은 ALGOL 계열에서 나타나고, 또한 타입 시스템 자체도 수십년간 끝없는 발전이 있었지만,

기본적으로 정적 타이핑과 동적 타이핑의 큰 틀은 유지 됐다.

그리고 이후에 이 정적 타이핑과 동적 타이핑을 나누고,

또 나누는데, 분류 방식들에 대해서 보자

(Washinton CSE583)

타입추론으로의 분류

public class TypeInferenceExample1
{
    public static void main(String[] args)
    {
        // 명시적 타입 선언 (기존 방식)
        int number = 10;
        double pi = 3.14;
        String message = "Hello, Type Inference!";

        // 타입 추론 (var 키워드 사용)
        var inferredNumber = 20; // int 로 추론
        var inferredPi = 3.14159; // double 로 추론
        var inferredMessage = "Welcome to Java!"; // String 으로 추론

        System.out.println("Number: " + number + ", Inferred Number: " + inferredNumber);
        System.out.println("Pi: " + pi + ", Inferred Pi: " + inferredPi);
        System.out.println("Message: " + message + ", Inferred Message: " + inferredMessage);
    }
}

(예시는 자바의 타입 추론 예시인 var 키워드)

타입 추론(Type Inference)

타입 추론이란 프로그래머가 명시적으로 타입을 선언하지 않아도, 컴파일러(또는 인터프리터)가 문맥(Context) 또는 코드 구조를 분석하여 변수, 함수, 표현식의 타입을 자동으로 추론하는 기능을 말한다.

Types and Programming Languages에서는 타입 재구성(Type Reconstruction)이라는 파트로 나오며, 타입 추론(Type Inference)이라는 단어와 혼용된다고 한다. 두 용어의 차이는 다음과 같다.

타입 추론(Type Inference): 컴파일러가 문맥만으로 타입을 완전히 결정할 수 있는 경우

타입 재구성(Type Reconstruction): 일부 타입 정보가 주어진 상태에서 나머지를 추론해야 하는 경우

다만 학계에서는 이 둘을 대부분 동의어로 혼용하며, TAPL도 이 점을 명시하고 있다.

타입 선언 방식에 따라 언어는 다시 두 가지로 나뉜다.

명시적 타입 시스템(Explicit Typing): 개발자가 타입을 직접 선언해야 한다. 코드 가독성이 좋지만 장황해질 수 있다.

암시적 타입 시스템(Implicit Typing): 컴파일러가 타입을 자동으로 추론한다. 코드가 간결해지지만 추론 오류 발생 시 디버깅이 어렵다.

그리고 이걸 더 깊게 이해하기 위해선 Hindley-Milner 타입 시스템에 대해서도 설명해보자.

(힌들리 미너 타입 시스템을 표현하는 규칙)

위의 식은 힌들리 미너 타입 시스템의 선언적 타입 시스템을 나타내고, 타입 판별 및 타입 유추 규칙을 나타낸 것이다.

힌들리 미너 시스템은 강력한 타입추론을 제공하는 것이라고 이해할 수 있다.

(제약 기반 타입 시스템 Constraint- Based Typing)

제약 기반 타입 시스템은 타입 추론 과정에서 제약을 수집한 후, 일괄적으로 제약(Constraint)를 모아서 해결하는 방식이다.

즉 필요한 모든 관계(제약 조건)을 수집하고, 해결하여 최종 타입을 결정한다.

함수 적용시 타입을 바로 맞추는 것이 아니라 먼저 타입 제약(Constraint)를 모아서 나중에 해결(Unification) 하는 것이다.

그리고 이후에 타입들에 대해서 개발자가 직접 코드에서 선언(Explicit), 컴파일러/인터프리터가 자동으로 유추(Implicit)에 따라, 언어는 나뉜다.

강타입 / 약타입 (Strong Typing / Weak Typing)

정적/동적이 "타입 검사를 언제 하느냐"의 문제라면, 강/약 타입은 "타입 변환을 얼마나 엄격하게 통제하느냐"의 문제다. 이 두 축은 서로 독립적이다.

강타입(Strong Typing): 암묵적 타입 변환(Implicit Casting)이 엄격하게 제한된다. 타입이 맞지 않으면 오류를 발생시킨다.

약타입(Weak Typing): 타입 변환이 자유로우며, 런타임에서 예기치 않은 동작이 발생할 수 있다.

언어별 타입 시스템 분류

분류 기준은 커뮤니티 내 통용되는 관점을 따른 것이며, 언어 버전과 맥락에 따라 달라질 수 있다는 점 명시할 것!

프로그래밍에 대한 사고방식에 영향을 미치지 않는 언어는 배울 가치가 없다. -Alan J.Perlis

마치며...

프로그래밍 언어의 타입 시스템은 단순히 기술적 도구가 아닌, 사상과 철학의 결정체이다.

알론조 처치의 람다 계산법에서 시작해 포트란과 Lisp의 대립을 거치며,

정적 타이핑은 안정성을, 동적 타이핑은 유연성을 추구하는 두 축이 형성되었고,

이 두 흐름은 수십 년간 서로 경쟁하고 융합하며 현대 언어의 토대를 이루었고, 또 점진적 타이핑이라는 새로운 융합 기조와 철학으로 나아갔다.

우리는 언어를 선택하기 앞서, 사실 자기가 진출하고자 하는 산업계에 주로 쓰이는 라이브러리와 프레임 워크 기준으로 언어를 선택한다.

하지만 타입 시스템을 이해한다면, 그 언어의 설계 의도를 바탕으로 파생된 라이브러리와 프레임 워크를 더 깊게 이해할 수 있고,

문제에 맞는 도구(프로그래밍 언어)를 선택할 수 있는 지혜를 얻게 될 것이다.