coolguyandClaude Opus 5
5218bc59a7
철학 1이 나열한 다섯 항목 중 비어 있던 자리를 채운다. Maranget의 usefulness 알고리즘으로 반례를 만들어 "빠진 경우"를 이름으로 말한다 — 중첩된 자리의 반례도 찾는다(Some(Rect(_, _))). 이 검사가 왜 지금 필요한가: interface hash가 enum 정의 본문을 입력으로 삼는 이유가 바로 이것이다. upstream에 variant가 하나 늘면 downstream의 match가 깨져야 하는데, 검사가 없으면 깨질 것이 없다. 다음 마일스톤(모듈 경계를 넘는 재검사)의 핵심 시나리오가 여기에 걸려 있다. 테스트로 그 시나리오를 직접 고정했다 — 같은 코드가 variant 둘일 때는 통과하고 셋이 되면 깨진다. 구현 중 한 번 틀렸다. 리터럴 패턴을 와일드카드로 줄였더니 Int 리터럴 두 개로 match가 완전해져 버렸다. 리터럴은 인자 없는 생성자이고, 타입의 생성자 집합이 무한하므로 리터럴만으로는 결코 완전해지지 않는다. 생성자 집합을 알 수 없는 타입(외부 타입, 미지수)은 검사하지 않는다. 모르는 것을 위반이라고 말하지 않는다. definite init은 문법이 이미 보장한다는 것을 문서에 적었다 — let이 항상 초기화식을 요구하므로 별도 검사가 필요 없다. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
59 lines
3.6 KiB
Markdown
59 lines
3.6 KiB
Markdown
# samples — 문법 탐침
|
|
|
|
여기 있는 `.cool` 파일은 **명세가 아니라 탐침**이다. 목적은
|
|
`docs/thesis.md`의 v0 성공 기준 중 "체감" 항목 — 확정된 규칙으로 짠 코드가
|
|
사람이 읽을 만한지 — 을 눈으로 확인하는 것. 문법 정의는 `docs/grammar.ebnf`.
|
|
|
|
파서는 아직 없으므로 이 파일들은 컴파일되지 않는다.
|
|
|
|
| 파일 | 검증 대상 |
|
|
|---|---|
|
|
| 01_capability_signature | capability 파라미터, effects 절 어순, capability struct 관용구 |
|
|
| 02_higher_order_effects | effect 변수, 구문 수준 제한, 명시적 인스턴스화 |
|
|
| 03_scope_concurrency | TaskScope, 이름 있는 scope, 중첩 시 수명 표현 |
|
|
| 04_enum_match_interface | enum 정의 본문이 interface surface에 들어가는 경로 |
|
|
| 05_move_errors | **move/affinity 검사기가** 거부해야 하는 코드 (자원을 직접 정의) |
|
|
| 06_affine_closure | callable affinity (fn vs affine fn), own과의 직교성 |
|
|
| 07_module_interface | interface artifact가 담아야 할 것 전부 |
|
|
| 08_syntax_errors | **파서가** 거부해야 하는 코드 |
|
|
| 09_type_errors | **타입 검사기가** 거부해야 하는 코드 (외부 타입 0개) |
|
|
| 10_effect_errors | **effect 검사기가** 거부해야 하는 코드 (capability를 직접 정의) |
|
|
| 11_exhaustiveness | **exhaustiveness 검사기가** 거부해야 하는 코드 |
|
|
|
|
05, 08, 09, 10은 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가
|
|
기대 진단이며, 넷의 목적이 다르다 — **08은 파서가, 09는 타입 검사기가,
|
|
10은 effect 검사기가, 05는 move/affinity 검사가** 거부해야 한다. 단계별로
|
|
파일을 나눈 이유는 앞 단계가 첫 오류에서 멈추면 뒤 단계 케이스에 영영
|
|
도달하지 못하기 때문이다.
|
|
|
|
05, 09, 10에는 외부 타입이 하나도 없다. 전부 모듈 안에서 정의되므로 검사기가
|
|
빠져나갈 구석이 없다 — 검사기에 이빨이 있는지 보는 파일들이다. 10은
|
|
capability를 직접 정의해야 메서드의 effect가 알려지고, 05는 affinity의 뿌리가
|
|
capability라 자원 타입을 정의해야 affine임이 유도된다.
|
|
|
|
01~04, 06, 07은 `cool check`를 통과한다 (exit 0).
|
|
|
|
파서는 첫 오류에서 멈춘다(오류 복구 미구현). 타입 검사기는 오류를 전부 모은다.
|
|
|
|
## 확정된 표기
|
|
|
|
- 어순: `fn 이름(파라미터) effects {...} -> 반환타입`.
|
|
함수 타입도 동일: `fn(a) effects e -> b`
|
|
- 파라미터는 기본이 빌림(use, 무표기). 소유 이전만 `own` 유표기.
|
|
capability든 클로저든 일반 affine 값이든 규칙은 하나다
|
|
- 파라미터 밖(반환 타입, struct 필드, channel 원소)은 항상 owned, 무표기
|
|
- 제네릭은 대괄호: 타입 `List[a]`, 식 `map[Int, String, {fs.read}](xs, f)`.
|
|
인덱싱 연산자는 두지 않는다 (`List.at`)
|
|
- 수식어 순서: `own` / `mut`가 먼저, 타입 수식어 `affine`은 타입 안
|
|
- 모듈: 파일 = 모듈, `pub`이 exported, `import "domain/path" as Name`
|
|
- 재수출: `reexport Name` (전용 키워드 — hash 전파를 동반한다)
|
|
- effect 집합: `effects {Type.method, ...}`, 빈 집합은 생략
|
|
- effect 변수: `[e: effects]` 선언, 합집합 `e1 | e2`는 결과 위치 전용
|
|
- 문 구분은 줄바꿈 (Go식 자동 삽입)
|
|
- 블록은 식. 마지막 식이 값이고 `return`은 조기 탈출 전용
|
|
- `if`와 `match`는 식. `match` 가드 없음
|
|
- scope: `scope inner = outer { ... }` — 부모를 구문에 명시
|
|
- 타입 이름은 그 타입의 함수 이름공간: `String.len(s)`, `File.close(f)`
|
|
- 리스트 리터럴 `[a, b, c]`, 빈 리터럴은 타입 주석 필요
|
|
- 오류 전파 `?`는 `Result` 전용
|