Refactor abstraction typing to prevent bugs related to shifting recursive type variables

sColin16 · sColin16 · commit 19fceae38d0b · 2024-01-21T15:09:52.000-07:00
diff --git a/src/structured/termOperations/eval.ml b/src/structured/termOperations/eval.ml
@@ -31,13 +31,21 @@ and eval_rec (term : term) (env : environment) : value =
       | VUnivQuantifier _ ->
           raise (Invalid_argument "Cannot apply a universal quantifier"))
   (* Perform implicit substitution with universal quantifier application for simplicity *)
-  | UnivApplication (app_term, app_type) ->
-    match eval_rec app_term env with
-    | VUnivQuantifier inner_term ->
-      let substituted_inner_term = substitute_univ_var_term app_type inner_term in
-      eval_rec substituted_inner_term env
-    | VConst _ -> raise (Invalid_argument "Cannot perform universal application on a constant")
-    | Closure _ -> raise (Invalid_argument "Cannot perform universal application on a abstraction")
+  | UnivApplication (app_term, app_type) -> (
+      match eval_rec app_term env with
+      | VUnivQuantifier inner_term ->
+          let substituted_inner_term =
+            substitute_univ_var_term app_type inner_term
+          in
+          eval_rec substituted_inner_term env
+      | VConst _ ->
+          raise
+            (Invalid_argument
+               "Cannot perform universal application on a constant")
+      | Closure _ ->
+          raise
+            (Invalid_argument
+               "Cannot perform universal application on a abstraction"))
 
 (* Determines the branch of the abstraction to execute, based on the type of the argument *)
 and resolve_branch branches argument =
diff --git a/src/structured/termOperations/typing.ml b/src/structured/termOperations/typing.ml
@@ -15,21 +15,22 @@ module TypeContextMap = Map.Make (struct
   let compare = compare
 end)
 
-type type_context_map = union_type TypeContextMap.t
+type type_context_map = structured_type TypeContextMap.t
 
 (** [type_lambda_term term] determines the type of a term, if it is well-typed *)
-let rec get_type (term : term) = get_type_rec term TypeContextMap.empty (-1) []
+let rec get_type (term : term) = get_type_rec term TypeContextMap.empty (-1)
 
 (* TODO: is this type context just an environment? Could I simplify by prepending to the front of the list to avoid the level? *)
-and get_type_rec (term : term) (type_context : type_context_map) (level : int)
-    (recursive_context : recursive_context) : structured_type option =
+and get_type_rec (term : term) (type_context : type_context_map) (level : int) :
+    structured_type option =
   match term with
   (* Constants always have label types *)
-  | Const name -> Some (build_structured_type [ Label name ] recursive_context)
+  (* TODO: use the base_to_structured function for this. Need to move it into TypeOperation, I think *)
+  | Const name -> Some (build_structured_type [ Label name ] [])
   (* Use the helper function to determine if an application is well-typed *)
   | Application (t1, t2) ->
-      let left_type = get_type_rec t1 type_context level recursive_context in
-      let right_type = get_type_rec t2 type_context level recursive_context in
+      let left_type = get_type_rec t1 type_context level in
+      let right_type = get_type_rec t2 type_context level in
       flat_map_opt2 get_application_type left_type right_type
   (* Abstractions are well-typed if their argument types don't match
      The return types of the body can be inferred recursively from the argument type *)
@@ -45,78 +46,44 @@ and get_type_rec (term : term) (type_context : type_context_map) (level : int)
       in
       if not disjoint_args then None
       else
-        (* TODO: should we fold right instead? The direction shouldn't matter and we need to append elements to the end of the list *)
-        (* The approach here is to always append to the end of the recursive context. So we add the argument's recursive context to our
-           current context, pass that down recursively, and whatever comes back should have just appended to the recursive context, so we
-           can use that context. We fold over all the branches to accumulate a single recursive context and intersection type *)
-        let intersection_type_opt =
-          List.fold_left
-            (fun acc (arg_branch_type, branch_body) ->
-              match acc with
-              | None -> None
-              | Some (acc_union_type, acc_recursive_context) ->
-                  (* TODO: investigate replacing this call with a call to get_unified_type_context *)
-                  let new_arg_type =
-                    get_type_in_context arg_branch_type acc_recursive_context
-                  in
-                  let body_type_opt =
-                    get_type_rec branch_body
-                      (TypeContextMap.add (level + 1) new_arg_type.union
-                         type_context)
-                      (level + 1) new_arg_type.context
-                  in
-                  Option.map
-                    (fun body_type ->
-                      ( acc_union_type
-                        @ [ (new_arg_type.union, body_type.union) ],
-                        body_type.context ))
-                    body_type_opt)
-            (Some ([], recursive_context))
+        let arg_types = List.map (fun (arg_type, _) -> arg_type) definitions in
+        let body_opt_types =
+          List.map
+            (fun (arg_type, body) ->
+              let new_type_context =
+                TypeContextMap.add (level + 1) arg_type type_context
+              in
+              get_type_rec body new_type_context (level + 1))
             definitions
         in
+        let body_types_opt = opt_list_to_list_opt body_opt_types in
         Option.map
-          (fun (intersection_type, recursive_context) ->
-            build_structured_type
-              [ Intersection intersection_type ]
-              recursive_context)
-          intersection_type_opt
-  (* The type of a variable is variable is based on the type of the argument in the abstraction defining it *)
-  | Variable var_num ->
-      let union_type_opt =
-        TypeContextMap.find_opt (level - var_num) type_context
-      in
-      Option.map
-        (fun union_type -> build_structured_type union_type recursive_context)
-        union_type_opt
+          (fun body_types -> unify_function_types arg_types body_types)
+          body_types_opt
+  (* The type of a variable is based on the type of the argument in the abstraction defining it *)
+  | Variable var_num -> TypeContextMap.find_opt (level - var_num) type_context
   (* Determine the type within the quantifier, then merge the recursive contexts and build the appropriate union type *)
   | UnivQuantifier inner_term ->
-      let inner_type_opt =
-        get_type_rec inner_term type_context level recursive_context
-      in
+      let inner_type_opt = get_type_rec inner_term type_context level in
       Option.map
         (fun inner_type ->
-          let recontextualized_inner =
-            (* TODO: investigate replacing this with a call to get_unified_type_context_pair *)
-            get_type_in_context inner_type recursive_context
-          in
           build_structured_type
-            [ UnivQuantification recontextualized_inner.union ]
-            recontextualized_inner.context)
+            [ UnivQuantification inner_type.union ]
+            inner_type.context)
         inner_type_opt
   | UnivApplication (inner_term, inner_type) ->
