effects: effect/capability 검사

문서가 "사활"이라고 지목한 단계다. 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

lib/driver.ml

@@ -96,7 +96,7 @@ let check (files : string list) : (unit, error list) result =
       in
       if errors <> [] then Error errors
       else
-        (* 타입 검사는 통과했다. 통과했다고 말하지 않는다 — 파이프라인의
+        (* effect 검사까지는 통과했다. 통과했다고 말하지 않는다 — 파이프라인의
            나머지가 아직 없으므로 검사되지 않은 것이다. *)
         Error
           (List.map
@@ -106,7 +106,7 @@ let check (files : string list) : (unit, error list) result =
                  line = 0;
                  col = 0;
                  message =
-                   "타입 검사까지 통과. effect/capability 검사와 move 검사가 아직 구현되지 않았습니다";
+                   "effect/capability 검사까지 통과. move/affinity 검사가 아직 구현되지 않았습니다";
                })
              files)
 

lib/typecheck.ml

@@ -12,8 +12,10 @@ module T = Types
 type error = { pos : Token.pos; msg : string }
 
 type scheme = {
-  s_gen : string list; (* 타입 파라미터 이름 (effect 파라미터는 제외) *)
+  s_gen : string list; (* 타입 파라미터 *)
+  s_eff_gen : string list; (* effect 파라미터 *)
   s_params : T.t list;
+  s_eff : T.eff; (* 이 함수를 부르면 수행되는 effect *)
   s_ret : T.t;
 }
 
@@ -26,6 +28,10 @@ type env = {
   ctors : (string, string) Hashtbl.t; (* variant -> enum *)
   mutable locals : (string * T.t) list list;
   mutable ret : T.t; (* 현재 함수의 선언된 반환 타입 *)
+  (* 현재 본문이 수행한 effect. 위치를 같이 들고 다녀야 "어디서 수행했는지"를
+     말할 수 있다. 클로저에 들어가면 저장하고 비운다 — 클로저의 effect는
+     정의한 자리가 아니라 부르는 자리에서 일어난다. *)
+  mutable performed : (T.atom * Token.pos) list;
   mutable errors : error list;
 }
 
@@ -55,6 +61,14 @@ let lookup env n =
 (* Ast.ty -> Types.t                                                   *)
 (* ------------------------------------------------------------------ *)
 
+let conv_eff_atom (a : Ast.eff_atom) : T.eff =
+  match a with
+  | Eff_var v -> [ T.A_var v ]
+  | Eff_set names -> List.map (fun { cap; meth } -> T.A_name (cap, meth)) names
+
+let conv_eff_result (atoms : Ast.eff_result) : T.eff =
+  T.eff_resolve (List.concat_map conv_eff_atom atoms)
+
 let rec conv env (gen : string list) (t : Ast.ty) : T.t =
   match t with
   | T_named { name; args; _ } -> (
@@ -77,11 +91,12 @@ let rec conv env (gen : string list) (t : Ast.ty) : T.t =
               || Hashtbl.mem env.enums name || Hashtbl.mem env.caps name
             then T.TCon (name, args)
             else T.TUnknown)
-  | T_fn { affine; params; ret; _ } ->
+  | T_fn { affine; params; eff; ret; _ } ->
       T.TFn
         {
           affine;
           params = List.map (conv env gen) params;
+          eff = (match eff with None -> [] | Some a -> conv_eff_atom a);
           ret = (match ret with None -> T.TUnit | Some r -> conv env gen r);
         }
 
@@ -91,20 +106,34 @@ let scheme_of env (d : fn_decl) : scheme =
       (fun g -> if g.gp_effect then None else Some g.gp_name)
       d.fn_gen
   in
+  let egen =
+    List.filter_map
+      (fun g -> if g.gp_effect then Some g.gp_name else None)
+      d.fn_gen
+  in
   {
     s_gen = gen;
+    s_eff_gen = egen;
     s_params = List.map (fun p -> conv env gen p.p_ty) d.fn_params;
+    s_eff =
+      (match d.fn_eff with None -> [] | Some atoms -> conv_eff_result atoms);
     s_ret = (match d.fn_ret with None -> T.TUnit | Some r -> conv env gen r);
   }
 
 (* 호출 지점 인스턴스화: 타입 파라미터마다 새 미지수 *)
 let instantiate (s : scheme) =
   let sub = List.map (fun v -> (v, T.fresh ())) s.s_gen in
