self-variable notation for record types, close #64

Author: mikeshulman

docs/source/codata-types.rst

@@ -32,6 +32,20 @@ That is, we use brackets and bars instead of parentheses and commas.  Moreover,
 It is often helpful to think of a codatatype as akin to an *interface* in an object-oriented programming language, in which case the variable ``x`` is like the ``this`` or ``self`` pointer by which an object refers to itself.  Of course an interface in a simply-typed language does not need a self-pointer to specify the *types* of its methods, but in a dependently typed language it does.  In higher-dimensional type theories, the presence of this variable can be used in other ways than simply accessing previously declared methods, such as in the definition of semi-simplicial types using :ref:`Displayed coinductive types`.
 
 
+Self variables for record types
+-------------------------------
+
+The syntax of self variables is also available as an alternative when defining record types.  For instance, the usual sort of Σ-type, as a record with eta-conversion, can also be defined by
+
+.. code-block:: none
+
+   def Σ (A : Type) (B : A → Type) : Type ≔ sig (
+     x .fst : A,
+     x .snd : B (x .fst))
+
+It should be emphasized that this is just a different notation for record types, not a "codatatype with eta-conversion".  At present there is no practical difference, but in the future recursion will be forbidden in record types, even those that use the self-variable notation.
+
+
 Copattern matching
 ------------------
 

lib/core/check.ml

@@ -648,11 +648,37 @@ let rec check : type a b s.
                           | Eq -> None
                           | Neq -> Some ()))
                     None fields in
-                check_codata status ctx tyargs Emp
+                check_codata status ctx Noeta tyargs Emp
                   (Fibrancy.Codata.empty dim dim (Ctx.dbwd ctx) Noeta
                      (readback_neu ctx (head_of_potential head) apps))
                   (Bwd.to_list fields) Emp ~has_higher_fields)
         | _ -> fatal (Checking_canonical_at_nonuniverse ("codatatype", PVal (ctx, ty))))
