diff --git a/docs/thesis.md b/docs/thesis.md index 952b40f..277436f 100644 --- a/docs/thesis.md +++ b/docs/thesis.md @@ -268,6 +268,12 @@ Generics (철학 2에서 파생): ※ 각 단계는 그 단계가 소유한 성질만 판정한다. 예: affinity는 타입 동등성이 아니라 substructural 성질이므로 타입 검사가 아니라 move 검사가 소유한다. 단계가 서로의 결론을 앞지르면 진단이 엉뚱한 곳에서 난다 + ※ 다만 effect 검사는 타입 검사와 같은 순회에서 돈다. effect 변수의 해소가 + 타입 변수와 같은 지점(호출 지점의 지역 unification)에서 일어나므로, + 떼어내면 순회와 인스턴스화를 두 번 하게 된다. 소유는 나뉘되 순회는 하나다 + ※ v0는 과잉 선언(선언했으나 수행하지 않는 effect)을 오류로 보지 않는다. + 외부 모듈의 effect를 모르는 상태에서는 판정할 수 없기 때문이다. + 모듈 로딩이 생기면 lint 대상이다 - move/affinity 검사, capability use 규칙, affinity 전이 - effect 변수 (effect 다형성) - interface artifact + hash 기반 incremental invalidation diff --git a/lib/driver.ml b/lib/driver.ml index 0529fb5..8d5b56b 100644 --- a/lib/driver.ml +++ b/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) diff --git a/lib/typecheck.ml b/lib/typecheck.ml index 591034e..cda17d8 100644 --- a/lib/typecheck.ml +++ b/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 diff --git a/lib/types.ml b/lib/types.ml index d418ffc..ae7f094 100644 --- a/lib/types.ml +++ b/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) diff --git a/samples/10_effect_errors.cool b/samples/10_effect_errors.cool new file mode 100644 index 0000000..e16ced0 --- /dev/null +++ b/samples/10_effect_errors.cool @@ -0,0 +1,86 @@ +// 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) +} diff --git a/samples/README.md b/samples/README.md index aaecdbe..ab91c62 100644 --- a/samples/README.md +++ b/samples/README.md @@ -17,14 +17,17 @@ | 07_module_interface | interface artifact가 담아야 할 것 전부 | | 08_syntax_errors | **파서가** 거부해야 하는 코드 | | 09_type_errors | **타입 검사기가** 거부해야 하는 코드 (외부 타입 0개) | +| 10_effect_errors | **effect 검사기가** 거부해야 하는 코드 (capability를 직접 정의) | -05, 08, 09는 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가 기대 -진단이며, 셋의 목적이 다르다 — **08은 파서가, 09는 타입 검사기가, 05는 아직 -없는 move/affinity 검사가** 거부해야 한다. 단계별로 파일을 나눈 이유는 -앞 단계가 첫 오류에서 멈추면 뒤 단계 케이스에 영영 도달하지 못하기 때문이다. +05, 08, 09, 10은 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가 +기대 진단이며, 넷의 목적이 다르다 — **08은 파서가, 09는 타입 검사기가, +10은 effect 검사기가, 05는 아직 없는 move/affinity 검사가** 거부해야 한다. +단계별로 파일을 나눈 이유는 앞 단계가 첫 오류에서 멈추면 뒤 단계 케이스에 +영영 도달하지 못하기 때문이다. -09에는 외부 타입이 하나도 없다. 전부 모듈 안에서 정의되므로 검사기가 +09와 10에는 외부 타입이 하나도 없다. 전부 모듈 안에서 정의되므로 검사기가 TUnknown으로 빠져나갈 구석이 없다 — 검사기에 이빨이 있는지 보는 파일이다. +10은 capability를 직접 정의해야 메서드의 effect가 알려지므로 특히 그렇다. 파서는 첫 오류에서 멈춘다(오류 복구 미구현). 타입 검사기는 오류를 전부 모은다. diff --git a/test/test_coollang.ml b/test/test_coollang.ml index f75eb9d..3d6bd28 100644 --- a/test/test_coollang.ml +++ b/test/test_coollang.ml @@ -580,7 +580,9 @@ let () = Sys.readdir dir |> Array.to_list |> List.filter (fun f -> Filename.check_suffix f ".cool") |> List.filter (fun f -> - f <> "08_syntax_errors.cool" && f <> "09_type_errors.cool") + f <> "08_syntax_errors.cool" + && f <> "09_type_errors.cool" + && f <> "10_effect_errors.cool") |> List.sort compare in List.iter @@ -593,7 +595,96 @@ let () = errors; check (f ^ " 타입 검사") false) ok_files; - match Driver.typecheck (Filename.concat dir "09_type_errors.cool") with + (match Driver.typecheck (Filename.concat dir "09_type_errors.cool") with | Ok () -> check "09는 타입 오류를 내야 한다" false | Error errors -> - check "09의 오류를 전부 모은다 (첫 오류에서 멈추지 않는다)" (List.length errors >= 18) + check "09의 오류를 전부 모은다 (첫 오류에서 멈추지 않는다)" (List.length errors >= 18)); + match Driver.typecheck (Filename.concat dir "10_effect_errors.cool") with + | Ok () -> check "10은 effect 오류를 내야 한다" false + | Error errors -> check "10의 effect 오류" (List.length errors >= 6) + +(* ================================================================== *) +(* effect / capability 검사 *) +(* ================================================================== *) + +let cap = + "capability Db {\n\ + \ fn read(id: Int) effects {Db.read} -> Int\n\ + \ fn touch(id: Int) effects {Db.read}\n\ + }\n" + +(* --- 미선언 effect = compile error (철학 1) --- *) + +let () = + check "선언하면 통과" + (type_ok (cap ^ "fn f(db: Db) effects {Db.read} -> Int {\n db.read(1)\n}")); + check "선언 없이 capability 메서드를 부르면 오류" + (type_has + (cap ^ "fn f(db: Db) -> Int {\n db.read(1)\n}") + "선언되지 않은 effect Db.read"); + check "헬퍼의 effect도 물려받는다" + (type_has + (cap + ^ "fn g(db: Db) effects {Db.read} -> Int {\n\ + \ db.read(1)\n\ + }\n\ + fn f(db: Db) -> Int {\n\ + \ g(db)\n\ + }") + "선언되지 않은 effect Db.read"); + check "effect 없는 함수는 절이 없어도 된다" + (type_ok "fn add(a: Int, b: Int) -> Int {\n a + b\n}") + +(* --- 클로저의 effect는 정의한 자리가 아니라 부르는 자리에서 일어난다 --- *) + +let () = + check "클로저를 만들기만 하면 effect가 새지 않는다" + (type_ok + (cap + ^ "fn f(db: Db) -> fn() effects {Db.read} -> Int {\n\ + \ fn() { db.read(1) }\n\ + }")); + check "클로저가 선언한 것보다 많이 수행하면 오류" + (type_has + (cap + ^ "fn run(f: fn() effects {}) \n\ + fn f(db: Db) {\n\ + \ run(fn() effects {} { db.touch(1) })\n\ + }") + "클로저가 선언하지 않은 effect Db.read"); + check "파라미터가 허용한 범위를 넘는 함수를 넘기면 오류" + (type_has + (cap + ^ "fn run(f: fn() effects {})\n\ + fn f(db: Db) {\n\ + \ run(fn() { db.touch(1) })\n\ + }") + "파라미터가 허용한 effect는 {}") + +(* --- effect 변수: 결정 위치에서 인자의 effect로 묶인다 --- *) + +let () = + let twice = "fn twice[e: effects](f: fn() effects e) effects e\n" in + check "effect 변수는 인자의 effect로 해소된다" + (type_ok + (cap ^ twice + ^ "fn f(db: Db) effects {Db.read} {\n twice(fn() { db.touch(1) })\n}")); + check "해소된 effect가 선언에 없으면 오류" + (type_has + (cap ^ twice ^ "fn f(db: Db) {\n twice(fn() { db.touch(1) })\n}") + "선언되지 않은 effect Db.read"); + check "effect 변수를 그대로 물려주는 것은 통과" + (type_ok + (twice ^ "fn g[e: effects](f: fn() effects e) effects e {\n twice(f)\n}")); + check "effect 변수를 선언하지 않고 물려주면 오류" + (type_has + (twice ^ "fn g[e: effects](f: fn() effects e) {\n twice(f)\n}") + "선언되지 않은 effect e") + +(* --- capability 없이는 effect를 수행할 수 없다 --- *) + +let () = + check "capability 값이 없으면 메서드를 부를 수 없다" + (type_has + (cap ^ "fn f() effects {Db.read} -> Int {\n Db.read(1)\n}") + "값을 통해서만")