Commit Graph
8 Commits
Author SHA1 Message Date
coolguyandClaude Opus 5 1bd88fc4d7 parser: 재귀 하강 구문 분석기와 AST
grammar.ebnf의 프로덕션 하나에 함수 하나로 대응한다. LL(1)이므로 선읽기는
항상 한 토큰이고 backtracking이 없다. 모든 노드가 위치를 들고 다닌다.

문법과 얽히는 두 자리를 원칙대로 처리했다:
- NEWLINE 흡수는 문법에 { NEWLINE }으로 적힌 자리에서만 한다. 파서가
  "여기선 줄바꿈 무시" 식으로 임의 판단하면 어디서 무시되는지 아무도 모르게
  된다.
- struct 리터럴은 if/match/scope 머리에서 금지하고(no_struct), 괄호·인자
  목록·블록에 들어가면 다시 허용한다.

문법에 새긴 제한이 실제로 파서에서 죽는 것을 확인했다. 파라미터 위치의
effect 합집합과 match 가드는 검사기가 아니라 파서가 거부하며, 진단이
원인을 직접 말한다. 후행 콤마 누락도 일반적인 "닫는 괄호 필요" 대신
"다중 줄 목록에는 후행 콤마가 필요합니다"로 보고한다.

샘플을 실제로 파싱해 두 가지를 잡았다:
- 02와 05가 own을 타입 위치에 쓰고 있었다. 확정한 규칙은 바인딩 수식어가
  이름 앞이므로 샘플이 틀렸다. 수정.
- 05에 구문 오류와 검사기 오류가 섞여 있었다. 파서가 첫 오류에서 멈추면
  검사기 케이스에 영영 도달하지 못하므로 08_syntax_errors.cool로 분리.

grammar.ebnf를 구현과 맞췄다: 제네릭 인자에 effect 집합 허용, 마지막 문의
구분자는 "}" 앞에서 생략, 중괄호 목록 안의 NEWLINE 흡수 위치 명시.

cool ast 추가. cool check는 이제 파서까지 돌리되 여전히 통과했다고 말하지
않는다.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
2026-08-30 02:26:01 +09:00
coolguyandClaude Opus 5 66a2cc6959 lexer: 어휘 분석 구현과 ASI 함정 하나 정정
grammar.ebnf의 어휘 절을 구현한다. 렉서는 선읽기를 요구하지 않고,
문법과 얽히는 유일한 부분인 NEWLINE 삽입은 can_end_statement 하나로
판정한다. 모든 토큰이 위치를 들고 다닌다 — 진단 품질이 헌법급이므로
나중에 붙이지 않는다.

샘플을 실제로 렉싱해 함정을 하나 잡았다. effects 절이 줄 끝에 오면 "}"가
값 종료 토큰이라 NEWLINE이 삽입되어 다음 줄의 "->"와 끊긴다(Go ASI와 같은
형태). 렉서에 문맥을 주는 대신 — 렉서 피드백은 철학 2가 배제한다 —
시그니처 머리의 흡수 위치를 프로덕션에 명시적으로 적어 닫았다. 파서가
임의로 건너뛰는 것이 아니라 문법에 적힌 자리에서만 흡수한다.
다중 줄 목록의 후행 콤마 필수도 함께 명시(콤마로 끝난 줄은 NEWLINE을
만들지 않으므로 목록이 자연히 이어진다).

cool check는 어휘 분석을 돌리되 통과했다고 말하지 않는다. 파이프라인의
나머지가 없는 이상 그 파일은 검사된 것이 아니다. 디버깅용 cool tokens 추가.

