[잘라먹는 프로그래밍 언어론] 타입 체계는 명제 논리와 닮아있다 (커리-하워드 대응)

RanolP @ranolp@hackers.pub

이 글은 함수 타입, 합 타입, 곱 타입과 논리 연산의 대응 관계를 탐구하며, 특히 부정(negation)을 타입 시스템에서 어떻게 표현할 수 있는지에 대해 설명합니다. "P가 아니다"는 "P이면 거짓이다"와 동치라는 점을 이용하여, 타입 이론에서 값이 없음을 거짓으로 해석하고, 이를 통해 "정수를 0으로 나눌 수 없다"는 명제를 타입으로 표현하는 방법을 제시합니다. `div_by_zero :: Int -> ⊥`와 같은 표현을 통해 타입 체계와 명제 논리 간의 커리-하워드 대응을 보여주며, 타입 시스템이 논리적 추론과 어떻게 연결되는지에 대한 통찰력을 제공합니다.

Read more →
10

❤️

9 people reacted.

웹개발자입니다.

Uncertified Quasi-pseudo dev

지금까지 다루어 봤던 언어는 아래와 같습니다. MSX Basic Z80 Assembly Pascal GW-Basic C Macromedia Director Visual Basic PHP Flash Actionscript C++ Javascript

그리고 지금은, 하스켈을 비즈니스에 쓰려고 몇 년간 노력하고 있습니다. 지금 상태는, 하스켈 자체를 연구하는 게 아니라, 하스켈 (혹은 함수형 언어) 이해가 어려운 이유를 연구하는 아마추어 연구가쯤 되어버렸습니다. 하스켈 주제로 블로그를 운영 중이지만, 아직은 하스켈 프로그래머라고 자신 있게 말하진 못하고 있습니다. 가끔 이해에 도움이 될만한 측면이 보이면, 가볍게 아이디어를 여러 SNS에 올려보곤 하는데, 그다지 프로그래머에게 쓸모 있는 내용이 포함되진 않는 것 같습니다.

Hi, I'm who's behind Fedify, Hollo, BotKit, and this website, Hackers' Pub! My main account is at @hongminhee洪 民憙 (Hong Minhee).

Fedify, Hollo, BotKit, 그리고 보고 계신 이 사이트 Hackers' Pub을 만들고 있습니다. 제 메인 계정은: @hongminhee洪 民憙 (Hong Minhee).

FedifyHolloBotKit、そしてこのサイト、Hackers' Pubを作っています。私のメインアカウントは「@hongminhee洪 民憙 (Hong Minhee)」に。

🤔

1 person reacted.

인간의 언어처리와 LLM의 언어처리를 서로 비교하는 전산심리언어학(Computational Psycholinguistics)을 연구했'었'습니다.

하지만 CS덕질이 더 재밌다는 걸 깨닫고선 대학원을 탈출했습니다.

요즘은 데이터 엔지니어링과 컴파일러가 재밌어요.