-      let inner_term_type_opt =
-        get_type_rec inner_term type_context level recursive_context
-      in
-      Option.join (Option.map
-        (fun inner_term_type ->
-          get_univ_application_type inner_term_type inner_type)
-        inner_term_type_opt)
+      let inner_term_type_opt = get_type_rec inner_term type_context level in
+      Option.join
+        (Option.map
+           (fun inner_term_type ->
+             get_univ_application_type inner_term_type inner_type)
+           inner_term_type_opt)
 
 (** [get_application_type func_type arg_type] determines the resulting type of
     applying a term of type [arg_type] to a term of type [func_type], if
     the function can be applied to the argument *)
-and get_application_type (func : structured_type)
-    (arg : structured_type) : structured_type option =
+and get_application_type (func : structured_type) (arg : structured_type) :
+    structured_type option =
   (* Flatten the func type so only labels and intersection types remain *)
   let func_flat = flatten_union func.union func.context in
   (* The argument should be applicable to any function in the union, so acquire the type of applying the arg to each option *)
@@ -160,25 +127,23 @@ and get_application_option_type
              [] functions)
 
 and get_univ_application_type (quantifier : structured_type)
-    (type_arg : structured_type): structured_type option =
+    (type_arg : structured_type) : structured_type option =
   (* Flatten the func type to get rid of recursive types *)
   let quantifier_flat = flatten_union quantifier.union quantifier.context in
   (* The type argument is applicable to any universal quantification in the union, so determine the types resulting
      from applying the type argument to each universal quantification in the union *)
   let return_opt_types =
     List.map
       (fun quant_option ->
-        get_univ_application_option_type (quant_option, quantifier.context) type_arg)
+        get_univ_application_option_type
+          (quant_option, quantifier.context)
+          type_arg)
       quantifier_flat
   in
   (* Aggregate the return types - if any of them were none, the application is not well-typed *)
   let return_types_opt = opt_list_to_list_opt return_opt_types in
   (* Combine all of the structured types, merging both the unions and and contexts *)
-  Option.map (
-    fun return_types -> (
-      get_type_union return_types
-    )
-  ) return_types_opt
+  Option.map (fun return_types -> get_type_union return_types) return_types_opt
 
 and get_univ_application_option_type
     ((func_option, context1) : flat_base_type * recursive_context)
@@ -191,6 +156,6 @@ and get_univ_application_option_type
   (* If we had bounded quantification, we'd need to make sure the type argument provided is valid *)
   (* But for now, we just substitution in the inner type. The function handles shifting for us *)
   | FUnivQuantification inner_union_type ->
-    (* Construct the complete inner type using the context *)
-    let inner_type = build_structured_type inner_union_type context1 in
-    Some (substitute_univ_var_type type_arg inner_type)
+      (* Construct the complete inner type using the context *)
+      let inner_type = build_structured_type inner_union_type context1 in
+      Some (substitute_univ_var_type type_arg inner_type)
diff --git a/src/structured/typeOperations/context.ml b/src/structured/typeOperations/context.ml
@@ -56,10 +56,29 @@ let get_unified_type_context (types : structured_type list) =
     List.fold_left
       (fun (acc_union, acc_context) next_type ->
         let recontextualized_next_union = get_type_in_context next_type acc_context in
-        let new_acc_union = recontextualized_next_union :: acc_union in
+        let new_acc_union = recontextualized_next_union.union :: acc_union in
         let new_acc_context = recontextualized_next_union.context in
         (new_acc_union, new_acc_context))
       ([], []) types in
   (* We must reverse the list of unions since we fold left but want to keep the types in the right order *)
   let new_unions = List.rev new_unions_rev in
   new_unions, new_context
+
+(* TODO: consider writing more dedicated logic for this rather than the showving intermediate into intersection *)
+(* Takes a list of arg types and their corresponding body types, and joined them into
+   a single structured type for the intersection of the functions *)
+let unify_function_types (arg_types: structured_type list) (body_types: structured_type list) =
+  (* First, build individual unary function types for each arg/body pair *)
+  let unary_types = List.map2 (fun arg_type body_type ->
+    let (new_arg_type, new_body_type), new_context = get_unified_type_context_pair arg_type body_type in
+    build_structured_type [ Intersection [(new_arg_type, new_body_type )]] new_context
+  ) arg_types body_types in
+  (* Then, rectonextualize all of them so we can prepare to join them into a single type *)
+  let new_unary_unions, new_context = get_unified_type_context unary_types in
+  (* Then destructure all of the unary types to build a single intersection type *)
+  let unary_list = List.fold_left (fun acc_func_types next_union ->
+    match next_union with
+    | [ Intersection [ next_unary ]] -> next_unary::acc_func_types
+    | _ -> raise (Failure "there was a problem destructuring the unary function types")
+  ) [] new_unary_unions in
+  build_structured_type [ Intersection unary_list ] new_context