테스트 30건: 키워드, 두 글자 연산자 우선, NEWLINE 삽입 6가지 경우,
리터럴과 이스케이프, 오류 7종과 오류 위치, 그리고 samples/*.cool 전체가
어휘 분석을 통과하는지.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
2026-08-30 02:14:37 +09:00
coolguyandClaude Opus 5 630d12104a grammar: v0 EBNF 확정과 열린 문법 결정 8건
열려 있던 문법 항목을 언어 철학에 따라 전부 닫고 EBNF로 고정한다.

- 제네릭 인자를 대괄호로 통일(List[a], map[Int, String](...)). <>는 식
  위치에서 비교 연산자와 갈리지 않아 turbofish라는 제2 표기를 부르는데,
  effect 규칙이 명시적 인스턴스화 문법을 요구하므로 회피할 수 없다.
  대괄호는 전위=리터럴 / 후위=인스턴스화로 위치가 결정해 LL(1)이고 표기가
  하나다. 대가로 인덱싱 연산자를 두지 않는다.
- 파라미터 규칙을 callable 한정에서 전 파라미터로 일반화. 기본은 빌림,
  own만 소유 이전. capability를 예외로 두지 않는 이유는 capability의 존재가
  이미 타입과 effects 절에 드러나기 때문이다 — 표기가 실을 정보는 소유 이동뿐.
- 문 구분은 줄바꿈(Go식 자동 삽입), 블록은 식, return은 조기 탈출 전용.
  if/match를 식으로 두면 재대입이 줄어 move 검사가 단순해진다.
- match 가드 없음. 가드는 exhaustiveness를 흐리고 SMT 없이는 _ 분기를
  강요한다. 철학 1의 대표 항목을 문법 편의와 바꾸지 않는다.
- ?는 Result 전용 하드코딩. 조기 탈출도 블록 종료이므로 scope의 join/cancel이
  ? 경로에서도 실행된다. v1 linear 도입 시 이 경로가 암묵 drop 문제와 만난다.
- 수식어 순서는 바인딩(own, mut) 먼저, 타입(affine) 나중.

docs/grammar.ebnf는 LL(1)을 설계 제약으로 명시하고, effect 합집합을
결과 위치 전용 프로덕션으로 새겨 파라미터 위치의 역산을 파서가 거부하게 한다.
samples/는 확정 표기로 전면 갱신.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
2026-08-30 02:09:58 +09:00
coolguyandClaude Opus 5 e3b19b1300 thesis+samples: 표기 결정 6건 반영과 문법 탐침 추가
샘플을 먼저 써서 EBNF 이전에 체감을 확인했고, 거기서 강제된 결정을 문서에
되먹인다.

- callable 파라미터의 기본을 use(비탈출)로 뒤집고 저장하는 쪽을 own fn으로
  유표기. 반대로 두면 클로저를 저장하지 않는 고차 함수 — 표준 라이브러리의
  거의 전부 — 가 use로 도배된다. 무표기-흔함/유표기-위험은 effects 표기에
  이미 있는 원칙이라 새 조항이 아니다.
- 재수출 키워드를 reexport로 확정. export는 "처음 내보내기"와 흐려지는데
  둘은 hash 규칙에서 의미가 다르고, use는 capability 전달 전용으로 남긴다.
- effects 절을 파라미터 목록 뒤·화살표 앞으로 이동. 중첩 함수 타입의 구문
  모호성이 어순으로 사라지고 읽기 순서가 "입력과 권한 → 출력"이 된다.
  선언과 타입 표기를 같은 어순으로 통일.
- effect 위치 제한을 검사기에서 구문 수준으로 격상. 파라미터 위치는 변수
  단독 또는 리터럴 집합만, 합집합은 결과 위치 전용 프로덕션.
- scope는 이름을 갖는 형태로 확정. 중첩에서 바깥 스코프에 붙이는 정당한
  패턴이 암묵 바인딩으로는 표현되지 않는다.
- capability struct를 표준 관용구로 문서화. named effect set과 scope
  축약형은 v1 예약.

samples/는 명세가 아니라 탐침이다. 05는 통과하면 안 되는 파일이며 체커가
생기면 그대로 테스트 케이스가 된다.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
2026-08-30 01:35:30 +09:00
coolguyandClaude Opus 5 c073e18b41 thesis: second-class 값 개념으로 use/callable/spawn을 일괄 정리
관통하는 해법 하나로 다섯 항목을 닫는다 — second-class 값의 일반화.

- Capability 전달: use의 탈출을 capture 전면 금지가 아니라 "use의 전염"으로
  해결한다. use 값을 capture한 closure는 그 자체가 use 값이 되고 use 파라미터
  위치로만 전달된다. 저장하는 sink는 일반 fn을 요구하므로 대입이 거부되고,
  판정 정보가 전부 시그니처에 남아 검사는 로컬로 유지된다. 별도의 nonescaping
  개념을 만들지 않아 "한 개념 한 방식"이 지켜진다.
- Affinity 전이를 closure 환경까지 확장: callable은 fn(copyable)과
  affine fn 두 종류이며, affinity는 타입 표기의 일부로 interface hash에
  포함된다. bound method와 partial application도 같은 규칙.
- Effect 다형성: 합집합이 있는 이상 일반 unification이 아니므로 해소를
  pattern unification으로 제한한다. 결정 위치에 단독 등장, 합집합은 결과
  위치 전용이며 분해하지 않음. 역산 시그니처는 작성 단계에서 거부된다.
- Invalidation 순서 정정: 변경 모듈 재검사 → hash 비교 → 달라졌을 때만
  dependents를 큐에 추가. hash 비교가 dependents 재검사보다 앞서야
  "본문만 수정 시 downstream 0건"이 성립한다.
  interface hash의 re-export 입력도 목록이 아니라 해소된 정의 본문으로 정정.
- 동시성: spawn은 primitive가 아니라 TaskScope capability의 메서드다.
  TaskScope는 use-only라 탈출할 수 없고, join/cancel은 handle 소비 관례가
  아니라 scope 구문의 실행 의미로 강제한다. v0가 미소비를 허용하는 이상
  handle 기반 보장은 불가능하기 때문이다. 루트 TaskScope는 main에 주입.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
2026-08-30 01:17:49 +09:00
coolguyandClaude Opus 5 994e2362ad thesis: move join 규칙 확정과 affine/linear 경계 명시
두 미해결 항목을 닫는다.

join 규칙 — 보수적 합집합으로 확정. 한 분기에서라도 moved면 병합 지점
이후 moved. 블록당 O(변수 수)로 결정적이고 오류가 한 줄로 끝난다.
경로별 정밀 추적은 오류 설명 가능성을 파는 거래라 채택하지 않고,
"분기 간 불일치 = 에러"는 정당한 코드까지 막아 과잉이다. 조건부 소비의
우회 강요는 인정하는 대가이며, 필요하면 v1에서 관용구로 흡수한다.

affine/linear — v0는 affine이다: 오용 금지, 누수 미검사. 따라서 v0
보안 정리의 범위는 non-duplication까지이며 자원 해제는 주장하지 않는다.
linear 검사와 해제 보장은 v1 과제로 미루되, 암묵적 drop은 선언되지 않은
effect를 실행해 철학 1과 충돌하므로 명시적 소비 강제 방향을 사전 베팅으로
남긴다.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
2026-08-30 00:44:08 +09:00
coolguyandClaude Opus 5 bef741e1ba thesis: Alias/Move 모델을 v0 필수로 승격하고 incremental 규칙 정정
"일반 ownership은 v0 제외"를 폐기한다. 없는 것은 borrow checker와
lifetime이지 alias 규칙이 아니며, 최소 move 모델 없이는 "safe code에
data race 없음" 주장이 closure·channel·container 경로에서 새어나간다.

신설:
- Alias/Move 모델: copyable/affine 이분, 전 경로 move, first-class
  reference 없음. 검사는 함수 로컬 데이터플로우로 결정.
- Capability 전달: second-class use가 기본(탈출 금지), 이전 시에만 move.
  non-duplication은 복제 금지이지 재사용 금지가 아니다.
- Affinity 전이: affine 필드를 가진 타입은 자동 affine. 없으면 wrapper
  복사로 non-duplication 정리가 깨진다.
- Effect의 정적/동적 층 분리: 정적 층은 타입 수준까지, 값 identity 귀속은
  동적/툴링 층.

정정:
- interface hash 입력을 exported surface 전체의 의미적 정규형으로 재정의.
- invalidation을 "direct dependents로만 전파"에서 hash 고정점 규칙으로 교체.
  v0 측정 시나리오를 본문 수정 / 시그니처 수정 둘로 분리.
- 형식 명세 투자 범위를 affine 전이 규칙과 non-duplication까지 확장.
- v0 포함/제외 목록과 v1 계획(제한적 second-class borrow) 갱신.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
2026-08-30 00:42:18 +09:00
coolguyandClaude Opus 5 f0739fc40c 초기 커밋: thesis 문서와 OCaml v0 스캐폴딩
문서(docs/thesis.md)에 네 가지 파생 결정을 반영:
- Effect 다형성: effect 변수는 타입 파라미터와 동일 규율(선언 명시,
  해소는 호출 지점에서 로컬). 집합 의미론으로 row polymorphism 회피.
- 인터페이스 경계: public 경계 전면 명시, 본문 추론 누출 금지,
  interface hash는 정규화된 시그니처 텍스트만으로 계산.
- 모듈/패키지: content hash는 무결성이지 가용성이 아님을 명시.
- 형식 명세 범위를 capability의 affine 규칙까지 확장.

스캐폴딩은 CLI 형태만 고정하고 파이프라인 단계는 비워 둔다.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
2026-08-30 00:35:48 +09:00