coolguyandClaude Opus 5
79e4ed4190
문서가 "사활"이라고 지목한 단계다. effects 절이 여기서부터 장식이 아니라 검사 대상이 된다. 핵심 규칙 — 미선언 effect = compile error(철학 1). 수행한 자리를 들고 다니므로 진단이 함수 머리가 아니라 실제로 수행한 줄에 붙는다. effect가 흐르는 경로 넷을 모두 막았다: - capability 메서드 호출이 그 메서드의 선언된 effect를 요구한다 - 함수 호출이 그 함수의 effect를 물려준다 - 클로저의 effect는 정의한 자리가 아니라 부르는 자리에서 일어난다. 클로저를 만들기만 하는 것은 effect가 아니고, 인자로 넘겨 호출되는 순간 호출자의 것이 된다 - 파라미터가 허용한 범위를 넘는 함수를 넘기면 거부한다 effect 변수는 결정 위치에서 인자의 effect로 묶인다. 순서가 중요해서 한 번 틀렸다 — 포함 검사를 unify보다 먼저 하면 아직 해소되지 않은 미지수를 제약으로 오해해 정당한 코드를 거부한다. unify가 먼저고, 남는 차이만이 위반이다. 결정되지 않은 미지수는 판정을 미룬다 — 모르는 것을 위반이라고 말하지 않는다. 보안 정리 (i)을 직접 구현했다: capability 메서드는 값을 통해서만 부를 수 있다. 타입 이름으로 부를 수 있으면 capability 없이 effect를 수행하게 되어 정리가 무너진다. effect 검사는 타입 검사와 같은 순회에서 돈다. effect 변수의 해소가 타입 변수와 같은 지점에서 일어나므로 떼어내면 순회와 인스턴스화를 두 번 한다. 소유는 나뉘되 순회는 하나다 — 문서에 근거를 적었다. 10_effect_errors.cool 추가. capability를 직접 정의해야 메서드의 effect가 알려지므로 외부 타입을 하나도 쓰지 않는다. 통과해야 하는 6개와 거부해야 하는 7개가 모두 의도대로 갈린다. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
87 lines
2.4 KiB
Plaintext
87 lines
2.4 KiB
Plaintext
// 10. effect 검사기가 거부해야 하는 코드
|
|
//
|
|
// 09와 같은 이유로 외부 타입이 하나도 없다. capability를 이 파일에서 정의해야
|
|
// 메서드의 effect가 알려지고, 검사기가 실제로 판정할 수 있다.
|
|
|
|
pub capability Db {
|
|
fn read(id: Int) effects {Db.read} -> Int
|
|
fn write(id: Int, v: Int) effects {Db.write}
|
|
}
|
|
|
|
pub capability Log {
|
|
fn write(msg: String) effects {Log.write}
|
|
}
|
|
|
|
// --- 통과해야 하는 것 ---
|
|
|
|
pub fn get(db: Db, id: Int) effects {Db.read} -> Int {
|
|
db.read(id)
|
|
}
|
|
|
|
pub fn copy(db: Db, from: Int, to: Int) effects {Db.read, Db.write} {
|
|
db.write(to, db.read(from))
|
|
}
|
|
|
|
// 헬퍼를 부르면 헬퍼의 effect를 물려받는다
|
|
pub fn get_twice(db: Db, id: Int) effects {Db.read} -> Int {
|
|
get(db, id) + get(db, id)
|
|
}
|
|
|
|
// effect 변수: 결정 위치의 변수가 인자의 effect로 묶인다
|
|
pub fn twice[e: effects](f: fn() effects e) effects e {
|
|
f()
|
|
f()
|
|
}
|
|
|
|
pub fn log_twice(log: Log) effects {Log.write} {
|
|
twice(fn() { log.write("hi") })
|
|
}
|
|
|
|
// effect 없는 함수는 effects 절이 없다
|
|
pub fn pure_add(a: Int, b: Int) -> Int {
|
|
a + b
|
|
}
|
|
|
|
// --- 여기서부터 전부 오류다 ---
|
|
|
|
// [E-effect-undeclared] 선언 없이 capability 메서드를 부른다
|
|
pub fn silent_read(db: Db) -> Int {
|
|
db.read(1)
|
|
}
|
|
|
|
// [E-effect-undeclared] 일부만 선언했다
|
|
pub fn partial(db: Db, id: Int) effects {Db.read} {
|
|
db.write(id, db.read(id))
|
|
}
|
|
|
|
// [E-effect-undeclared] 헬퍼가 수행하는 effect도 물려받아야 한다
|
|
pub fn via_helper(db: Db, id: Int) -> Int {
|
|
get(db, id)
|
|
}
|
|
|
|
// [E-effect-undeclared] 클로저를 통해 새어 나오는 effect
|
|
pub fn via_closure(log: Log) {
|
|
twice(fn() { log.write("hi") })
|
|
}
|
|
|
|
// [E-effect-closure-annotated] 클로저가 선언한 것보다 많이 수행한다
|
|
pub fn closure_lies(log: Log) effects {Log.write} {
|
|
twice(fn() effects {} { log.write("hi") })
|
|
}
|
|
|
|
// [E-effect-param] 파라미터가 허용한 effect를 넘는 함수를 넘긴다
|
|
pub fn takes_pure(f: fn() effects {}) {
|
|
f()
|
|
}
|
|
|
|
pub fn pass_impure(log: Log) effects {Log.write} {
|
|
takes_pure(fn() { log.write("hi") })
|
|
}
|
|
|
|
// [E-capability-static] capability 메서드를 타입 이름으로 부른다.
|
|
// 이것이 허용되면 capability 없이 effect를 수행할 수 있게 되어
|
|
// "capability 없이는 effect를 수행할 수 없다"는 정리가 무너진다.
|
|
pub fn no_instance() effects {Db.read} -> Int {
|
|
Db.read(1)
|
|
}
|