-  (List.map (T.subst sub) s.s_params, T.subst sub s.s_ret)
+  let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in
+  ( List.map (T.subst sub esub) s.s_params,
+    T.subst_eff esub s.s_eff,
+    T.subst sub esub s.s_ret )
 
 let instantiate_with (s : scheme) (args : T.t list) =
   let sub = List.map2 (fun v a -> (v, a)) s.s_gen args in
-  (List.map (T.subst sub) s.s_params, T.subst sub s.s_ret)
+  let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in
+  ( List.map (T.subst sub esub) s.s_params,
+    T.subst_eff esub s.s_eff,
+    T.subst sub esub s.s_ret )
 
 (* ------------------------------------------------------------------ *)
 (* 내장 생성자                                                          *)
@@ -144,8 +173,8 @@ let rec infer env (e : expr) : T.t =
               | _ -> (
                   match Hashtbl.find_opt env.fns n with
                   | Some s ->
-                      let params, ret = instantiate s in
-                      T.TFn { affine = false; params; ret }
+                      let params, eff, ret = instantiate s in
+                      T.TFn { affine = false; params; eff; ret }
                   | None -> (
                       match Hashtbl.find_opt env.ctors n with
                       | Some enum -> nullary_ctor env enum n
@@ -268,7 +297,7 @@ and infer_struct env name fields pos =
           match List.assoc_opt fname decl_fields with
           | None -> err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" name fname)
           | Some ft ->
-              let want = T.subst sub ft in
+              let want = T.subst sub [] ft in
               let got = infer env fe in
               if not (T.unify want got) then
                 mismatch env pos want got (Printf.sprintf "%s.%s 필드" name fname))
@@ -302,19 +331,41 @@ and infer_closure env (c : closure) (expected : T.t option) =
       c.cl_params expected_params
   in
   let declared_ret = Option.map (conv env []) c.cl_ret in
-  let saved = env.ret in
+  let saved_ret = env.ret in
   env.ret <-
     (match declared_ret with
     | Some t -> t
     | None -> ( match expected_ret with Some t -> t | None -> T.TUnknown));
+  (* 클로저 본문의 effect는 바깥 함수가 수행하는 것이 아니다. 저장하고 비운다. *)
+  let saved_perf = env.performed in
+  env.performed <- [];
   let body = infer_block env c.cl_body in
+  let inner = env.performed in
+  env.performed <- saved_perf;
+  let declared_eff = Option.map conv_eff_atom c.cl_eff in
+  let eff =
+    match declared_eff with
+    | Some d ->
+        (* 클로저가 effects를 명시했으면 본문이 그 안에 들어야 한다 *)
+        List.iter
+          (fun (a, pos) ->
+            List.iter
+              (fun m ->
+                err env pos
+                  (Printf.sprintf "클로저가 선언하지 않은 effect %s을(를) 수행합니다 (선언: %s)"
+                     (T.atom_show m) (T.eff_show d)))
+              (T.eff_missing ~declared:d ~performed:[ a ]))
+          inner;
+        d
+    | None -> T.eff_resolve (List.map fst inner)
+  in
   (match declared_ret with
   | Some t when not (T.unify t body) -> mismatch env c.cl_pos t body "클로저의 반환"
   | _ -> ());
   let ret = match declared_ret with Some t -> t | None -> body in
-  env.ret <- saved;
+  env.ret <- saved_ret;
   pop env;
-  T.TFn { affine = false; params = param_tys; ret }
+  T.TFn { affine = false; params = param_tys; eff; ret }
 
 and infer_call env callee args pos =
   let fn_ty =
@@ -324,12 +375,13 @@ and infer_call env callee args pos =
         | Some enum -> Some (ctor_fn env enum n)
         | None -> (
             match builtin_ctor n with
-            | Some (params, ret) -> Some (T.TFn { affine = false; params; ret })
+            | Some (params, ret) ->
+                Some (T.TFn { affine = false; params; eff = []; ret })
             | None -> (
                 match Hashtbl.find_opt env.fns n with
                 | Some s ->
-                    let params, ret = instantiate s in
-                    Some (T.TFn { affine = false; params; ret })
+                    let params, eff, ret = instantiate s in
+                    Some (T.TFn { affine = false; params; eff; ret })
                 | None -> None)))
     | _ -> (
         match T.resolve (infer env callee) with
@@ -340,7 +392,10 @@ and infer_call env callee args pos =
   | None ->
       List.iter (fun a -> ignore (infer env a)) args;
       T.TUnknown
-  | Some (T.TFn { params; ret; _ }) ->
+  | Some (T.TFn { params; eff; ret; _ }) ->
+      List.iter
+        (fun a -> env.performed <- (a, pos) :: env.performed)
+        (T.eff_resolve eff);
       if List.length params <> List.length args then (
         err env pos
           (Printf.sprintf "인자 %d개가 필요한데 %d개가 주어졌습니다" (List.length params)
@@ -354,7 +409,22 @@ and infer_call env callee args pos =
               | E_closure c -> infer_closure env c (Some p)
               | _ -> infer env a
             in
-            if not (T.unify p got) then mismatch env pos p got "인자")
+            (* 먼저 unify한다. 결정 위치의 effect 변수는 여기서 인자의
+               effect로 묶인다 — 제약이 아니라 해소다. 그 뒤에 남는 차이만이
+               진짜 위반이다. *)
+            if not (T.unify p got) then mismatch env pos p got "인자";
+            match (T.resolve p, T.resolve got) with
+            | T.TFn pf, T.TFn gf ->
+                let missing =
+                  T.eff_missing ~declared:pf.eff ~performed:gf.eff
+                in
+                if missing <> [] then
+                  err env pos
+                    (Printf.sprintf
+                       "넘긴 함수가 %s을(를) 수행하는데 파라미터가 허용한 effect는 %s입니다"
+                       (String.concat ", " (List.map T.atom_show missing))
+                       (T.eff_show pf.eff))
+            | _ -> ())
           params args;
       ret
   | Some _ -> T.TUnknown
@@ -366,12 +436,26 @@ and ctor_fn env enum name =
       let sub = List.map (fun v -> (v, T.fresh ())) gen in
       let params =
         match List.assoc_opt name variants with
-        | Some ts -> List.map (T.subst sub) ts
+        | Some ts -> List.map (T.subst sub []) ts
         | None -> []
       in
-      T.TFn { affine = false; params; ret = T.TCon (enum, List.map snd sub) }
+      T.TFn
+        {
+          affine = false;
+          params;
+          eff = [];
+          ret = T.TCon (enum, List.map snd sub);
+        }
 
 and infer_field env obj name pos =
+  (* capability 메서드는 값을 통해서만 부를 수 있다. 타입 이름으로 부를 수 있으면
+     capability 없이 effect를 수행하게 되어 보안 정리 (i)이 무너진다. *)
+  (match obj with
+  | E_ident (n, _) when lookup env n = None && Hashtbl.mem env.caps n ->
+      err env pos
+        (Printf.sprintf
+           "capability %s의 메서드는 값을 통해서만 부를 수 있습니다 (%s를 파라미터로 받아야 합니다)" n n)
+  | _ -> ());
   let t = infer env obj in
   match T.resolve t with
   | T.TUnknown -> T.TUnknown
@@ -380,7 +464,7 @@ and infer_field env obj name pos =
       | Some (gen, fields) -> (
           let sub = List.map2 (fun v a -> (v, a)) gen (adjust gen args) in
           match List.assoc_opt name fields with
-          | Some ft -> T.subst sub ft
+          | Some ft -> T.subst sub [] ft
           | None ->
               err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" cname name);
               T.TUnknown)
@@ -389,8 +473,8 @@ and infer_field env obj name pos =
           | Some methods -> (
               match List.assoc_opt name methods with
               | Some s ->
-                  let params, ret = instantiate s in
-                  T.TFn { affine = false; params; ret }
+                  let params, eff, ret = instantiate s in
+                  T.TFn { affine = false; params; eff; ret }
               | None ->
                   err env pos
                     (Printf.sprintf "capability %s에 %s 메서드가 없습니다" cname name);
@@ -428,8 +512,8 @@ and infer_inst env callee args pos =
                  (List.length s.s_gen) (List.length tys));
             T.TUnknown)
           else
