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

docs/thesis.md

@@ -66,6 +66,20 @@ Capability 전달 (Alias/Move 모델의 제3의 규칙):
      죽이므로 기각. 별도의 nonescaping 개념을 만들지 않고 use의 전염으로 정의해
      "한 개념 한 방식"을 지킨다 (Swift @noescape, second-class values의 검증된 경로)
 - 소유권 이전이 필요할 때만 명시적 move
+- 파라미터 위치의 callable은 기본이 use(비탈출)이고, 저장하는 쪽이 own fn으로
+  유표기한다. 파라미터 밖(반환 타입, struct 필드, channel 원소)의 callable은
+  use가 애초에 불가능한 위치이므로 무표기로 항상 owned 의미다
+  ※ 무표기-흔함 / 유표기-위험은 이미 언어의 다른 곳에 있는 규칙이다
+     (effect 없는 함수가 무표기, effect 있는 쪽이 effects 유표기).
+     새 조항이 아니라 같은 원칙의 적용이다
+  ※ 반대로 두면 클로저를 저장하지 않는 고차 함수 — 즉 표준 라이브러리의 거의 전부 —
+     가 use 표기로 도배된다. 위험한 쪽(클로저를 오래 보관하는 sink)에 표기가 가야
+     리뷰어의 눈이 그리로 간다
+- capability가 셋 이상 필요하면 capability struct로 접는다 (표준 관용구):
+      struct Deps { pay: PaymentGateway, log: Logger, db: Database }
+  use deps: Deps로 받으면 affinity 전이와 use 규칙이 그대로 적용되므로
+  새 언어 기능 없이 시그니처가 접힌다
+  ※ capability 3개 이상은 대체로 응집도가 낮다는 설계 신호이기도 하다
 근거: non-duplication은 "복제 금지"이지 "재사용 금지"가 아니다. use는 복제를
 만들지 않으므로 보안 정리와 양립하고, 탈출 금지가 locality를 보존한다.
 
@@ -102,14 +116,25 @@ Affinity 전이 (보안 주장의 필수 전제):
   ※ v0는 affine 미소비(누수)를 허용하므로 handle 기반 보장은 애초에 불가능하다.
      실행 의미로 옮겨야 그 허점이 사라진다
 - 루트 TaskScope는 main에 주입 → ambient authority 없이 권한 사슬이 main부터 닫힌다
+- scope는 이름을 갖는다: scope sc { sc.spawn(...) }. 암묵 바인딩은 채택하지 않는다
+  ※ 중첩 시 결정적이다. scope outer { scope inner { ... } }에서 안쪽 블록이
+     바깥 스코프에 spawn하는 것(수명이 다른 태스크를 의도적으로 부모에 붙이는
+     정당한 패턴)이 암묵 바인딩으로는 표현 불가이거나 섀도잉 규칙이라는
+     새 복잡성을 부른다. 이름이 있으면 outer.spawn / inner.spawn으로 그냥 갈린다
+  ※ "어느 스코프에 붙는 태스크인가"가 리뷰어 눈에 보이는 것 자체가 이 언어가
+     파는 물건이다. 축약형은 체감 불만이 실제로 쌓이면 v1에서 검토
 
 Effect 다형성 (철학 2,5에서 파생):
 - effect 변수는 타입 파라미터와 정확히 같은 규율을 따른다:
   시그니처에 선언은 명시 강제, 해소는 호출 지점에서 로컬 unification
       fn map<a, b, e: effects>(
-          f: fn(a) -> b effects e,
-          xs: List<a>
-      ) -> List<b> effects e
+          xs: List<a>,
+          f: fn(a) effects e -> b,
+      ) effects e -> List<b>
+  ※ effects 절은 파라미터 목록 뒤, 화살표 앞이다. 함수 선언과 함수 타입이 같은
+     어순을 쓴다. 반환 타입 뒤에 두면 중첩 함수 타입에서 어느 쪽 effects인지
+     구문만으로 갈리지 않는다 — 괄호로 떠넘기지 않고 어순으로 없앤다.
+     읽기 순서도 "입력과 권한 → 출력"이 되어 자연스럽다
   ※ 전역 추론이 배제하는 것은 "선언 없이 프로그램 전체를 보고 알아내기"이지
      선언된 변수의 로컬 해소가 아니다. map 체크에 필요한 것은
      map과 인자의 시그니처뿐 (locality 유지)
@@ -120,6 +145,11 @@ Effect 다형성 (철학 2,5에서 파생):
     · 변수의 해는 그 결정 위치에서 읽어오기만 한다
     · 합집합 식은 결과 위치에만 허용하며 절대 분해하지 않는다
     · 합집합 식이 기대 타입과 대조되는 위치는 compile error + 명시적 인스턴스화 요구
+  ※ 이 제한은 검사기가 아니라 구문 수준에 새긴다: 파라미터 위치의 effect 절
+     프로덕션은 effects <변수> 또는 effects { 리터럴 집합 }만 허용하고,
+     합집합 프로덕션은 결과 위치 전용이다. "검사기가 거부"가 아니라
+     "그런 문장이 존재하지 않음"이 되므로 오류가 파서의 한 줄로 끝나고,
+     형식 명세에서 증명할 대상도 그만큼 줄어든다
   ※ map·filter·fold류는 전부 이 형태에 들어간다. 역산이 필요한 시그니처(peel류)는
      작성 자체가 거부된다 — 표현력을 팔아 결정성을 사는 거래이고,
      이 언어에서는 항상 그 방향이 맞다
@@ -146,7 +176,10 @@ interface hash의 입력 = 모듈 exported surface 전체의 의미적 정규형
 - 타입의 affinity (copyable / affine)
 - exported constant의 타입과 값
 - capability/effect 선언
-- re-export된 선언을 완전히 해소한 정의 본문 (목록이 아니다)
+- reexport된 선언을 완전히 해소한 정의 본문 (목록이 아니다)
+  ※ 키워드는 reexport 단독이다. export는 "처음 내보내기"와 "다시 내보내기"를
+     흐리는데 이 둘은 hash 규칙에서 의미가 다르므로 구문에서도 달라야 하고,
+     use는 capability 전달 전용으로 보존한다
   ※ A의 enum에 variant가 추가되면 B의 소스가 그대로여도 B의 hash가 변하고,
      C의 exhaustive match가 재검사된다. "의미적 정규형"을 구현 수준까지 내린 것
 원칙: downstream 검사 결과에 영향을 줄 수 있는 모든 것을 포함한다. 의심스러우면
@@ -230,6 +263,9 @@ Generics (철학 2에서 파생):
 - 독립 verifier: compiler를 통짜로 신뢰하지 않고 IR invariants 재검증
 - semantic diff, IR 기반 semantic operations (AI 툴링)
 - generics 완성, contracts, 공유 mutable 탈출구(명시적 타입 하나)
+- named effect set (effects Checkout = {PaymentGateway.charge, Database.write}).
+  v0는 풀어쓴다 — 무엇을 접어도 되는지는 리뷰 가능성 데이터가 쌓인 뒤에 안다
+- 단일 스코프 함수 한정 scope 축약형 (체감 불만이 실제로 쌓였을 때만)
 - 제한적 second-class borrow (Alias/Move 모델의 "반환으로 돌려받기" 대가 완화)
 - linear 검사(자원 해제 보장). 사전 베팅: 암묵적 drop보다 명시적 close(f) 강제 +
   미소비 시 compile error(순수 linear) 쪽이 coollang 철학에 맞는다 — effect가