# 타입 시스템 표기법은 어떻게 읽어야 하는가?

> Clean Markdown view of GeekNews topic #10385. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=10385](https://news.hada.io/topic?id=10385)
- GeekNews Markdown: [https://news.hada.io/topic/10385.md](https://news.hada.io/topic/10385.md)
- Type: GN+
- Author: [neo](https://news.hada.io/@neo)
- Published: 2023-08-17T10:06:20+09:00
- Updated: 2023-08-17T10:06:20+09:00
- Original source: [langdev.stackexchange.com](https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation)
- Points: 1
- Comments: 1

## Topic Body

- 이 기사는 프로그래밍 언어에서 타입 시스템 표기법을 읽고 이해하는 방법에 대한 상세한 설명입니다.
- 타입 시스템 표기법은 타입 시스템에 관한 기사나 논문에서 사용되는 수학적 표현입니다.
- 타입 시스템을 설명하는 데 사용되는 표기법은 발표에 따라 다르지만, 대부분의 발표는 많은 공통 부분을 공유합니다.
- 프로그래밍 언어에 적용된 타입 시스템은 구문 시스템으로, 프로그래밍 언어의 구문에 작용하는 규칙 집합입니다.
- 이 표기법은 공식 논리에서 기원하며, 시스템의 속성에 대한 공식 증명을 구성하는 데 사용됩니다.
- 이 기사는 또한 타입 시스템 표기법에서의 관계, 판단, 공리, 추론 규칙 개념에 대해 논의합니다.
- 타이핑 관계는 일반적으로 e:τ로 쓰여지며 "e는 타입 τ를 가지고 있다"로 읽을 수 있습니다.
- 타이핑 판단은 ⊢e:τ⊢ 표기법을 사용하여 작성되며, 여기서 ⊢는 "다음 문장이 참이다"를 의미하는 것으로 읽을 수 있습니다.
- 이 기사는 또한 타입 시스템 표기법에서의 변수, 컨텍스트, 환경 개념에 대해 자세히 설명합니다.
- 컨텍스트 또는 타입 환경은 표기법에서 Γ로 표현됩니다.
- 이 기사는 또한 추론 규칙 레이아웃, 사이드 조건, 서브타이핑, 다중 컨텍스트, 양방향 타입 체크와 같은 다른 일반적인 표기법과 고려 사항을 다룹니다.
- 이 기사는 타입 시스템 표기법을 이해하는 데 대한 종합적인 가이드로, 특히 이 개념에 새로운 사람들을 위한 것입니다.

## Comments



### Comment 18321

- Author: neo
- Created: 2023-08-17T10:06:20+09:00
- Points: 1

###### [Hacker News 의견](https://news.ycombinator.com/item?id=37138807) 
- 컴퓨터 과학 논문에서의 타입 시스템 표기법에 대한 논의, BNF 표기법, 추론 규칙 등에 대한 기초 설명
- 표기법의 기원은 Frege로 추적되며, 회전문 심볼과 수평선이 핵심 요소
- 컴퓨터 과학 전공자임에도 불구하고, 일부 독자들은 |-와 |=, 그리고 사용된 변수의 메타-구문 수준의 의미를 혼란스럽게 느낌
- 설명은 감사하지만, 일부 독자들은 왜 Stack Exchange에서 작성되었는지, 다른 플랫폼인 lexi-lambda.github.io에서는 왜 작성되지 않았는지 의문
- Benjamin C. Pierce의 "Types and Programming Languages"는 이러한 내용을 다루는 좋은 교재로 추천
- 일부 독자들은 수년 동안 이 주제에 대해 궁금해하였지만, 어떻게 접근해야 할지 몰랐음
- Ada Reference Manual이 이러한 종류의 구문의 실용적인 사용 예로 언급됨
- 기본적인 것부터 시작하여 발전시키는 답변에 대한 칭찬
- "𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍"는 대부분의 언어에서는 nonsensical하지만, Python에서는 `True + 2`가 실제로 정수이며 3과 같음이 예로 들어짐