-            let params, ret = instantiate_with s tys in
-            T.TFn { affine = false; params; ret })
+            let params, eff, ret = instantiate_with s tys in
+            T.TFn { affine = false; params; eff; ret })
   | _ -> T.TUnknown
 
 and check_pattern env (scrutinee : T.t) (p : pattern) =
@@ -466,7 +550,7 @@ and check_ctor env scrutinee enum name args pos =
       in
       if List.length fields = List.length args then
         List.iter2
-          (fun ft ap -> check_pattern env (T.subst sub ft) ap)
+          (fun ft ap -> check_pattern env (T.subst sub [] ft) ap)
           fields args
 
 (* ------------------------------------------------------------------ *)
@@ -527,10 +611,29 @@ let check_fn env (d : fn_decl) =
         match d.fn_ret with None -> T.TUnit | Some r -> conv env gen r
       in
       env.ret <- declared;
+      env.performed <- [];
       let got = infer_block env body in
       if not (T.unify declared got) then
         mismatch env d.fn_pos declared got
           (Printf.sprintf "%s의 본문이 남기는 값" d.fn_name);
+      (* 미선언 effect = compile error (철학 1).
+         수행한 자리를 알고 있으므로 그 자리에 진단을 붙인다. *)
+      let declared_eff =
+        match d.fn_eff with None -> [] | Some atoms -> conv_eff_result atoms
+      in
+      List.iter
+        (fun (a, pos) ->
+          match T.eff_missing ~declared:declared_eff ~performed:[ a ] with
+          | [] -> ()
+          | missing ->
+              List.iter
+                (fun m ->
+                  err env pos
+                    (Printf.sprintf "선언되지 않은 effect %s (%s의 effects 절은 %s입니다)"
+                       (T.atom_show m) d.fn_name (T.eff_show declared_eff)))
+                missing)
+        (List.rev env.performed);
+      env.performed <- [];
       pop env
 
 let check (m : modul) : error list =