+    | SelfRecord fields, Potential (head, apps, _) -> (
+        match view_type ~severity ty "typechecking self-record" with
+        | Canonical (_, UU dim, ins, tyargs) -> (
+            match (D.compare_zero dim, Endpoints.hott (), !gel_ok) with
+            | Pos _, Some _, false ->
+                fatal (Unimplemented "general higher-dimensional types in HOTT: use glue")
+            | _ -> (
+                let Eq = eq_of_ins_zero ins in
+                let has_higher_fields =
+                  Bwd.fold_left
+                    (fun acc (Field.Wrap fld, _) ->
+                      match acc with
+                      | Some () -> Some ()
+                      | None -> (
+                          match D.compare (Field.dim fld) D.zero with
+                          | Eq -> None
+                          | Neq -> Some ()))
+                    None fields in
+                match has_higher_fields with
+                | Some () -> fatal (Unimplemented "higher fields in record types: use codata")
+                | None ->
+                    check_codata status ctx Eta tyargs Emp
+                      (Fibrancy.Codata.empty dim dim (Ctx.dbwd ctx) Eta
+                         (readback_neu ctx (head_of_potential head) apps))
+                      (Bwd.to_list fields) Emp ~has_higher_fields))
+        | _ -> fatal (Checking_canonical_at_nonuniverse ("codatatype", PVal (ctx, ty))))
     | Record (xs, fields, opacity), Potential (head, apps, _) -> (
         match view_type ~severity ty "typechecking record" with
         | Canonical (_, UU dim, ins, tyargs) -> (
@@ -679,6 +705,7 @@ let rec check : type a b s.
     | Synth (Match _), Kinetic l -> kinetic_of_potential l ctx tm ty "match"
     | Refute _, Kinetic l -> kinetic_of_potential l ctx tm ty "match"
     | Codata _, Kinetic l -> kinetic_of_potential l ctx tm ty "codata"
+    | SelfRecord _, Kinetic l -> kinetic_of_potential l ctx tm ty "sig"
     | Record _, Kinetic l -> kinetic_of_potential l ctx tm ty "sig"
     | Data _, Kinetic l -> kinetic_of_potential l ctx tm ty "data"
     (* If the user left a hole, we create an eternal metavariable. *)
@@ -1926,33 +1953,34 @@ and with_codata_so_far : type a b n c et.
   in
   run_with_definition h (hyp codataterm) errs @@ fun () -> cont domvars codataterm
 
-and check_codata : type a b n.
+and check_codata : type a b n et.
     (b, potential) status ->
     (a, b) Ctx.t ->
+    (potential, et) eta ->
     (D.zero, n, n, normal) TubeOf.t ->
-    (b * n * no_eta) Term.CodatafieldAbwd.t ->
-    (n, n, b, no_eta) Fibrancy.Codata.t ->
+    (b * n * et) Term.CodatafieldAbwd.t ->
+    (n, n, b, et) Fibrancy.Codata.t ->
     (Field.wrapped * a Raw.codatafield) list ->
     Code.t Asai.Diagnostic.t Bwd.t ->
     has_higher_fields:unit option ->
     (b, potential) term =
- fun status ctx tyargs checked_fields fibrancy raw_fields errs ~has_higher_fields ->
+ fun status ctx eta tyargs checked_fields fibrancy raw_fields errs ~has_higher_fields ->
   let dim = TubeOf.inst tyargs in
   match raw_fields with
   | [] -> (
       match errs with
       | Emp ->
-          with_codata_so_far status Noeta ctx `Opaque dim tyargs checked_fields fibrancy
+          with_codata_so_far status eta ctx `Opaque dim tyargs checked_fields fibrancy
             ~has_higher_fields errs
           @@ fun _ codataterm -> codataterm
       | Snoc _ -> fatal (Accumulated ("check_codata", errs)))
   | (Wrap fld, Codatafield (x, rty)) :: raw_fields -> (
-      with_codata_so_far status Noeta ctx `Opaque dim tyargs checked_fields fibrancy
+      with_codata_so_far status eta ctx `Opaque dim tyargs checked_fields fibrancy
         ~has_higher_fields errs
       @@ fun domvars _ ->
       let newctx = Ctx.cube_vis ctx x domvars in
-      match (D.compare_zero (Field.dim fld), D.compare_zero (TubeOf.inst tyargs)) with
-      | Zero, _ ->
+      match (D.compare_zero (Field.dim fld), D.compare_zero (TubeOf.inst tyargs), eta) with
+      | Zero, _, _ ->
           (* Zero-dimensional field *)
           let checked_fields, fibrancy, errs =
             Reporter.try_with ~fatal:(fun e -> (checked_fields, fibrancy, Snoc (errs, e)))
@@ -1961,16 +1989,19 @@ and check_codata : type a b n.
             let cty = check (Kinetic `Nolet) newctx rty (universe D.zero) in
             let entry = CodatafieldAbwd.Entry (fld, Lower cty) in
             (Snoc (checked_fields, entry), Fibrancy.Codata.add_field fibrancy entry, errs) in
-          check_codata status ctx tyargs checked_fields fibrancy raw_fields errs ~has_higher_fields
-      | Pos _, Zero ->
+          check_codata status ctx eta tyargs checked_fields fibrancy raw_fields errs
+            ~has_higher_fields
+      | Pos _, Zero, Noeta ->
           (* Higher-dimensional field, currently requires a zero-dimensional codatatype (non-Gel). *)
           let checked_fields, errs =
             Reporter.try_with ~fatal:(fun e -> (checked_fields, Snoc (errs, e))) @@ fun () ->
             let (Degctx (plusmap, degctx, _)) = degctx newctx (Field.dim fld) in
             let cty = check (Kinetic `Nolet) degctx rty (universe D.zero) in
             (Snoc (checked_fields, Entry (fld, Codatafield.Higher (plusmap, cty))), errs) in
-          check_codata status ctx tyargs checked_fields fibrancy raw_fields errs ~has_higher_fields
-      | Pos _, Pos _ -> fatal (Unimplemented "higher fields in higher-dimensional codatatypes"))
+          check_codata status ctx eta tyargs checked_fields fibrancy raw_fields errs
+            ~has_higher_fields
+      | Pos _, Zero, Eta -> fatal (Unimplemented "higher fields in record types")
+      | Pos _, Pos _, _ -> fatal (Unimplemented "higher fields in higher-dimensional codatatypes"))
 
 and check_record : type a f1 f2 f af d acd b n.
     (b, potential) status ->

lib/core/dump.ml

@@ -308,6 +308,7 @@ module F = struct
     | Data _ -> fprintf ppf "Data(?)"
     | Codata _ -> fprintf ppf "Codata(?)"
     | Record (_, _, _) -> fprintf ppf "Record(?)"
+    | SelfRecord _ -> fprintf ppf "SelfRecord(?)"
     | Refute (_, _) -> fprintf ppf "Refute(?)"
     | Hole _ -> fprintf ppf "Hole"
     | Realize x -> fprintf ppf "Realize %a" check x

lib/core/raw.ml

@@ -129,6 +129,7 @@ module rec Make : functor (I : Indices) -> sig
     | Data : (Constr.t, 'a dataconstr located) Abwd.t -> 'a check
     | Codata : (Field.wrapped, 'a codatafield) Abwd.t -> 'a check
     | Record : ('a, 'c, 'ac) Namevec.t located * ('ac, 'd, 'acd) tel * opacity -> 'a check
+    | SelfRecord : (Field.wrapped, 'a codatafield) Abwd.t -> 'a check
     | Refute : 'a synth located list * [ `Explicit | `Implicit ] -> 'a check
     | Hole : {
         scope : 'a I.scope;
@@ -302,6 +303,8 @@ functor
       | Codata : (Field.wrapped, 'a codatafield) Abwd.t -> 'a check
       (* A record type binds its "self" variable namelessly, exposing it to the user by additional variables that are bound locally to its fields.  This can't be "cubeified" as easily, so we have the user specify a list of ordinary variables to be its boundary.  Thus, in practice below 'c must be a number of faces associated to a dimension, but the parser doesn't know the dimension, so it can't ensure that.  The unnamed internal variable is included as the last one. *)
       | Record : ('a, 'c, 'ac) Namevec.t located * ('ac, 'd, 'acd) tel * opacity -> 'a check
+      (* There's also a notation for record types that uses self variables like codata. *)
+      | SelfRecord : (Field.wrapped, 'a codatafield) Abwd.t -> 'a check
       (* Empty match against the first one of the arguments belonging to an empty type. *)
       | Refute : 'a synth located list * [ `Explicit | `Implicit ] -> 'a check
       (* A hole must store the entire "state" from when it was entered, so that the user can later go back and fill it with a term that would have been valid in its original position.  This includes the variables in lexical scope, which are available only during parsing, so we store them here at that point.  During typechecking, when the actual metavariable is created, we save the lexical scope along with its other context and type data.  A hole also stores its source location so that proofgeneral can create an overlay at that place, and the notation tightnesses of the hole location. *)
@@ -528,6 +531,12 @@ module Resolve (R : Resolver) = struct
                (fun (R.T1.Codatafield (x, fld)) ->
                  R.T2.Codatafield (R.rename ctx x, check (R.snoc ctx x) fld))
                fields)
+      | SelfRecord fields ->
+          SelfRecord
+            (Abwd.map
+               (fun (R.T1.Codatafield (x, fld)) ->
+                 R.T2.Codatafield (R.rename ctx x, check (R.snoc ctx x) fld))
+               fields)
       | Record (xs, fields, opaq) ->
           let (Bplus ac2) = R.T2.bplus (R.T1.Namevec.length xs.value) in
           let xs2 = renames ctx xs.value ac2 in

lib/core/reporter.ml

@@ -1076,6 +1076,12 @@ let extra_field_in_struct : type s et. (s, et) eta -> string * string list -> Co
   | Eta -> Extra_field_in_tuple (Some (fst fld))
   | Noeta -> Extra_method_in_comatch fld
 
+let duplicate_field_in_type : type s et i. (s, et) eta -> i Field.t -> Code.t =
+ fun eta fld ->
+  match eta with
+  | Eta -> Duplicate_field_in_record fld
+  | Noeta -> Duplicate_method_in_codata fld
+
 let duplicate_field_in_struct : type s et. (s, et) eta -> string * string list -> Code.t =
  fun eta fld ->
   match eta with

lib/parser/builtins.ml

@@ -1960,6 +1960,37 @@ let rec codata_fields bar_ok =
              (terms [ (Op "|", Lazy (lazy (codata_fields false))); (RBracket, Done_closed codata) ]));
     }
 
+let process_codata_field : type n lt ls rt rs lt' ls' rt' rs' et.
+    (potential, et) eta ->
+    (Field.wrapped, n Raw.codatafield) Abwd.t ->
+    (string option, n) Bwv.t ->
+    (lt, ls, rt, rs) parse located ->
+    (lt', ls', rt', rs') parse located ->
+    Field.wrapped * n Raw.codatafield =
+ fun eta flds ctx tm ty ->
+  match tm.value with
+  | App
+      { fn = { value = x; loc = xloc }; arg = { value = Field (fstr, fdstr, _); loc = fldloc }; _ }
+    -> (
+      with_loc tm.loc @@ fun () ->
+      if not (Lexer.valid_field fstr) then fatal ?loc:fldloc (Invalid_field fstr);
+      let x =
+        match x with
+        | Ident ([ x ], _) when Lexer.valid_var x -> Some x
+        | Placeholder _ -> None
+        | Ident (x, _) -> fatal ?loc:xloc (Invalid_variable x)
+        | _ -> fatal ?loc:xloc Parse_error in
+      match dim_of_string (String.concat "" fdstr) with
+      | Some (Any fdim) -> (
+          let fld = Field.intern fstr fdim in
+          match Abwd.find_opt (Field.Wrap fld) flds with
+          | Some _ -> fatal ?loc:fldloc (duplicate_field_in_type eta fld)
+          | None ->
+              let ty = process (Bwv.snoc ctx x) ty in
+              (Field.Wrap fld, Raw.Codatafield (x, ty)))
+      | None -> fatal (Invalid_field (String.concat "." ("" :: fstr :: fdstr))))
+  | _ -> fatal ?loc:tm.loc Parse_error
+
 let rec process_codata : type n.
     (Field.wrapped, n Raw.codatafield) Abwd.t ->
     (string option, n) Bwv.t ->
@@ -1969,34 +2000,8 @@ let rec process_codata : type n.
  fun flds ctx obs loc ->
   match obs with
   | [ Token (RBracket, _) ] -> { value = Raw.Codata flds; loc }
-  | Token (Op "|", _) :: Term tm :: Token (Colon, _) :: Term ty :: obs -> (
-      match tm.value with
-      | App
-          {
-            fn = { value = x; loc = xloc };
-            arg = { value = Field (fstr, fdstr, _); loc = fldloc };
-            _;
-          } -> (
-          with_loc tm.loc @@ fun () ->
-          if not (Lexer.valid_field fstr) then fatal ?loc:fldloc (Invalid_field fstr);
-          let x =
-            match x with
-            | Ident ([ x ], _) when Lexer.valid_var x -> Some x
-            | Placeholder _ -> None
-            | Ident (x, _) -> fatal ?loc:xloc (Invalid_variable x)
-            | _ -> fatal ?loc:xloc Parse_error in
-          match dim_of_string (String.concat "" fdstr) with
-          | Some (Any fdim) -> (
-              let fld = Field.intern fstr fdim in
-              match Abwd.find_opt (Field.Wrap fld) flds with
-              | Some _ -> fatal ?loc:fldloc (Duplicate_method_in_codata fld)
-              | None ->
-                  let ty = process (Bwv.snoc ctx x) ty in
-                  process_codata
-                    (Abwd.add (Field.Wrap fld) (Raw.Codatafield (x, ty)) flds)
-                    ctx obs loc)
-          | None -> fatal (Invalid_field (String.concat "." ("" :: fstr :: fdstr))))
-      | _ -> fatal ?loc:tm.loc Parse_error)
+  | Token (Op "|", _) :: Term tm :: Token (Colon, _) :: Term ty :: obs ->
+      process_codata (Snoc (flds, process_codata_field Noeta flds ctx tm ty)) ctx obs loc
   | _ -> invalid "codata 1"
 
 let rec pp_codata_fields first prews accum obs : document * Whitespace.t list =
@@ -2104,8 +2109,23 @@ let rec process_tel : type a.
         let (Any_tel tel) = process_tel ctx (StringSet.add name seen) obs in
         Any_tel (Ext (Some name, ty, tel)))
       else fatal ?loc (Invalid_field name)
+  | Term { loc; _ } :: Token (Colon, _) :: Term _ :: _ -> fatal ?loc Parse_error
   | _ -> invalid "record"
 
+let rec process_self_record : type n.
+    (Field.wrapped, n Raw.codatafield) Abwd.t ->
+    (string option, n) Bwv.t ->
+    observation list ->
+    Asai.Range.t option ->
+    n check located =
+ fun flds ctx obs loc ->
+  match obs with
+  | [ Token (RParen, _) ] -> { value = Raw.SelfRecord flds; loc }
+  | Token (Op ",", _) :: obs -> process_self_record flds ctx obs loc
+  | Term tm :: Token (Colon, _) :: Term ty :: obs ->
+      process_self_record (Snoc (flds, process_codata_field Eta flds ctx tm ty)) ctx obs loc
+  | _ -> invalid "self record"
+
 let process_record ctx obs loc =
   let opacity, obs =
     match obs with
@@ -2137,10 +2157,12 @@ let process_record ctx obs loc =
       let ctx = Bwv.append ac ctx vars in
       let (Any_tel tel) = process_tel ctx StringSet.empty obs in
       Range.locate (Raw.Record (locate_opt x.loc (namevec_of_vec ac vars), tel, opacity)) loc
+  | Token (LParen, _) :: (Term { value = App _; _ } :: _ as obs) ->
+      process_self_record Emp ctx obs loc
   | Token (LParen, _) :: obs ->
       let ctx = Bwv.snoc ctx None in
       let (Any_tel tel) = process_tel ctx StringSet.empty obs in
-      { value = Record ({ value = [ None ]; loc }, tel, opacity); loc }
+      Range.locate (Raw.Record ({ value = [ None ]; loc }, tel, opacity)) loc
   | _ -> invalid "record"
 
 let rec pp_record_fields prews accum obs =