Added subkind Numeric and reconfigured lib.ml's

arithmetic operations to use the numeric subkind
as a primitive form of ad hoc polymorphism.

Author: yung-turabian

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

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,19 +47,34 @@ 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 =
   (`PFun (fun _ -> mk_binop_fn impl Value.unbox_string (fun x -> `String x))),
   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",

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)])
 

core/sugartoir.ml

@@ -909,20 +909,21 @@ 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
                  short-circuit evaluation *)
               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]))

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 =

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)

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

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

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"