@@ -544,6 +647,7 @@ let check (m : modul) : error list =
       ctors = Hashtbl.create 16;
       locals = [];
       ret = T.TUnit;
+      performed = [];
       errors = [];
     }
   in

lib/types.ml

@@ -1,11 +1,12 @@
-(* 타입 표현과 지역 unification.
+(* 타입과 effect 표현, 그리고 지역 unification.
 
    TUnknown이 핵심이다. 외부 모듈에서 오는 이름은 모듈 로딩이 없는 v0에서
    해소할 수 없다. 그런 타입은 TUnknown이 되고 무엇과도 맞는다 — 모르는 것을
-   틀렸다고 말하지 않기 위해서다. 아는 범위에서만 검사한다.
+   틀렸다고 말하지 않기 위해서다.
 
-   TMeta는 호출 지점에서 제네릭을 인스턴스화할 때 생기는 미지수다. 함수 하나
-   범위에서만 살고 전역으로 흐르지 않는다 (철학 2: 전역 추론 없음). *)
+   effect는 순서 없는 집합이고 합성은 합집합이다. 변수는 집합 변수이며,
+   호출 지점에서 결정 위치(파라미터의 effect 자리에 단독으로 선 변수)를 통해
+   메타에 묶인다. 함수 하나 범위를 넘지 않는다. *)
 
 type t =
   | TUnknown
@@ -15,20 +16,84 @@ type t =
   | TUnit
   | TVar of string
   | TCon of string * t list
-  | TFn of { affine : bool; params : t list; ret : t }
+  | TFn of { affine : bool; params : t list; eff : eff; ret : t }
   | TMeta of meta ref
 
 and meta = Unbound of int | Bound of t
 
+(* effect 집합. 원소는 구체 이름, 집합 변수, 또는 호출 지점의 미지수다. *)
+and eff = atom list
+
+and atom =
+  | A_name of string * string (* Cap.method *)
+  | A_var of string
+  | A_meta of emeta ref
+
+and emeta = EUnbound of int | EBound of eff
+
 let counter = ref 0
 
 let fresh () =
   incr counter;
   TMeta (ref (Unbound !counter))
 
+let fresh_eff () =
+  incr counter;
+  [ A_meta (ref (EUnbound !counter)) ]
+
 let rec resolve t =
   match t with TMeta { contents = Bound u } -> resolve u | _ -> t
 
+(* 묶인 메타를 펼치고 중복을 없앤다. 집합이므로 순서는 의미가 없다. *)
+let rec eff_resolve (e : eff) : eff =
+  let expand a =
+    match a with
+    | A_meta { contents = EBound inner } -> eff_resolve inner
+    | _ -> [ a ]
+  in
+  let flat = List.concat_map expand e in
+  let mem a acc =
+    List.exists
+      (fun b ->
+        match (a, b) with
+        | A_name (c1, m1), A_name (c2, m2) -> c1 = c2 && m1 = m2
+        | A_var x, A_var y -> x = y
+        | A_meta r, A_meta r' -> r == r'
+        | _ -> false)
+      acc
+  in
+  List.fold_left (fun acc a -> if mem a acc then acc else a :: acc) [] flat
+  |> List.rev
+
+let atom_show = function
+  | A_name (c, m) -> c ^ "." ^ m
+  | A_var v -> v
+  | A_meta { contents = EUnbound n } -> Printf.sprintf "_e%d" n
+  | A_meta { contents = EBound _ } -> "?"
+
+let eff_show e =
+  match eff_resolve e with
+  | [] -> "{}"
+  | atoms -> "{" ^ String.concat ", " (List.map atom_show atoms) ^ "}"
+
+let atom_eq a b =
+  match (a, b) with
+  | A_name (c1, m1), A_name (c2, m2) -> c1 = c2 && m1 = m2
+  | A_var x, A_var y -> x = y
+  | A_meta r, A_meta r' -> r == r'
+  | _ -> false
+
+(* declared가 덮지 못하는 원소들. 미지수는 판정을 미룬다 —
+   결정되지 않은 것을 위반이라고 말하지 않는다. *)
+let eff_missing ~declared ~performed =
+  let declared = eff_resolve declared in
+  List.filter
+    (fun a ->
+      match a with
+      | A_meta { contents = EUnbound _ } -> false
+      | _ -> not (List.exists (atom_eq a) declared))
+    (eff_resolve performed)
+
 let rec show t =
   match resolve t with
   | TUnknown -> "?"
