From 5218bc59a7b92445805c8a20db15168270dd4307 Mon Sep 17 00:00:00 2001 From: coolguy Date: Sun, 30 Aug 2026 03:23:47 +0900 Subject: [PATCH] =?UTF-8?q?exhaust:=20match=20exhaustiveness=EC=99=80=20?= =?UTF-8?q?=EB=8F=84=EB=8B=AC=20=EB=B6=88=EA=B0=80=20=ED=8C=94=20=EA=B2=80?= =?UTF-8?q?=EC=82=AC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 철학 1이 나열한 다섯 항목 중 비어 있던 자리를 채운다. Maranget의 usefulness 알고리즘으로 반례를 만들어 "빠진 경우"를 이름으로 말한다 — 중첩된 자리의 반례도 찾는다(Some(Rect(_, _))). 이 검사가 왜 지금 필요한가: interface hash가 enum 정의 본문을 입력으로 삼는 이유가 바로 이것이다. upstream에 variant가 하나 늘면 downstream의 match가 깨져야 하는데, 검사가 없으면 깨질 것이 없다. 다음 마일스톤(모듈 경계를 넘는 재검사)의 핵심 시나리오가 여기에 걸려 있다. 테스트로 그 시나리오를 직접 고정했다 — 같은 코드가 variant 둘일 때는 통과하고 셋이 되면 깨진다. 구현 중 한 번 틀렸다. 리터럴 패턴을 와일드카드로 줄였더니 Int 리터럴 두 개로 match가 완전해져 버렸다. 리터럴은 인자 없는 생성자이고, 타입의 생성자 집합이 무한하므로 리터럴만으로는 결코 완전해지지 않는다. 생성자 집합을 알 수 없는 타입(외부 타입, 미지수)은 검사하지 않는다. 모르는 것을 위반이라고 말하지 않는다. definite init은 문법이 이미 보장한다는 것을 문서에 적었다 — let이 항상 초기화식을 요구하므로 별도 검사가 필요 없다. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E --- docs/thesis.md | 5 + lib/exhaust.ml | 202 +++++++++++++++++++++++++++++++++ lib/typecheck.ml | 35 ++++++ samples/11_exhaustiveness.cool | 108 ++++++++++++++++++ samples/README.md | 1 + test/test_coollang.ml | 102 ++++++++++++++++- 6 files changed, 450 insertions(+), 3 deletions(-) create mode 100644 lib/exhaust.ml create mode 100644 samples/11_exhaustiveness.cool diff --git a/docs/thesis.md b/docs/thesis.md index 89d4afd..c7a100f 100644 --- a/docs/thesis.md +++ b/docs/thesis.md @@ -8,6 +8,11 @@ AI의 코드 생성 속도 >> 신뢰 확보 속도. 1. 오류는 더 일찍: 컴파일 타임으로 최대한 끌어당김 → null 없음(Option), Result, exhaustive matching, definite init, 미선언 effect = compile error + ※ definite init은 문법이 이미 보장한다: let은 항상 초기화식을 요구하고 + 미초기화 바인딩을 쓸 방법이 없다. 별도 검사가 필요 없는 것이 맞다 + ※ exhaustive matching은 interface hash가 enum 정의 본문을 입력으로 삼는 + 이유이기도 하다. upstream에 variant가 하나 늘면 downstream의 match가 + 깨져야 하는데, 이 검사가 없으면 깨질 것이 없다 2. 검증은 더 빨리: 검증 속도가 언어 설계의 헌법 → fast path(check) / slow path(release, deep verify) 분리 → 컴파일을 느리게/비결정적으로 만드는 기능 원천 배제 diff --git a/lib/exhaust.ml b/lib/exhaust.ml new file mode 100644 index 0000000..25158f4 --- /dev/null +++ b/lib/exhaust.ml @@ -0,0 +1,202 @@ +(* match exhaustiveness와 도달 불가 팔 검사 (Maranget의 usefulness 알고리즘). + + 철학 1의 대표 항목이다. 그리고 interface hash가 enum 정의 본문을 입력으로 + 삼는 이유이기도 하다 — upstream에 variant가 하나 늘면 downstream의 match가 + 깨져야 하는데, 이 검사가 없으면 깨질 것이 없다. + + 생성자 집합을 알 수 없는 타입(외부 타입, 미지수)은 검사하지 않는다. + 모르는 것을 위반이라고 말하지 않는다. *) + +module T = Types + +(* 패턴을 검사용 형태로 줄인다. 바인딩은 와일드카드와 같다 — + 무엇을 덮는가만 중요하다. *) +type cpat = CWild | CCtor of string * cpat list +type ctor = { c_name : string; c_args : T.t list } +type ctors = Finite of ctor list | Infinite + +type env = { + (* enum 이름 -> variant 목록. 제네릭은 인스턴스화해서 넘어온다 *) + variants : string -> T.t list -> (string * T.t list) list option; + is_ctor : string -> bool; +} + +let ctors_of env (t : T.t) : ctors = + match T.resolve t with + | T.TBool -> + Finite + [ { c_name = "true"; c_args = [] }; { c_name = "false"; c_args = [] } ] + | T.TUnit -> Finite [ { c_name = "unit"; c_args = [] } ] + | T.TCon ("Option", [ a ]) -> + Finite + [ + { c_name = "Some"; c_args = [ a ] }; { c_name = "None"; c_args = [] }; + ] + | T.TCon ("Result", [ a; b ]) -> + Finite + [ + { c_name = "Ok"; c_args = [ a ] }; { c_name = "Err"; c_args = [ b ] }; + ] + | T.TCon (n, args) -> ( + match env.variants n args with + | Some vs -> + Finite + (List.map (fun (name, tys) -> { c_name = name; c_args = tys }) vs) + | None -> Infinite) + | _ -> Infinite + +let rec of_pattern env (p : Ast.pattern) : cpat = + match p with + | Ast.P_wild _ -> CWild + | Ast.P_lit (Ast.L_bool true, _) -> CCtor ("true", []) + | Ast.P_lit (Ast.L_bool false, _) -> CCtor ("false", []) + (* 리터럴은 인자 없는 생성자다. 와일드카드로 바꾸면 모든 값을 덮는 것이 되어 + Int 리터럴 몇 개로 exhaustive가 되어버린다. 타입의 생성자 집합이 무한하므로 + 리터럴만으로는 결코 완전해지지 않는다. *) + | Ast.P_lit (Ast.L_int n, _) -> CCtor ("<" ^ n ^ ">", []) + | Ast.P_lit (Ast.L_str v, _) -> CCtor ("<" ^ String.escaped v ^ ">", []) + | Ast.P_bind (n, _) -> if env.is_ctor n then CCtor (n, []) else CWild + | Ast.P_ctor { name; args; _ } -> + if env.is_ctor name then CCtor (name, List.map (of_pattern env) args) + else CWild + +let wilds n = List.init n (fun _ -> CWild) + +(* 행렬을 생성자 c로 특수화한다 *) +let specialize (c : ctor) (matrix : cpat list list) : cpat list list = + let arity = List.length c.c_args in + List.filter_map + (fun row -> + match row with + | CCtor (n, args) :: rest -> + if n = c.c_name then Some (args @ rest) else None + | CWild :: rest -> Some (wilds arity @ rest) + | [] -> None) + matrix + +let default_matrix (matrix : cpat list list) : cpat list list = + List.filter_map + (fun row -> + match row with + | CCtor _ :: _ -> None + | CWild :: rest -> Some rest + | [] -> None) + matrix + +let head_names (matrix : cpat list list) = + List.filter_map + (fun row -> match row with CCtor (n, _) :: _ -> Some n | _ -> None) + matrix + +(* 행렬이 덮지 못하는 반례 벡터를 찾는다. None이면 완전하다. *) +let rec witness env (matrix : cpat list list) (tys : T.t list) : + cpat list option = + match tys with + | [] -> if matrix = [] then Some [] else None + | th :: rest -> ( + let heads = head_names matrix in + match ctors_of env th with + | Finite cs + when List.for_all (fun c -> List.mem c.c_name heads) cs && cs <> [] -> + (* 모든 생성자가 나타났다: 각각으로 파고든다 *) + let rec try_each = function + | [] -> None + | c :: more -> ( + let arity = List.length c.c_args in + match witness env (specialize c matrix) (c.c_args @ rest) with + | Some ws -> + let args = List.filteri (fun i _ -> i < arity) ws in + let tail = List.filteri (fun i _ -> i >= arity) ws in + Some (CCtor (c.c_name, args) :: tail) + | None -> try_each more) + in + try_each cs + | kind -> ( + (* 빠진 생성자가 있거나 집합이 무한하다 *) + match witness env (default_matrix matrix) rest with + | None -> None + | Some ws -> + let head = + match kind with + | Finite cs -> ( + match + List.find_opt (fun c -> not (List.mem c.c_name heads)) cs + with + | Some c -> CCtor (c.c_name, wilds (List.length c.c_args)) + | None -> CWild) + | Infinite -> CWild + in + Some (head :: ws))) + +let rec show_cpat = function + | CWild -> "_" + | CCtor (n, []) -> n + | CCtor (n, args) -> + n ^ "(" ^ String.concat ", " (List.map show_cpat args) ^ ")" + +(* 행 q가 행렬 P에 대해 쓸모 있는가 = P가 덮지 못하는 값을 q가 덮는가 *) +let useful env (matrix : cpat list list) (q : cpat list) (tys : T.t list) : bool + = + let rec go matrix q tys = + match (q, tys) with + | [], [] -> matrix = [] + | qh :: qt, th :: tt -> ( + match qh with + | CCtor (n, args) -> ( + match ctors_of env th with + | Finite cs -> ( + match List.find_opt (fun c -> c.c_name = n) cs with + | Some c -> go (specialize c matrix) (args @ qt) (c.c_args @ tt) + | None -> go (default_matrix matrix) qt tt) + | Infinite -> + let c = + { c_name = n; c_args = List.map (fun _ -> T.TUnknown) args } + in + go (specialize c matrix) (args @ qt) (c.c_args @ tt)) + | CWild -> ( + let heads = head_names matrix in + match ctors_of env th with + | Finite cs + when List.for_all (fun c -> List.mem c.c_name heads) cs + && cs <> [] -> + List.exists + (fun c -> + go (specialize c matrix) + (wilds (List.length c.c_args) @ qt) + (c.c_args @ tt)) + cs + | _ -> go (default_matrix matrix) qt tt)) + | _ -> false + in + go matrix q tys + +type result = { + missing : string option; (* 빠진 경우의 반례 *) + unreachable : int list; (* 도달할 수 없는 팔의 번호 (0부터) *) +} + +let check env (scrutinee : T.t) (pats : Ast.pattern list) : result = + match ctors_of env scrutinee with + | Infinite when T.resolve scrutinee = T.TUnknown -> + (* 생성자 집합을 모르면 검사하지 않는다 *) + { missing = None; unreachable = [] } + | _ -> + let rows = List.map (fun p -> [ of_pattern env p ]) pats in + let unreachable = + let acc = ref [] in + List.iteri + (fun i row -> + let before = List.filteri (fun j _ -> j < i) rows in + if not (useful env before row [ scrutinee ]) then acc := i :: !acc) + rows; + List.rev !acc + in + let missing = + (* 리터럴 패턴이 섞이면 정확한 반례를 만들 수 없다 — 그 열은 무한 + 집합이므로 와일드카드가 없으면 불완전으로 본다 *) + match witness env rows [ scrutinee ] with + | Some ws -> ( + match ws with [ w ] -> Some (show_cpat w) | _ -> Some "_") + | None -> None + in + { missing; unreachable } diff --git a/lib/typecheck.ml b/lib/typecheck.ml index cda17d8..f1c67ee 100644 --- a/lib/typecheck.ml +++ b/lib/typecheck.ml @@ -216,6 +216,7 @@ let rec infer env (e : expr) : T.t = pop env) arms; if arms = [] then err env pos "match에 팔이 없습니다"; + check_exhaustive env s arms pos; result | E_scope { name; parent; body; pos } -> (match lookup env parent with @@ -276,6 +277,40 @@ let rec infer env (e : expr) : T.t = if not (T.unify a b) then mismatch env pos a b "같은 타입끼리만 비교할 수 있습니다"; T.TBool) +(* exhaustiveness: 철학 1의 대표 항목이자 interface hash가 enum 본문을 + 입력으로 삼는 이유다 *) +and check_exhaustive env scrutinee arms pos = + let eenv : Exhaust.env = + { + variants = + (fun name args -> + match Hashtbl.find_opt env.enums name with + | None -> None + | Some (gen, variants) -> + let sub = + try List.map2 (fun v a -> (v, a)) gen args + with Invalid_argument _ -> [] + in + Some + (List.map + (fun (n, tys) -> (n, List.map (T.subst sub []) tys)) + variants)); + is_ctor = + (fun n -> + Hashtbl.mem env.ctors n || List.mem n [ "Ok"; "Err"; "Some"; "None" ]); + } + in + let r = Exhaust.check eenv scrutinee (List.map (fun a -> a.arm_pat) arms) in + (match r.missing with + | None -> () + | Some w -> err env pos (Printf.sprintf "match가 모든 경우를 덮지 않습니다 (빠진 경우: %s)" w)); + List.iter + (fun i -> + match List.nth_opt arms i with + | Some a -> err env a.arm_pos "이 팔은 앞의 팔들에 가려 도달할 수 없습니다" + | None -> ()) + r.unreachable + and nullary_ctor env enum name = match Hashtbl.find_opt env.enums enum with | None -> T.TUnknown diff --git a/samples/11_exhaustiveness.cool b/samples/11_exhaustiveness.cool new file mode 100644 index 0000000..dd5e30e --- /dev/null +++ b/samples/11_exhaustiveness.cool @@ -0,0 +1,108 @@ +// 11. exhaustiveness 검사기가 거부해야 하는 코드 +// +// 철학 1의 대표 항목이자, interface hash가 enum 정의 본문을 입력으로 삼는 이유다. +// upstream에 variant가 하나 늘면 downstream의 match가 깨져야 하는데, +// 이 검사가 없으면 깨질 것이 없다. + +pub enum Shape { + Circle(Int), + Rect(Int, Int), + Point, +} + +// --- 통과해야 하는 것 --- + +pub fn area(s: Shape) -> Int { + match s { + Circle(r) => r * r, + Rect(w, h) => w * h, + Point => 0, + } +} + +pub fn with_wildcard(s: Shape) -> Int { + match s { + Circle(r) => r, + _ => 0, + } +} + +pub fn nested_full(o: Option[Shape]) -> Int { + match o { + Some(Circle(r)) => r, + Some(Rect(w, h)) => w * h, + Some(Point) => 0, + None => 0, + } +} + +pub fn results(r: Result[Int, Int]) -> Int { + match r { + Ok(n) => n, + Err(e) => e, + } +} + +pub fn flags(b: Bool) -> Int { + match b { + true => 1, + false => 0, + } +} + +// --- 여기서부터 전부 오류다 --- + +// [E-match-missing] variant 하나가 빠졌다 +pub fn missing_variant(s: Shape) -> Int { + match s { + Circle(r) => r, + Rect(w, h) => w * h, + } +} + +// [E-match-missing] Bool도 생성자 집합이 유한하다 +pub fn missing_false(b: Bool) -> Int { + match b { + true => 1, + } +} + +// [E-match-missing] Option +pub fn missing_none(o: Option[Int]) -> Int { + match o { + Some(n) => n, + } +} + +// [E-match-missing] 중첩된 자리에서 빠진 경우도 찾는다 +pub fn missing_nested(o: Option[Shape]) -> Int { + match o { + Some(Circle(r)) => r, + None => 0, + } +} + +// [E-match-missing] Int 리터럴은 생성자 집합이 무한하다 +pub fn missing_literal(n: Int) -> Int { + match n { + 0 => 1, + 1 => 2, + } +} + +// [E-match-unreachable] 앞의 와일드카드에 가린다 +pub fn shadowed(s: Shape) -> Int { + match s { + _ => 0, + Point => 1, + } +} + +// [E-match-unreachable] 같은 생성자가 두 번 +pub fn duplicated(s: Shape) -> Int { + match s { + Circle(r) => r, + Circle(x) => x, + _ => 0, + } +} diff --git a/samples/README.md b/samples/README.md index a8ba546..9a451f9 100644 --- a/samples/README.md +++ b/samples/README.md @@ -18,6 +18,7 @@ | 08_syntax_errors | **파서가** 거부해야 하는 코드 | | 09_type_errors | **타입 검사기가** 거부해야 하는 코드 (외부 타입 0개) | | 10_effect_errors | **effect 검사기가** 거부해야 하는 코드 (capability를 직접 정의) | +| 11_exhaustiveness | **exhaustiveness 검사기가** 거부해야 하는 코드 | 05, 08, 09, 10은 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가 기대 진단이며, 넷의 목적이 다르다 — **08은 파서가, 09는 타입 검사기가, diff --git a/test/test_coollang.ml b/test/test_coollang.ml index 656cf18..f77e8fd 100644 --- a/test/test_coollang.ml +++ b/test/test_coollang.ml @@ -583,7 +583,8 @@ let () = f <> "05_move_errors.cool" && f <> "08_syntax_errors.cool" && f <> "09_type_errors.cool" - && f <> "10_effect_errors.cool") + && f <> "10_effect_errors.cool" + && f <> "11_exhaustiveness.cool") |> List.sort compare in List.iter @@ -603,9 +604,12 @@ let () = (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)); - match Driver.typecheck (Filename.concat dir "05_move_errors.cool") with + (match Driver.typecheck (Filename.concat dir "05_move_errors.cool") with | Ok () -> check "05는 move 오류를 내야 한다" false - | Error errors -> check "05의 move 오류" (List.length errors >= 9) + | Error errors -> check "05의 move 오류" (List.length errors >= 9)); + match Driver.typecheck (Filename.concat dir "11_exhaustiveness.cool") with + | Ok () -> check "11은 exhaustiveness 오류를 내야 한다" false + | Error errors -> check "11의 exhaustiveness 오류" (List.length errors >= 7) (* ================================================================== *) (* effect / capability 검사 *) @@ -817,3 +821,95 @@ let () = let () = check "모르는 타입은 copyable로 본다" (move_ok "fn f(x: Widget) -> Widget {\n x\n}") + +(* ================================================================== *) +(* exhaustiveness *) +(* ================================================================== *) + +let e3 = "enum E {\n A(Int),\n B,\n C,\n}\n" + +let () = + check "모든 variant를 덮으면 통과" + (type_ok + (e3 + ^ "fn f(x: E) -> Int {\n\ + \ match x {\n\ + \ A(n) => n,\n\ + \ B => 1,\n\ + \ C => 2,\n\ + \ }\n\ + }")); + check "빠진 variant를 이름으로 말한다" + (type_has + (e3 + ^ "fn f(x: E) -> Int {\n match x {\n A(n) => n,\n B => 1,\n }\n}" + ) + "빠진 경우: C"); + check "와일드카드가 나머지를 덮는다" + (type_ok + (e3 + ^ "fn f(x: E) -> Int {\n match x {\n A(n) => n,\n _ => 0,\n }\n}" + )); + check "Bool의 생성자 집합도 유한하다" + (type_has "fn f(b: Bool) -> Int {\n match b {\n true => 1,\n }\n}" + "빠진 경우: false"); + check "Option" + (type_has + "fn f(o: Option[Int]) -> Int {\n match o {\n Some(n) => n,\n }\n}" + "빠진 경우: None"); + check "Result" + (type_ok + "fn f(r: Result[Int, Int]) -> Int {\n\ + \ match r {\n\ + \ Ok(n) => n,\n\ + \ Err(e) => e,\n\ + \ }\n\ + }"); + check "중첩된 자리의 반례도 찾는다" + (type_has + (e3 + ^ "fn f(o: Option[E]) -> Int {\n\ + \ match o {\n\ + \ Some(A(n)) => n,\n\ + \ None => 0,\n\ + \ }\n\ + }") + "Some(B)"); + check "Int 리터럴만으로는 완전해지지 않는다" + (type_has + "fn f(n: Int) -> Int {\n match n {\n 0 => 1,\n 1 => 2,\n }\n}" + "모든 경우를 덮지 않습니다"); + check "와일드카드가 있으면 리터럴 match도 통과" + (type_ok + "fn f(n: Int) -> Int {\n match n {\n 0 => 1,\n _ => 2,\n }\n}") + +let () = + check "와일드카드 뒤의 팔은 도달할 수 없다" + (type_has + (e3 + ^ "fn f(x: E) -> Int {\n match x {\n _ => 0,\n B => 1,\n }\n}") + "도달할 수 없습니다"); + check "같은 생성자를 두 번 쓰면 뒤가 죽는다" + (type_has + (e3 + ^ "fn f(x: E) -> Int {\n\ + \ match x {\n\ + \ A(n) => n,\n\ + \ A(m) => m,\n\ + \ _ => 0,\n\ + \ }\n\ + }") + "도달할 수 없습니다"); + check "생성자 집합을 모르면 검사하지 않는다" + (type_ok "fn f(w: Widget) -> Int {\n match w {\n _ => 0,\n }\n}") + +(* upstream의 variant 추가가 downstream match를 깨뜨린다 — + interface hash가 enum 본문을 입력으로 삼는 이유 *) +let () = + let two = "enum E {\n A,\n B,\n}\n" in + let three = "enum E {\n A,\n B,\n C,\n}\n" in + let user = + "fn f(x: E) -> Int {\n match x {\n A => 0,\n B => 1,\n }\n}" + in + check "variant 둘일 때는 통과" (type_ok (two ^ user)); + check "variant가 늘면 같은 코드가 깨진다" (type_has (three ^ user) "빠진 경우: C")