From 175be347f4ca82e7bdecd6048bf7d9fa15443ac9 Mon Sep 17 00:00:00 2001 From: Henry Wandover Date: Mon, 20 Jan 2025 10:06:00 -0500 Subject: [PATCH] Added subkind `Numeric` and reconfigured lib.ml's arithmetic operations to use the numeric subkind as a primitive form of ad hoc polymorphism. --- core/commonTypes.ml | 29 +++++++++++++------- core/lib.ml | 60 ++++++++++++++++++++++++++++++------------ core/parser.mly | 4 ++- core/sugartoir.ml | 11 ++++---- core/transformSugar.ml | 10 ++++--- core/typeSugar.ml | 10 ++++--- core/types.ml | 50 +++++++++++++++++++++++++++++++++++ core/types.mli | 1 + links.opam | 4 +-- prelude.links | 1 - 10 files changed, 138 insertions(+), 42 deletions(-) diff --git a/core/commonTypes.ml b/core/commonTypes.ml index 2d05b84f6..594b5eff3 100644 --- a/core/commonTypes.ml +++ b/core/commonTypes.ml @@ -51,6 +51,7 @@ module Restriction = struct type t = | Any | Base + | Numeric | Mono | Session | Effect @@ -64,6 +65,10 @@ module Restriction = struct | Base -> true | _ -> false + let is_numeric = function + | Numeric -> true + | _ -> false + let is_mono = function | Mono -> true | _ -> false @@ -77,20 +82,23 @@ module Restriction = struct | _ -> false let to_string = function - | Any -> "Any" - | Base -> "Base" - | Mono -> "Mono" - | Session -> "Session" - | Effect -> "Eff" + | Any -> "Any" + | Base -> "Base" + | Numeric -> "Numeric" + | Mono -> "Mono" + | Session -> "Session" + | Effect -> "Eff" let min l r = match l, r with - | Any, Any -> Some Any - | Mono, Mono -> Some Mono - | Session, Session -> Some Session - | Effect, Effect -> Some Effect - | Base, Base -> Some Base + | Any, Any -> Some Any + | Mono, Mono -> Some Mono + | Session, Session -> Some Session + | Effect, Effect -> Some Effect + | Base, Base -> Some Base + | Numeric, Numeric -> Some Numeric | x, Any | Any, x -> Some x (* Any will narrow to anything. *) + | Numeric, Mono | Mono, Numeric -> Some Numeric (* Mono can narrow to Numeric. *) | Base, Mono | Mono, Base -> Some Base (* Mono can narrow to Base. *) | Session, Mono | Mono, Session -> Some Session (* Super dubious, but we don't have another way*) | _ -> None @@ -99,6 +107,7 @@ end (* Convenient aliases for constructing values *) let res_any = Restriction.Any let res_base = Restriction.Base +let res_numeric = Restriction.Numeric let res_mono = Restriction.Mono let res_session = Restriction.Session let res_effect = Restriction.Effect diff --git a/core/lib.ml b/core/lib.ml index f5b6e2e44..96dbca191 100644 --- a/core/lib.ml +++ b/core/lib.ml @@ -35,7 +35,7 @@ type primitive = [ Value.t | `PFun of RequestData.request_data -> Value.t list -> Value.t Lwt.t ] -type pure = PURE | IMPURE +type pure = PURE | IMPURE | F2 of (Value.t -> Value.t -> pure) type located_primitive = [ `Client | `Server of primitive | primitive ] @@ -47,12 +47,12 @@ let mk_binop_fn impl unbox_fn constr = function let int_op impl pure : located_primitive * Types.datatype * pure = (`PFun (fun _ -> mk_binop_fn impl Value.unbox_int (fun x -> `Int x))), - datatype "(Int, Int) -> Int", + datatype "(a::Numeric, a) -> Int", pure let float_op impl pure : located_primitive * Types.datatype * pure = (`PFun (fun _ -> mk_binop_fn impl Value.unbox_float (fun x -> `Float x))), - datatype "(Float, Float) -> Float", + datatype "(a::Numeric, a) -> Float", pure let string_op impl pure : located_primitive * Types.datatype * pure = @@ -60,6 +60,21 @@ let string_op impl pure : located_primitive * Types.datatype * pure = datatype "(String, String) -> String", pure +let numeric_op impli implf purei puref : located_primitive * Types.datatype * pure = + (`PFun (fun _ args -> match args with + | [x; y] -> + (match (x,y) with + | (`Int _, `Int _) -> Lwt.return (`Int (impli (Value.unbox_int x) (Value.unbox_int y))) + | (`Float _, `Float _) -> Lwt.return (`Float (implf (Value.unbox_float x) (Value.unbox_float y))) + | _ -> raise (runtime_type_error "type error in numeric operation")) + | _ -> raise (internal_error "arity error in numeric operation"))), + datatype "(a::Numeric, a) -> a", + F2 (fun l r -> match (l, r) with + | (`Int _, `Int _) -> purei + | (`Float _, `Float _) -> puref + | _ -> raise (internal_error ("cannot establish purity in numeric operations")) + ) + let conversion_op' ~unbox ~conv ~(box :'a->Value.t): Value.t list -> Value.t = function | [x] -> box (conv (unbox x)) | _ -> assert false @@ -228,18 +243,22 @@ let project_datetime (f: CalendarShow.t -> int) : located_primitive * Types.data let env : (string * (located_primitive * Types.datatype * pure)) list = [ - "+", int_op (+) PURE; - "-", int_op (-) PURE; - "*", int_op ( * ) PURE; - "/", int_op (/) IMPURE; - "^", int_op pow PURE; - "mod", int_op (mod) IMPURE; - "+.", float_op (+.) PURE; - "-.", float_op (-.) PURE; - "*.", float_op ( *.) PURE; - "/.", float_op (/.) PURE; - "^.", float_op ( ** ) PURE; - "^^", string_op ( ^ ) PURE; + "+", numeric_op ( + ) ( +. ) PURE PURE; + "-", numeric_op ( - ) ( -. ) PURE PURE; + "*", numeric_op ( * ) ( *. ) PURE PURE; + "/", numeric_op ( / ) ( /. ) IMPURE PURE; + "^", numeric_op (pow) ( ** ) PURE PURE; + + "mod", int_op ( mod ) IMPURE; + + (* for backwards compatability *) + "+.", float_op ( +. ) PURE; + "-.", float_op ( -. ) PURE; + "*.", float_op ( *.) PURE; + "/.", float_op ( /. ) PURE; + "^.", float_op ( ** ) PURE; + + "^^", string_op ( ^ ) PURE; "max_int", (Value.box_int max_int, @@ -718,7 +737,6 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [ "print", (p1 (fun msg -> print_string (Value.unbox_string msg); flush stdout; `Record []), - (* datatype "(String) ~> ()", *) datatype "(String) ~> ()", IMPURE); @@ -732,7 +750,15 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [ PURE); "negate", - (p1 (Value.unbox_int ->- (~-) ->- Value.box_int), datatype "(Int) -> Int", + (p1 (fun i -> match i with + | `Int _ -> Value.box_int (- (Value.unbox_int i)) + | `Float _ -> Value.box_float (-. (Value.unbox_float i)) + | _ -> raise (runtime_type_error ("Cannot negate: " ^ Value.string_of_value i))), + datatype "(a::Numeric) -> a", + PURE); + + "negatei", + (p1 (fun i -> Value.box_int (- (Value.unbox_int i))), datatype "(Int) -> Int", PURE); "negatef", diff --git a/core/parser.mly b/core/parser.mly index 60f0d16c9..87e03165c 100644 --- a/core/parser.mly +++ b/core/parser.mly @@ -79,6 +79,7 @@ let restriction_of_string p = function | "Any" -> res_any | "Base" -> res_base + | "Numeric" -> res_numeric | "Session" -> res_session | "Mono" -> res_mono | rest -> @@ -148,6 +149,7 @@ let kind_of p = (* subkind of type abbreviations *) | "Any" -> (Some pk_type, Some (lin_any, res_any)) | "Base" -> (Some pk_type, Some (lin_unl, res_base)) + | "Numeric" -> (Some pk_type, Some (lin_unl, res_numeric)) | "Session" -> (Some pk_type, Some (lin_any, res_session)) | "Eff" -> (Some pk_row , Some (default_effect_lin, res_effect)) | k -> raise (ConcreteSyntaxError (pos p, "Invalid kind: " ^ k)) @@ -158,6 +160,7 @@ let subkind_of p = | "Any" -> Some (lin_any, res_any) | "Lin" -> Some (lin_unl, res_any) (* for linear effect vars *) | "Base" -> Some (lin_unl, res_base) + | "Numeric" -> Some (lin_unl, res_numeric) | "Session" -> Some (lin_any, res_session) | "Eff" -> Some (default_effect_lin, res_effect) | sk -> raise (ConcreteSyntaxError (pos p, "Invalid subkind: " ^ sk)) @@ -198,7 +201,6 @@ let attach_presence_subkind (t, subkind) = | _ -> assert false in attach_subkind_helper update subkind - let alias p name args aliasbody = with_pos p (Aliases [with_pos p (name, args, aliasbody)]) diff --git a/core/sugartoir.ml b/core/sugartoir.ml index c0cad95f3..6df120e70 100644 --- a/core/sugartoir.ml +++ b/core/sugartoir.ml @@ -909,10 +909,11 @@ struct I.apply (instantiate n tyargs, [ev e1; ev e2]) | InfixAppl ((tyargs, BinaryOp.Cons), e1, e2) -> cofv (I.apply_pure (instantiate "Cons" tyargs, [ev e1; ev e2])) - | InfixAppl ((tyargs, BinaryOp.FloatMinus), e1, e2) -> + | InfixAppl ((tyargs, BinaryOp.FloatMinus), e1, e2) -> (* NOTE for legacy purposes *) cofv (I.apply_pure (instantiate "-." tyargs, [ev e1; ev e2])) | InfixAppl ((tyargs, BinaryOp.Minus), e1, e2) -> - cofv (I.apply_pure (instantiate "-" tyargs, [ev e1; ev e2])) + let v1 = (ev e1) and v2 = (ev e2) in + cofv (I.apply_pure (instantiate "-" tyargs, [v1; v2])) | InfixAppl ((_tyargs, BinaryOp.And), e1, e2) -> (* IMPORTANT: we compile boolean expressions to conditionals in order to faithfully capture @@ -920,9 +921,9 @@ struct I.condition (ev e1, ec e2, cofv (I.constant (Constant.Bool false))) | InfixAppl ((_tyargs, BinaryOp.Or), e1, e2) -> I.condition (ev e1, cofv (I.constant (Constant.Bool true)), ec e2) - | UnaryAppl ((_tyargs, UnaryOp.Minus), e) -> - cofv (I.apply_pure(instantiate_mb "negate", [ev e])) - | UnaryAppl ((_tyargs, UnaryOp.FloatMinus), e) -> + | UnaryAppl ((tyargs, UnaryOp.Minus), e) -> + cofv (I.apply_pure (instantiate "negate" tyargs, [ev e])) + | UnaryAppl ((_, UnaryOp.FloatMinus), e) -> (* NOTE for legacy purposes *) cofv (I.apply_pure(instantiate_mb "negatef", [ev e])) | UnaryAppl ((tyargs, UnaryOp.Name n), e) when Lib.is_pure_primitive n -> cofv (I.apply_pure(instantiate n tyargs, [ev e])) diff --git a/core/transformSugar.ml b/core/transformSugar.ml index b0af370a4..01900a932 100644 --- a/core/transformSugar.ml +++ b/core/transformSugar.ml @@ -31,14 +31,14 @@ let type_section env = let type_unary_op env tycon_env = let datatype = DesugarDatatypes.read ~aliases:tycon_env in function - | UnaryOp.Minus -> datatype "(Int) -> Int" - | UnaryOp.FloatMinus -> datatype "(Float) -> Float" + | UnaryOp.Minus -> datatype "(a::Numeric) -> a" + | UnaryOp.FloatMinus -> datatype "(Float) -> Float" (* keeping for compatability with previous version *) | UnaryOp.Name n -> TyEnv.find n env let type_binary_op env tycon_env = let open BinaryOp in let datatype = DesugarDatatypes.read ~aliases:tycon_env in function - | Minus -> TyEnv.find "-" env + | Minus -> datatype "(a::Numeric, a) -> a" | FloatMinus -> TyEnv.find "-." env | RegexMatch flags -> let nativep = List.exists ((=) RegexNative) flags @@ -66,6 +66,10 @@ let type_binary_op env tycon_env = Function (Types.make_tuple_type [a; a], e, Primitive Primitive.Bool )) | Name "!" -> TyEnv.find "Send" env + | Name "+" + | Name "*" + | Name "/" + | Name "^" -> datatype "(a::Numeric, a) -> a" | Name n -> TyEnv.find n env let fun_effects t pss = diff --git a/core/typeSugar.ml b/core/typeSugar.ml index f9f5225b7..ae9109e57 100644 --- a/core/typeSugar.ml +++ b/core/typeSugar.ml @@ -1979,8 +1979,8 @@ let add_empty_usages (p, t) = (p, t, Usage.empty) let type_unary_op pos env = let datatype = datatype env.tycon_env in function - | UnaryOp.Minus -> add_empty_usages (datatype "(Int) { |_::Any}-> Int") - | UnaryOp.FloatMinus -> add_empty_usages (datatype "(Float) { |_::Any}-> Float") + | UnaryOp.Minus -> add_empty_usages (datatype "(a::Numeric) -> a") + | UnaryOp.FloatMinus -> add_empty_usages (datatype "(Float) -> Float") (* keeping for compatability with previous version *) | UnaryOp.Name n -> try add_usages (Utils.instantiate env.var_env n) (Usage.singleton n) @@ -1992,7 +1992,7 @@ let type_binary_op pos ctxt = let open BinaryOp in let open Types in let datatype = datatype ctxt.tycon_env in function - | Minus -> add_empty_usages (Utils.instantiate ctxt.var_env "-") + | Minus -> add_empty_usages (datatype "(a::Numeric, a) -> a") | FloatMinus -> add_empty_usages (Utils.instantiate ctxt.var_env "-.") | RegexMatch flags -> let nativep = List.exists ((=) RegexNative) flags @@ -2021,6 +2021,10 @@ let type_binary_op pos ctxt = Function (Types.make_tuple_type [a; a], eff, Primitive Primitive.Bool), Usage.empty) | Name "!" -> add_empty_usages (Utils.instantiate ctxt.var_env "Send") + | Name "+" + | Name "*" + | Name "/" + | Name "^" -> add_empty_usages (datatype "(a::Numeric, a) -> a") | Name n -> try add_usages (Utils.instantiate ctxt.var_env n) (Usage.singleton n) diff --git a/core/types.ml b/core/types.ml index 6a8690b24..3e98641af 100644 --- a/core/types.ml +++ b/core/types.ml @@ -799,6 +799,50 @@ module Base : Constraint = struct let make_type, make_row = make_restriction_transform Base end +module Numeric : Constraint = struct + open Restriction + open Primitive + + module NumericPredicate = struct + class klass = object + inherit type_predicate as super + + method! point_satisfies f vars point = + match Unionfind.find point with + | Recursive _ -> false + | _ -> super#point_satisfies f vars point + + method! type_satisfies vars = function + (* Unspecified kind *) + | Not_typed -> assert false + | Var _ | Recursive _ | Closed -> + failwith ("[3] freestanding Var / Recursive / Closed not implemented yet (must be inside Meta)") + | Alias _ as t -> super#type_satisfies vars t + | (Application _ | RecursiveApplication _) -> false + | Meta _ as t -> super#type_satisfies vars t + (* Type *) + | Primitive (Int | Float) -> true + | Primitive _ -> false + | (Function _ | Lolli _ | Record _ | Variant _ | Table _ | Lens _ | ForAll (_::_, _)) -> false + | ForAll ([], t) -> super#type_satisfies vars t + (* Effect *) + | Effect _ as t -> super#type_satisfies vars t + | Operation _ -> failwith "TODO types.ml/766" + (* Row *) + | Row _ as t -> super#type_satisfies vars t + (* Presence *) + | Absent -> true + | Present _ as t -> super#type_satisfies vars t + (* Session *) + | Input _ | Output _ | Select _ | Choice _ | Dual _ | End -> false + end + end + + let type_satisfies, row_satisfies = make_restriction_predicate (module NumericPredicate) Numeric false + let can_type_be, can_row_be = make_restriction_predicate (module NumericPredicate) Numeric true + let make_type, make_row = make_restriction_transform Numeric +end + (* unl type stuff *) module Unl : Constraint = struct class unl_predicate = object(o) @@ -994,6 +1038,7 @@ let get_restriction_constraint : Restriction.t -> (module Constraint) option = let open Restriction in function | Any | Effect -> None | Base -> Some (module Base) + | Numeric -> Some (module Numeric) | Session -> Some (module Session) | Mono -> Some (module Mono) @@ -2395,6 +2440,7 @@ struct | (Linearity.Unl, Restriction.Any) -> "" | (Linearity.Any, Restriction.Any) -> "Any" | (Linearity.Unl, Restriction.Base) -> Restriction.to_string res_base + | (Linearity.Unl, Restriction.Numeric) -> Restriction.to_string res_numeric | (Linearity.Any, Restriction.Session) -> Restriction.to_string res_session | (Linearity.Unl, Restriction.Effect) -> Restriction.to_string res_effect | (l, r) -> full (l, r) @@ -2411,6 +2457,8 @@ struct | PrimaryKind.Type, (Linearity.Unl, Restriction.Any) -> "" | PrimaryKind.Type, (Linearity.Unl, Restriction.Base) -> Restriction.to_string res_base + | PrimaryKind.Type, (Linearity.Unl, Restriction.Numeric) -> + Restriction.to_string res_numeric | PrimaryKind.Type, (Linearity.Any, Restriction.Session) -> Restriction.to_string res_session | PrimaryKind.Type, sk -> @@ -3498,6 +3546,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct | (L.Unl, R.Any) -> if is_eff && lincont_enabled then constant "Lin" else Empty (* (1) see above *) | (L.Any, R.Any) -> if is_eff && lincont_enabled then Empty else constant "Any" | (L.Unl, R.Base) -> constant @@ R.to_string res_base + | (L.Unl, R.Numeric) -> constant @@ R.to_string res_numeric | (L.Any, R.Session) -> constant @@ R.to_string res_session | (L.Unl, R.Effect) -> constant @@ R.to_string res_effect (* control-flow-linearity may also need changing this *) | _ -> full_name @@ -3535,6 +3584,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct match subknd with | L.Unl, R.Any -> assert false | L.Unl, R.Base -> StringBuffer.write buf (R.to_string res_base) + | L.Unl, R.Numeric -> StringBuffer.write buf (R.to_string res_numeric) | L.Any, R.Session -> StringBuffer.write buf (R.to_string res_session) | subknd -> let policy = Policy.set_kinds Policy.Full (Context.policy ctx) in diff --git a/core/types.mli b/core/types.mli index 5ef8b3f0a..eb587ebff 100644 --- a/core/types.mli +++ b/core/types.mli @@ -198,6 +198,7 @@ module type Constraint = sig end module Base : Constraint +module Numeric : Constraint module Unl : Constraint module Session : Constraint module Mono : Constraint diff --git a/links.opam b/links.opam index 7f4fc1164..a26d62522 100644 --- a/links.opam +++ b/links.opam @@ -23,8 +23,8 @@ doc: "https://links-lang.org/quick-help.html" bug-reports: "https://github.com/links-lang/links/issues" depends: [ "dune" {>= "2.7"} - "ocaml" { >= "5.1.0"} - "dune-configurator" { >= "3.8"} + "ocaml" {":" >= "5.1.1"} + "dune-configurator" {":" >= "3.8"} "ppx_deriving" "ppx_deriving_yojson" {>= "3.3"} "base64" diff --git a/prelude.links b/prelude.links index 1f53a2b87..c210282d8 100644 --- a/prelude.links +++ b/prelude.links @@ -307,7 +307,6 @@ fun dropWhile(pred, list) { # else 0 # } -sig abs : (Int) -> Int fun abs(i) { if (i < 0) -i else i }