@@ -39,10 +104,11 @@ let rec show t =
   | TVar v -> v
   | TCon (n, []) -> n
   | TCon (n, args) -> n ^ "[" ^ String.concat ", " (List.map show args) ^ "]"
-  | TFn { affine; params; ret } -> (
+  | TFn { affine; params; eff; ret } -> (
       (if affine then "affine fn(" else "fn(")
       ^ String.concat ", " (List.map show params)
       ^ ")"
+      ^ (match eff_resolve eff with [] -> "" | e -> " effects " ^ eff_show e)
       ^ match resolve ret with TUnit -> "" | r -> " -> " ^ show r)
   | TMeta { contents = Unbound n } -> Printf.sprintf "_%d" n
   | TMeta { contents = Bound _ } -> "?"
@@ -54,8 +120,19 @@ let rec occurs r t =
   | TFn { params; ret; _ } -> List.exists (occurs r) params || occurs r ret
   | _ -> false
 
-(* 성공하면 true. 실패해도 예외를 던지지 않는다 — 호출자가 위치를 알고
-   진단을 만든다. *)
+(* 결정 위치의 해소: 파라미터의 effect 자리에 단독으로 선 미지수만 묶는다.
+   그 외에는 참을 돌려주고, 실제 포함 검사는 호출 지점에서 방향을 아는
+   쪽이 한다 (진단 품질 때문에). *)
+let unify_eff a b =
+  match (eff_resolve a, eff_resolve b) with
+  | [ A_meta ({ contents = EUnbound _ } as r) ], other ->
+      r := EBound other;
+      true
+  | other, [ A_meta ({ contents = EUnbound _ } as r) ] ->
+      r := EBound other;
+      true
+  | _ -> true
+
 let rec unify a b =
   match (resolve a, resolve b) with
   | TUnknown, _ | _, TUnknown -> true
@@ -75,19 +152,30 @@ let rec unify a b =
          소유한다. 여기서 섞으면 두 검사가 서로의 결론을 앞질러 버린다. *)
       List.length f.params = List.length g.params
       && List.for_all2 unify f.params g.params
-      && unify f.ret g.ret
+      && unify_eff f.eff g.eff && unify f.ret g.ret
   | _ -> false
 
-(* 제네릭 인스턴스화: TVar를 주어진 대입으로 바꾼다 *)
-let rec subst env t =
+(* 제네릭 인스턴스화: 타입 변수와 effect 변수를 동시에 바꾼다 *)
+let rec subst tenv eenv t =
   match resolve t with
-  | TVar v -> ( match List.assoc_opt v env with Some u -> u | None -> TVar v)
-  | TCon (n, args) -> TCon (n, List.map (subst env) args)
+  | TVar v -> ( match List.assoc_opt v tenv with Some u -> u | None -> TVar v)
+  | TCon (n, args) -> TCon (n, List.map (subst tenv eenv) args)
   | TFn f ->
       TFn
         {
           affine = f.affine;
-          params = List.map (subst env) f.params;
-          ret = subst env f.ret;
+          params = List.map (subst tenv eenv) f.params;
+          eff = subst_eff eenv f.eff;
+          ret = subst tenv eenv f.ret;
         }
   | u -> u
+
+and subst_eff eenv (e : eff) : eff =
+  eff_resolve
+    (List.concat_map
+       (fun a ->
+         match a with
+         | A_var v -> (
+             match List.assoc_opt v eenv with Some s -> s | None -> [ a ])
+         | _ -> [ a ])
+       e)