diff --git a/docs/grammar.ebnf b/docs/grammar.ebnf index 2a6be44..ea5c318 100644 --- a/docs/grammar.ebnf +++ b/docs/grammar.ebnf @@ -170,8 +170,11 @@ eff_name = ident , "." , ident ; type = fn_type | named_type ; -fn_type = [ "affine" ] , "fn" , "(" , [ type_list ] , ")" , +(* 함수 타입의 파라미터에도 own을 적는다. 이것이 없으면 "소유권을 가져가는 + * 클로저"를 타입으로 표현할 수 없고, 고차 경계에서 소유권 검사가 뚫린다 *) +fn_type = [ "affine" ] , "fn" , "(" , [ list ] , ")" , [ eff_param ] , [ "->" , type ] ; +fn_param_ty = [ "own" ] , type ; (* 다른 모듈의 타입은 별칭으로 한정한다: Shapes.Shape. * 한 단계뿐이다 — 별칭은 이 모듈의 이름이므로 더 이어질 자리가 없다 *) @@ -277,7 +280,11 @@ list_lit = "[" , [ args ] , "]" ; closure = "fn" , "(" , [ cl_params ] , ")" , [ eff_param ] , [ "->" , type ] , block ; cl_params = list ; -cl_param = ident , [ ":" , type ] ; +(* 클로저 파라미터의 소유권은 리터럴이 스스로 적는다. 타입은 기대 타입에서 + * 읽어오지만 소유권은 읽어오지 않는다 — move 검사는 타입 검사와 별도 순회라 + * 타입을 모르고, 소유권은 타입보다 결과가 크기 때문이다. + * 무표기는 빌림이다 (함수 파라미터와 같다) *) +cl_param = [ "own" ] , ident , [ ":" , type ] ; (* 파라미터 타입 생략 가능. 호출 지점의 기대 타입에서 읽어온다 — 함수 로컬이다. * 기대 타입이 없는 자리에서 생략하면 error *) diff --git a/dogfoods/FINDINGS.md b/dogfoods/FINDINGS.md index 2819166..1791909 100644 --- a/dogfoods/FINDINGS.md +++ b/dogfoods/FINDINGS.md @@ -120,6 +120,49 @@ Mini Shell(파이프라인을 따라 FD를 나름)과 DB Pool(lease를 fold로 → 그 둘을 쓰기 전에 결정해야 한다. +### D5 후속 — 고침, 그리고 std의 실수 하나가 딸려 나왔다 + +`own`을 함수 타입과 클로저 파라미터에 넣었다: + +```cool +fn(own Handle) -> Handle // 타입에 적을 수 있다 +List.fold(xs, h, fn(own acc, n) {...}) // 리터럴에도 적는다 +``` + +클로저 파라미터의 소유권은 **리터럴이 스스로 적는다.** 타입은 기대 타입에서 +읽어오지만 소유권은 읽어오지 않는다 — move 검사는 타입 검사와 별도 순회라 +타입을 모르고, 소유권은 타입보다 결과가 크기 때문이다. + +`unify`가 정확히 일치를 요구한다. 빌리는 클로저를 소유 자리에 넘기는 것은 +안전하지만 그 반대는 아니고, 방향을 다루려면 부분 타입이 필요한데 없다. + +**딸려 나온 것**: `std/list.cool`의 `fold`가 틀려 있었다. + +```cool +f: fn(acc, a) -> acc // 전 — 빌림 +f: fn(own acc, a) -> acc // 후 — 누적자는 매 단계 소비되고 새것으로 바뀐다 +``` + +빌림으로 적혀 있어서 **affine 값을 fold로 실어나를 수 없었다.** 그런데 그 +사실이 드러나지 않았던 이유가 바로 이 구멍이었다 — 클로저 파라미터를 무조건 +소유로 봤으니 아무 오류도 안 났다. **구멍이 자기가 숨긴 버그를 덮고 있었다.** + +#### 남은 한계 — 제네릭을 통과해 보지 못한다 + +move 검사는 타입이 없어 `fold`의 `acc`가 호출 지점에서 무엇으로 묶이는지 +모른다. 그래서 클로저 파라미터에 표기가 없고 기대 타입이 제네릭 변수면 +affinity를 판정하지 못한다. 지금은 소유권 표기 불일치로 잡히지만, 표기가 +양쪽 다 없으면 통과한다. + +근본 해법은 move 검사가 타입을 보는 것이고, 그건 두 순회를 합치는 일이다. +v0에서는 하지 않는다. + +#### 대가 하나 — own이 흔해진다 + +`own`은 흔하지 않은 쪽에 붙는 표기인데, `fold`가 항상 요구하면 흔해진다. +`Config` 같은 copyable 누적자에도 `own`을 적게 된다. 정확히 일치를 요구한 +결과이고, 부분 타입을 넣으면 사라진다. **표기의 신호가 약해지는지 지켜본다.** + ### D6. 문자에 접근할 방법이 없다 — 열림 `String`에 `split`, `trim`, `starts_with`, `contains`뿐이다. 인덱싱도 diff --git a/lib/ast.ml b/lib/ast.ml index 4f83528..391bad4 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -21,7 +21,8 @@ type ty = } | T_fn of { affine : bool; - params : ty list; + (* 파라미터마다 소유권 표시. 무표기는 빌림 *) + params : fn_param_ty list; eff : eff_atom option; ret : ty option; pos : pos; @@ -29,6 +30,7 @@ type ty = (* 제네릭 인자는 타입 또는 effect다. 맨 이름은 둘 다일 수 있으므로 파서는 타입으로 읽고 이름 해소가 판정한다. *) +and fn_param_ty = { pt_own : bool; pt_ty : ty } and targ = TA_ty of ty | TA_eff of eff_atom type pattern = @@ -79,13 +81,16 @@ type expr = | E_binary of { op : binop; lhs : expr; rhs : expr; pos : pos } and closure = { - cl_params : (string * ty option) list; + (* (own, 이름, 타입). 타입은 기대 타입에서 읽어오지만 소유권은 리터럴이 + 스스로 적는다 — move 검사가 타입을 모르기 때문이다 *) + cl_params : cl_param list; cl_eff : eff_atom option; cl_ret : ty option; cl_body : block; cl_pos : pos; } +and cl_param = { cp_own : bool; cp_name : string; cp_ty : ty option } and arm = { arm_pat : pattern; arm_body : expr; arm_pos : pos } and block = { stmts : stmt list; block_pos : pos } @@ -194,7 +199,11 @@ let rec buf_ty b = function Buffer.add_char b ')') | T_fn { affine; params; eff; ret; _ } -> Buffer.add_string b (if affine then "(affine-fn (" else "(fn ("); - buf_list b (buf_ty b) " " params; + buf_list b + (fun (p : fn_param_ty) -> + if p.pt_own then Buffer.add_string b "own "; + buf_ty b p.pt_ty) + " " params; Buffer.add_char b ')'; (match eff with | None -> () @@ -274,9 +283,10 @@ let rec buf_expr b = function | E_closure c -> Buffer.add_string b "(closure ("; buf_list b - (fun (n, t) -> - Buffer.add_string b n; - match t with + (fun (p : cl_param) -> + if p.cp_own then Buffer.add_string b "own "; + Buffer.add_string b p.cp_name; + match p.cp_ty with | None -> () | Some t -> Buffer.add_char b ':'; diff --git a/lib/iface.ml b/lib/iface.ml index cb91197..3d08102 100644 --- a/lib/iface.ml +++ b/lib/iface.ml @@ -108,7 +108,11 @@ let rec q_ty alias defined gen (t : ty) : ty = T_fn { affine; - params = List.map (q_ty alias defined gen) params; + params = + List.map + (fun (p : fn_param_ty) -> + { p with pt_ty = q_ty alias defined gen p.pt_ty }) + params; eff; ret = Option.map (q_ty alias defined gen) ret; pos; diff --git a/lib/ir.ml b/lib/ir.ml index 3284694..9229347 100644 --- a/lib/ir.ml +++ b/lib/ir.ml @@ -194,12 +194,12 @@ let rec lower c (e : Ast.expr) : t = I_make (name, List.map (fun (n, e) -> (n, lower c e)) fields) | Ast.E_closure cl -> lpush c; - List.iter (fun (n, _) -> lbind c n) cl.cl_params; + List.iter (fun (p : Ast.cl_param) -> lbind c p.cp_name) cl.cl_params; let body = lower_block c cl.cl_body in lpop c; I_closure { - c_params = List.map fst cl.cl_params; + c_params = List.map (fun (p : Ast.cl_param) -> p.cp_name) cl.cl_params; c_body = body; c_pos = cl.cl_pos; } diff --git a/lib/move.ml b/lib/move.ml index f68b1de..9285469 100644 --- a/lib/move.ml +++ b/lib/move.ml @@ -41,6 +41,10 @@ type state = { mutable depth : int; (* 클로저 프레임: (프레임 깊이, 잡아온 바깥 바인딩). 중첩 클로저를 위해 스택 *) mutable frames : (int * binding list ref) list; + (* 클로저 인자를 걸을 때 기대 파라미터 타입. move 검사는 타입 검사와 별도 + 순회라 타입을 모르는데, 클로저 파라미터의 affinity를 알아야 빌림 여부를 + 판정할 수 있다. 호출 대상의 시그니처에서 읽어와 여기 잠깐 둔다. *) + mutable cl_expect : fn_param_ty list option; mutable errors : error list; } @@ -334,10 +338,24 @@ and walk_closure st (c : closure) : vinfo = let acc = ref [] in st.frames <- (st.depth, acc) :: st.frames; push st; - List.iter - (fun (n, ann) -> - let affine = match ann with Some t -> ty_affine st t | None -> false in - ignore (add st n ~affine ~use:false ~mut_:false)) + let expect = st.cl_expect in + st.cl_expect <- None; + List.iteri + (fun i (p : cl_param) -> + let affine = + match p.cp_ty with + | Some t -> ty_affine st t + | None -> ( + (* 표기가 없으면 호출 대상의 시그니처에서 읽어온다 *) + match Option.bind expect (fun ps -> List.nth_opt ps i) with + | Some pt -> ty_affine st pt.pt_ty + | None -> false) + in + (* 함수 파라미터와 같은 규칙 — 무표기는 빌림이다. 전에는 클로저 + 파라미터를 무조건 소유로 봤고, 그래서 고차 경계에서 소유권 검사가 + 뚫렸다 (dogfoods/FINDINGS D5). *) + let use_ = affine && not p.cp_own in + ignore (add st p.cp_name ~affine ~use:use_ ~mut_:false)) c.cl_params; ignore (walk_block st (Move "반환할 수") c.cl_body); pop st; @@ -372,6 +390,9 @@ and walk_call st callee args pos = let own = match p with Some p -> p.p_own | None -> false in let pty = Option.map (fun p -> p.p_ty) p in let ctx = if own then Move "다른 함수에 넘길 수" else Borrow in + (match (a, pty) with + | E_closure _, Some (T_fn { params; _ }) -> st.cl_expect <- Some params + | _ -> st.cl_expect <- None); let got = walk st ctx a in (* callable affinity: affine 클로저를 fn 자리에 넘길 수 없다 *) match pty with @@ -448,6 +469,7 @@ let check ?(imports : item list = []) (m : modul) : error list = next_id = 0; depth = 0; frames = []; + cl_expect = None; errors = []; } in diff --git a/lib/parser.ml b/lib/parser.ml index 25d6245..0788ae3 100644 --- a/lib/parser.ml +++ b/lib/parser.ml @@ -145,7 +145,8 @@ and parse_fn_ty st affine p = if kind st = Token.RParen then [] else let rec loop acc = - let t = parse_ty st in + let own = accept st Token.Kw_own in + let t = { pt_own = own; pt_ty = parse_ty st } in if accept st Token.Comma then if kind st = Token.RParen then List.rev (t :: acc) else loop (t :: acc) else List.rev (t :: acc) @@ -449,12 +450,14 @@ and parse_closure st = if kind st = Token.RParen then [] else let rec loop acc = + let own = accept st Token.Kw_own in let n = ident st "파라미터 이름" in let t = if accept st Token.Colon then Some (parse_ty st) else None in + let cp = { cp_own = own; cp_name = n; cp_ty = t } in if accept st Token.Comma then - if kind st = Token.RParen then List.rev ((n, t) :: acc) - else loop ((n, t) :: acc) - else List.rev ((n, t) :: acc) + if kind st = Token.RParen then List.rev (cp :: acc) + else loop (cp :: acc) + else List.rev (cp :: acc) in loop [] in diff --git a/lib/resolve.ml b/lib/resolve.ml index 2e2f0a4..d1099ec 100644 --- a/lib/resolve.ml +++ b/lib/resolve.ml @@ -104,7 +104,7 @@ let rec resolve_ty st = function then external_ref st name pos; List.iter (resolve_targ st pos) args | T_fn { params; eff; ret; pos; _ } -> - List.iter (resolve_ty st) params; + List.iter (fun (p : fn_param_ty) -> resolve_ty st p.pt_ty) params; (match eff with None -> () | Some a -> resolve_eff_atom st (a, pos)); Option.iter (resolve_ty st) ret @@ -170,9 +170,9 @@ let rec resolve_expr st = function | E_closure c -> push st; List.iter - (fun (n, t) -> - Option.iter (resolve_ty st) t; - bind st c.cl_pos n false) + (fun (p : cl_param) -> + Option.iter (resolve_ty st) p.cp_ty; + bind st c.cl_pos p.cp_name false) c.cl_params; (match c.cl_eff with | None -> () diff --git a/lib/typecheck.ml b/lib/typecheck.ml index ceae0fe..8fa4890 100644 --- a/lib/typecheck.ml +++ b/lib/typecheck.ml @@ -14,7 +14,8 @@ type error = { pos : Token.pos; msg : string } type scheme = { s_gen : string list; (* 타입 파라미터 *) s_eff_gen : string list; (* effect 파라미터 *) - s_params : T.t list; + (* (own, 타입). 무표기는 빌림 *) + s_params : (bool * T.t) list; s_eff : T.eff; (* 이 함수를 부르면 수행되는 effect *) s_ret : T.t; } @@ -122,7 +123,10 @@ let rec conv env (gen : string list) (t : Ast.ty) : T.t = T.TFn { affine; - params = List.map (conv env gen) params; + params = + List.map + (fun (p : fn_param_ty) -> (p.pt_own, conv env gen p.pt_ty)) + 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); } @@ -141,7 +145,7 @@ let scheme_of env (d : fn_decl) : scheme = { s_gen = gen; s_eff_gen = egen; - s_params = List.map (fun p -> conv env gen p.p_ty) d.fn_params; + s_params = List.map (fun p -> (p.p_own, 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); @@ -151,14 +155,14 @@ let scheme_of env (d : fn_decl) : scheme = let instantiate (s : scheme) = let sub = List.map (fun v -> (v, T.fresh ())) s.s_gen in let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in - ( List.map (T.subst sub esub) s.s_params, + ( List.map (fun (o, t) -> (o, T.subst sub esub t)) 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 let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in - ( List.map (T.subst sub esub) s.s_params, + ( List.map (fun (o, t) -> (o, T.subst sub esub t)) s.s_params, T.subst_eff esub s.s_eff, T.subst sub esub s.s_ret ) @@ -384,20 +388,31 @@ and infer_closure env (c : closure) (expected : T.t option) = match Option.map T.resolve expected with | Some (T.TFn { params; ret; _ }) when List.length params = List.length c.cl_params -> - (List.map Option.some params, Some ret) + (List.map (fun (o, t) -> Some (o, t)) params, Some ret) | _ -> (List.map (fun _ -> None) c.cl_params, None) in push env; let param_tys = List.map2 - (fun (n, ann) exp -> + (fun (p : cl_param) exp -> let t = - match ann with + match p.cp_ty with | Some a -> conv env [] a - | None -> ( match exp with Some t -> t | None -> T.TUnknown) + | None -> ( match exp with Some (_, t) -> t | None -> T.TUnknown) in - bind env n t; - t) + (* 기대 타입이 소유를 말하는데 리터럴이 안 적었으면 오류다. + 반대도 오류다 — 빌리는 자리에 소유를 주장하면 빌린 값을 소비한다. + 방향을 다루려면 부분 타입이 필요하고 우리에겐 없다. *) + (match exp with + | Some (o, _) when o <> p.cp_own -> + err env c.cl_pos + (Printf.sprintf "클로저 파라미터 %s의 소유권이 기대와 다릅니다 (기대: %s, 적힌 것: %s)" + p.cp_name + (if o then "own" else "빌림") + (if p.cp_own then "own" else "빌림")) + | _ -> ()); + bind env p.cp_name t; + (p.cp_own, t)) c.cl_params expected_params in let declared_ret = Option.map (conv env []) c.cl_ret in @@ -446,7 +461,14 @@ and infer_call env callee args pos = | None -> ( match builtin_ctor n with | Some (params, ret) -> - Some (T.TFn { affine = false; params; eff = []; ret }) + Some + (T.TFn + { + affine = false; + params = List.map (fun t -> (false, t)) params; + eff = []; + ret; + }) | None -> ( match Hashtbl.find_opt env.fns n with | Some s -> @@ -474,7 +496,7 @@ and infer_call env callee args pos = List.iter (fun a -> ignore (infer env a)) args) else List.iter2 - (fun p a -> + (fun (_, p) a -> let got = match a with | E_closure c -> infer_closure env c (Some p) @@ -507,7 +529,7 @@ 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 (fun t -> (false, T.subst sub [] t)) ts | None -> [] in T.TFn diff --git a/lib/types.ml b/lib/types.ml index 71273c2..1ab4345 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -20,7 +20,9 @@ type t = | TUnit | TVar of string | TCon of string * t list - | TFn of { affine : bool; params : t list; eff : eff; ret : t } + (* params의 bool은 소유권이다 (own이면 true). affinity와 다른 축이다 — + affinity는 타입의 성질이고 소유권은 이 자리가 값을 가져가는가다. *) + | TFn of { affine : bool; params : (bool * t) list; eff : eff; ret : t } | TMeta of meta ref and meta = Unbound of int | Bound of t @@ -111,7 +113,8 @@ let rec show t = | TCon (n, args) -> n ^ "[" ^ String.concat ", " (List.map show args) ^ "]" | TFn { affine; params; eff; ret } -> ( (if affine then "affine fn(" else "fn(") - ^ String.concat ", " (List.map show params) + ^ String.concat ", " + (List.map (fun (o, t) -> (if o then "own " else "") ^ show t) params) ^ ")" ^ (match eff_resolve eff with [] -> "" | e -> " effects " ^ eff_show e) ^ match resolve ret with TUnit -> "" | r -> " -> " ^ show r) @@ -122,7 +125,8 @@ let rec occurs r t = match resolve t with | TMeta r' -> r == r' | TCon (_, args) -> List.exists (occurs r) args - | TFn { params; ret; _ } -> List.exists (occurs r) params || occurs r ret + | TFn { params; ret; _ } -> + List.exists (fun (_, t) -> occurs r t) params || occurs r ret | _ -> false (* 결정 위치의 해소: 파라미터의 effect 자리에 단독으로 선 미지수만 묶는다. @@ -157,8 +161,13 @@ let rec unify a b = (* affinity는 타입 동등성의 일부가 아니다. 값이 affine인지는 무엇을 capture했는지로 정해지는 substructural 성질이고, move/affinity 검사가 소유한다. 여기서 섞으면 두 검사가 서로의 결론을 앞질러 버린다. *) + (* 소유권은 타입 동등성의 일부다. 빌리는 클로저를 소유 자리에 넘기는 + 것은 안전하지만 그 반대는 아니고, 방향을 다루려면 부분 타입이 + 필요하다. 우리에겐 없으므로 정확히 일치를 요구한다. *) List.length f.params = List.length g.params - && List.for_all2 unify f.params g.params + && List.for_all2 + (fun (o1, t1) (o2, t2) -> o1 = o2 && unify t1 t2) + f.params g.params && unify_eff f.eff g.eff && unify f.ret g.ret | _ -> false @@ -171,7 +180,7 @@ let rec subst tenv eenv t = TFn { affine = f.affine; - params = List.map (subst tenv eenv) f.params; + params = List.map (fun (o, t) -> (o, subst tenv eenv t)) f.params; eff = subst_eff eenv f.eff; ret = subst tenv eenv f.ret; } diff --git a/samples/app/config.cool b/samples/app/config.cool index ae0bab8..6111548 100644 --- a/samples/app/config.cool +++ b/samples/app/config.cool @@ -106,7 +106,7 @@ pub fn add_problem(cfg: Config, no: Int, msg: String) -> Config { pub fn parse(text: String) -> Config { let lines = List.enumerate(String.split(text, "\n")) let empty = Config { entries: [], problems: [] } - List.fold(lines, empty, fn(cfg, l) { + List.fold(lines, empty, fn(own cfg, l) { parse_line(cfg, l.i + 1, l.value) }) } diff --git a/std/list.cool b/std/list.cool index 2e40842..63122cf 100644 --- a/std/list.cool +++ b/std/list.cool @@ -50,8 +50,10 @@ pub fn filter[a, e: effects]( keep: fn(a) effects e -> Bool, ) effects e -> List[a] +// 누적자는 매 단계 소비되고 새것으로 바뀐다. own이 그 사실을 말한다 — +// 빌림으로 적으면 affine 값을 fold로 실어나를 수 없다. pub fn fold[a, acc, e: effects]( xs: List[a], - init: acc, - f: fn(acc, a) effects e -> acc, + own init: acc, + f: fn(own acc, a) effects e -> acc, ) effects e -> acc