HyperAccel Tech Blog · 2026. 10. 19.
모나드와 범주론 ② 다른 계산, 같은 합성
AI 엔지니어링 브리핑
Option과 List처럼 서로 다른 계산을 함수 합성이라는 같은 틀로 다루고, 그 공통 구조가 범주로 이어지는 과정을 Lean 4로 확인한 글입니다.
문제 & 배경
- 문제 & 배경: 값이 없을 수 있는 함수뿐 아니라 여러 결과를 내는 함수도 일반적인 함수 합성만으로는 연결할 수 없어, 결과를 다음 계산에 어떻게 넘기고 합칠지 별도 규칙이 필요했습니다.
기술 & 해결책
- 기술 & 해결책: Option은 bind로 값이 있을 때만 다음 함수를 실행하고 List는 flatMap으로 각 결과에 함수를 적용한 뒤 목록을 합치도록 하여 공통 합성을 만들고, Lean 4에서 이 합성이 결합법칙과 항등법칙을 만족함을 증명했습니다.
교훈 & 주의점
- 교훈 & 주의점: 계산 방식은 달라도 합성·항등·법칙이 같으면 범주로 설명할 수 있지만, 예시 입력만으로 일반 법칙을 단정하지 말고 모든 타입과 함수에 대한 증명이 필요하며 Option과 List의 합성은 서로 섞어 쓸 수 없습니다.
함께 읽을 글
내용이 비슷해요내용이 비슷한 글을 먼저 보여드려요. 같은 문제나 해결책을 다룬다는 뜻은 아니에요.