Anonymous Records

.github/workflows/proofs/formatting.txt

@@ -1 +1 @@
-e22453ae22870523f79984c00371b3514967b63f230dfee2297964f1b6c1b251 ab5370655049c955d122d644eb26598258e7998bf91ebc7433f068470a966a9e pass
+6fa984cffdeb66869d9e53ccf73166a0d3cbaa2c1e07ded9780652f9c0002d1b ab5370655049c955d122d644eb26598258e7998bf91ebc7433f068470a966a9e pass

.github/workflows/proofs/tests.txt

@@ -1 +1 @@
-8309e64b8a084106fe325f756e8e5e7abd81cea1f33b20f335cfb06a83d80eb9 36894b8d3d19e10c74bdc233d752feca155998462033d20e6770eba9f82a10a0 pass
+4338a8b7d94500696756f67931282126fc0dd23b8c838efa0599781226d03ce9 36894b8d3d19e10c74bdc233d752feca155998462033d20e6770eba9f82a10a0 pass

.github/workflows/proofs/transcripts.txt

@@ -1 +1 @@
-8667add51840b308bc23bf95a9c9c0032ff5486ec285e3d3de38970385912c67 beb4a304f24dcbdf3db627887d7c02e22209258fc25b84ad944267279c7278aa pass
+4497d4885947f64a10a617e786b65a989442e48af7e92cdbf2f1ef4eee8daf76 beb4a304f24dcbdf3db627887d7c02e22209258fc25b84ad944267279c7278aa pass

codebase2/codebase-sqlite-hashing-v2/src/Unison/Hashing/V2/Convert2.hs

@@ -84,6 +84,10 @@ v2ToH2Type' mkReference = ABT.transform convertF
       V2.Type.Effects a -> H2.TypeEffects a
       V2.Type.Forall a -> H2.TypeForall a
       V2.Type.IntroOuter a -> H2.TypeIntroOuter a
+      V2.Type.Record fb fields -> H2.TypeRecord (convertFB fb) fields
+    convertFB = \case
+      V2.Type.AllowExtraFields -> H2.AllowExtraFields
+      V2.Type.RequireExactFields -> H2.RequireExactFields
 
 convertKind :: V2.Kind -> H2.Kind
 convertKind = \case
@@ -179,6 +183,7 @@ v2ToH2Term = ABT.transform convertF
       V2.Term.Char c -> H2.TermChar c
       V2.Term.Ref r -> H2.TermRef (v2ToH2Reference r)
       V2.Term.Constructor r cid -> H2.TermConstructor (v2ToH2Reference r) cid
+      V2.Term.Record fields -> H2.TermRecord fields
       V2.Term.Request r cid -> H2.TermRequest (v2ToH2Reference r) cid
       V2.Term.Handle a b -> H2.TermHandle a b
       V2.Term.App a b -> H2.TermApp a b
@@ -210,6 +215,7 @@ v2ToH2Term = ABT.transform convertF
       V2.Term.PChar c -> H2.PatternChar () c
       V2.Term.PBytes b -> H2.PatternBytes () b
       V2.Term.PConstructor r cid ps -> H2.PatternConstructor () (v2ToH2Reference r) cid (convertPattern <$> ps)
+      V2.Term.PRecord fieldPats -> H2.PatternRecord () (convertPattern <$> fieldPats)
       V2.Term.PAs pat -> H2.PatternAs () (convertPattern pat)
       V2.Term.PEffectPure pat -> H2.PatternEffectPure () (convertPattern pat)
       V2.Term.PEffectBind r conId pats pat -> H2.PatternEffectBind () (v2ToH2Reference r) conId (convertPattern <$> pats) (convertPattern pat)

codebase2/codebase-sqlite/U/Codebase/Sqlite/Queries.hs

@@ -465,7 +465,7 @@ type TextPathSegments = [Text]
 -- * main squeeze
 
 currentSchemaVersion :: SchemaVersion
-currentSchemaVersion = 26
+currentSchemaVersion = 27
 
 runCreateSql :: Transaction ()
 runCreateSql =
@@ -2738,6 +2738,7 @@ c2sDecl saveText saveDefn (C.Decl.DataDeclaration dt m b cts) = do
       C.Type.Effects es -> pure $ C.Type.Effects es
       C.Type.Forall a -> pure $ C.Type.Forall a
       C.Type.IntroOuter a -> pure $ C.Type.IntroOuter a
+      C.Type.Record fb fields -> pure $ C.Type.Record fb fields
     done :: (S.Decl.Decl Symbol, (Seq Text, Seq Hash)) -> m (LocalIds' t d, S.Decl.Decl Symbol)
     done (decl, (localTextValues, localDefnValues)) = do
       textIds <- traverse saveText localTextValues
@@ -2771,6 +2772,7 @@ c2xTerm saveText saveDefn tm tp =
         C.Term.Constructor
           <$> bitraverse lookupText lookupDefn typeRef
           <*> pure cid
+      C.Term.Record fields -> pure $ C.Term.Record fields
       C.Term.Request typeRef cid ->
         C.Term.Request <$> bitraverse lookupText lookupDefn typeRef <*> pure cid
       C.Term.Handle a a2 -> pure $ C.Term.Handle a a2
@@ -2806,6 +2808,7 @@ c2xTerm saveText saveDefn tm tp =
       C.Type.Effects es -> pure $ C.Type.Effects es
       C.Type.Forall a -> pure $ C.Type.Forall a
       C.Type.IntroOuter a -> pure $ C.Type.IntroOuter a
+      C.Type.Record fb fields -> pure $ C.Type.Record fb fields
     goCase ::
       forall m w s a.
       ( MonadState s m,
@@ -2842,6 +2845,7 @@ c2xTerm saveText saveDefn tm tp =
       C.Term.PChar c -> pure $ C.Term.PChar c
       C.Term.PBytes b -> pure $ C.Term.PBytes b
       C.Term.PConstructor r i ps -> C.Term.PConstructor <$> bitraverse lookupText lookupDefn r <*> pure i <*> traverse goPat ps
+      C.Term.PRecord fields -> C.Term.PRecord <$> traverse goPat fields
       C.Term.PAs p -> C.Term.PAs <$> goPat p
       C.Term.PEffectPure p -> C.Term.PEffectPure <$> goPat p
       C.Term.PEffectBind r i bindings k -> C.Term.PEffectBind <$> bitraverse lookupText lookupDefn r <*> pure i <*> traverse goPat bindings <*> goPat k

codebase2/codebase-sqlite/U/Codebase/Sqlite/Serialization.hs

@@ -58,6 +58,7 @@ import Data.Bytes.Put (MonadPut, putByteString, putWord8)
 import Data.Bytes.Serial (SerialEndian (serializeBE), deserialize, deserializeBE, serialize)
 import Data.Bytes.VarInt (VarInt (VarInt), unVarInt)
 import Data.List (elemIndex)
+import Data.Map qualified as Map
 import Data.Set qualified as Set
 import Data.Vector (Vector)
 import U.Codebase.Decl (Modifier)
@@ -281,6 +282,8 @@ putSingleTerm t = putABT putSymbol putUnit putF t
         putWord8 20 *> putReferent' putRecursiveReference putReference r
       Term.TypeLink r ->
         putWord8 21 *> putReference r
+      Term.Record fields ->
+        putWord8 22 *> putFoldable (\(name, val) -> putText name *> putChild val) (Map.toList fields)
     putMatchCase :: (MonadPut m) => (a -> m ()) -> Term.MatchCase LocalTextId TermFormat.TypeRef a -> m ()
     putMatchCase putChild (Term.MatchCase pat guard body) =
       putPattern pat *> putMaybe putChild guard *> putChild body
@@ -317,6 +320,10 @@ putSingleTerm t = putABT putSymbol putUnit putF t
       Term.PBytes b ->
         let bs = Bytes.toByteString b
          in putWord8 14 *> putVarInt (BS.length bs) *> putByteString bs
+      Term.PRecord fields ->
+        putWord8 15
+          *> putFoldable (\(name, pat) -> putText name *> putPattern pat) (Map.toList fields)
+
     putSeqOp :: (MonadPut m) => Term.SeqOp -> m ()
     putSeqOp Term.PCons = putWord8 0
     putSeqOp Term.PSnoc = putWord8 1
@@ -368,6 +375,10 @@ getSingleTerm = getABT getSymbol getUnit getF
         19 -> Term.Char <$> getChar
         20 -> Term.TermLink <$> getReferent
         21 -> Term.TypeLink <$> getReference
+        22 ->
+          getList
+            ((,) <$> getText <*> getChild)
+            <&> Term.Record . Map.fromList
         tag -> unknownTag "getSingleTerm" tag
       where
         getReferent :: (MonadGet m) => m (Referent' TermFormat.TermRef TermFormat.TypeRef)
@@ -406,6 +417,7 @@ getSingleTerm = getABT getSymbol getUnit getF
               n <- getVarInt
               bs <- getByteString n
               pure $ Term.PBytes (Bytes.fromByteString bs)
+            15 -> Term.PRecord . Map.fromList <$> (getList ((,) <$> getText <*> getPattern))
             x -> unknownTag "Pattern" x
           where
             getSeqOp :: (MonadGet m) => m Term.SeqOp
@@ -452,6 +464,7 @@ getType getReference = getABT getSymbol getUnit go
         5 -> Type.Effects <$> getList getChild
         6 -> Type.Forall <$> getChild
         7 -> Type.IntroOuter <$> getChild
+        8 -> Type.Record <$> getEnum @Type.FieldBehavior <*> (Map.fromList <$> getList (getPair getText getChild))
         tag -> unknownTag "getType" tag
     getKind :: (MonadGet m) => m Kind
     getKind =
@@ -1128,6 +1141,7 @@ putType putReference putVar = putABT putVar putUnit go
       Type.Effects es -> putWord8 5 *> putFoldable putChild es
       Type.Forall body -> putWord8 6 *> putChild body
       Type.IntroOuter body -> putWord8 7 *> putChild body
+      Type.Record fb fields -> putWord8 8 *> putEnum @Type.FieldBehavior fb *> putFoldable (\(l, t) -> putText l *> putChild t) (Map.toAscList fields)
     putKind :: (MonadPut m) => Kind -> m ()
     putKind k = case k of
       Kind.Star -> putWord8 0
@@ -1154,3 +1168,9 @@ getMaybe getA =
 unknownTag :: (MonadGet m, Show a) => String -> a -> m x
 unknownTag msg tag =
   fail $ "unknown tag " ++ show tag ++ " while deserializing: " ++ msg
+
+putEnum :: forall e m. (MonadPut m, Enum e) => e -> m ()
+putEnum e = putVarInt (fromEnum e)
+
+getEnum :: forall e m. (MonadGet m, Enum e) => m e
+getEnum = toEnum <$> getVarInt

codebase2/codebase/U/Codebase/Decl.hs

@@ -145,3 +145,4 @@ unhashComponent componentHash refToVar m =
             Type.Effects as -> ABT.tm () $ Type.Effects as
             Type.Forall a -> ABT.tm () $ Type.Forall a
             Type.IntroOuter a -> ABT.tm () $ Type.IntroOuter a
+            Type.Record fb fields -> ABT.tm () $ Type.Record fb fields

codebase2/codebase/U/Codebase/Term.hs

@@ -65,6 +65,7 @@ data F' text termRef typeRef termLink typeLink vt a
   | -- First argument identifies the data type,
     -- second argument identifies the constructor
     Constructor typeRef ConstructorId
+  | Record (Map Text {- field name -} a {- field value -})
   | Request typeRef ConstructorId
   | Handle a a
   | App a a
@@ -109,6 +110,7 @@ data Pattern t r
   | PChar !Char
   | PBytes !Bytes
   | PConstructor !r !ConstructorId [Pattern t r]
+  | PRecord (Map Text (Pattern t r))
   | PAs (Pattern t r)
   | PEffectPure (Pattern t r)
   | PEffectBind !r !ConstructorId [Pattern t r] (Pattern t r)
@@ -189,6 +191,7 @@ extraMapM ftext ftermRef ftypeRef ftermLink ftypeLink fvt = go'
       Char c -> pure $ Char c
       Ref r -> Ref <$> ftermRef r
       Constructor r cid -> Constructor <$> (ftypeRef r) <*> pure cid
+      Record fields -> pure $ Record fields
       Request r cid -> Request <$> ftypeRef r <*> pure cid
       Handle e h -> pure $ Handle e h
       App f a -> pure $ App f a
@@ -224,6 +227,7 @@ rmapPatternM ft fr = go
       PChar c -> pure $ PChar c
       PBytes b -> pure $ PBytes b
       PConstructor r i ps -> PConstructor <$> fr r <*> pure i <*> (traverse go ps)
+      PRecord fields -> PRecord <$> (traverse go fields)
       PAs p -> PAs <$> go p
       PEffectPure p -> PEffectPure <$> go p
       PEffectBind r i ps p -> PEffectBind <$> fr r <*> pure i <*> traverse go ps <*> go p
@@ -332,6 +336,7 @@ unhashComponent componentHash refToVar m =
             Text t -> ABT.tm () $ Text t
             Char c -> ABT.tm () $ Char c
             Constructor typeRef conId -> ABT.tm () $ Constructor typeRef conId
+            Record fields -> ABT.tm () $ Record fields
             Request typeRef conId -> ABT.tm () $ Request typeRef conId
             Handle e h -> ABT.tm () $ Handle e h
             App f a -> ABT.tm () $ App f a

codebase2/codebase/U/Codebase/Type.hs

@@ -16,6 +16,17 @@ type FT = F' Reference
 -- | For potentially recursive types, like those in DataDeclaration
 type FD = F' (Reference' Text (Maybe Hash))
 
+-- | Whether the record type unifies with types that have _extra_ fields.
+-- E.g. subtype (Record _ {a: Int, b: Nat}) (Record AllowExtraFields {a: Int})
+--   will succeed, since the former has all the required fields, and extra fields are allowed,
+--   but:
+--   subtype (Record _ {a: Int, b: Nat}) (Record RequireExactFields {a: Int})
+-- fails.
+data FieldBehavior
+  = AllowExtraFields
+  | RequireExactFields
+  deriving (Eq, Ord, Show, Enum, Bounded)
+
 data F' r a
   = Ref r
   | Arrow a a
@@ -27,6 +38,7 @@ data F' r a
   | IntroOuter a -- binder like ∀, used to introduce variables that are
   -- bound by outer type signatures, to support scoped type
   -- variables
+  | Record FieldBehavior (Map Text a)
   deriving (Foldable, Functor, Eq, Ord, Show, Traversable)
 
 -- | Non-recursive type

lib/unison-pretty-printer/src/Unison/Util/ColorText.hs

@@ -201,3 +201,6 @@ defaultColors = \case
   ST.Parenthesis -> Nothing
   ST.DocDelimiter -> Just Green
   ST.DocKeyword -> Just HiCyan
+  ST.RecordFieldName {} -> Just HiCyan
+  ST.RecordFieldValueColon -> Just HiPurple
+  ST.RecordExtraFields -> Just HiPurple

lib/unison-pretty-printer/src/Unison/Util/SyntaxText.hs

@@ -51,6 +51,9 @@ data Element r
   | DocDelimiter
   | -- the 'source' in @source{…}, etc
     DocKeyword
+  | RecordFieldName Text
+  | RecordFieldValueColon
+  | RecordExtraFields
   deriving (Eq, Ord, Show, Functor)
 
 syntax :: Element r -> SyntaxText' r -> SyntaxText' r

lib/unison-util-relation/src/Unison/Util/BiMap.hs

@@ -0,0 +1,105 @@
+module Unison.Util.BiMap
+  ( BiMap (..),
+    empty,
+    singleton,
+    fromList,
+    fromMap,
+    toList,
+    toMapL,
+    toMapR,
+    lookupL,
+    lookupR,
+    union,
+    difference,
+    insert,
+    deleteL,
+    deleteR,
+    keysSetL,
+    keysSetR,
+  )
+where
+
+import Data.Map qualified as Map
+import Data.Set (Set)
+import Data.Tuple (swap)
+
+-- | A bidirectional map between keys of type k and values of type v.
+data BiMap k v = BiMap
+  { forward :: Map.Map k v,
+    backward :: Map.Map v k
+  }
+  deriving (Eq, Ord, Show)
+
+-- | Combine two BiMaps. In case of key or value collisions, the entries from
+-- the second BiMap take precedence.
+instance (Ord k, Ord v) => Semigroup (BiMap k v) where
+  BiMap f1 b1 <> BiMap f2 b2 =
+    BiMap (Map.union f2 f1) (Map.union b2 b1)
+
+instance (Ord k, Ord v) => Monoid (BiMap k v) where
+  mempty = BiMap Map.empty Map.empty
+
+empty :: (Ord k, Ord v) => BiMap k v
+empty = mempty
+
+singleton :: k -> v -> BiMap k v
+singleton k v = BiMap (Map.singleton k v) (Map.singleton v k)
+
+fromList :: (Ord k, Ord v) => [(k, v)] -> BiMap k v
+fromList kvs =
+  let forward = Map.fromList kvs
+      backward = Map.fromList (swap <$> Map.toList forward)
+   in BiMap {forward, backward}
+
+fromMap :: (Ord k, Ord v) => Map.Map k v -> BiMap k v
+fromMap f =
+  let b = Map.fromList (swap <$> Map.toList f)
+   in BiMap f b
+
+toList :: BiMap k v -> [(k, v)]
+toList (BiMap f _) = Map.toList f
+
+toMapL :: BiMap k v -> Map.Map k v
+toMapL (BiMap f _) = f
+
+toMapR :: BiMap k v -> Map.Map v k
+toMapR (BiMap _ b) = b
+
+lookupL :: (Ord k) => k -> BiMap k v -> Maybe v
+lookupL k (BiMap f _) = Map.lookup k f
+
+lookupR :: (Ord v) => v -> BiMap k v -> Maybe k
+lookupR v (BiMap _ b) = Map.lookup v b
+
+union :: (Ord k, Ord v) => BiMap k v -> BiMap k v -> BiMap k v
+union = (<>)
+
+difference :: (Ord k, Ord v) => BiMap k v -> BiMap k v -> BiMap k v
+difference (BiMap f1 b1) (BiMap f2 b2) =
+  let f' = Map.difference f1 f2
+      b' = Map.difference b1 b2
+   in BiMap f' b'
+
+insert :: (Ord k, Ord v) => k -> v -> BiMap k v -> BiMap k v
+insert k v (BiMap f b) =
+  BiMap (Map.insert k v f) (Map.insert v k b)
+
+deleteL :: (Ord k, Ord v) => k -> BiMap k v -> BiMap k v
+deleteL k bm = case lookupL k bm of
+  Nothing -> bm
+  Just v ->
+    BiMap
+      (Map.delete k (forward bm))
+      (Map.delete v (backward bm))
+
+deleteR :: (Ord v, Ord k) => v -> BiMap k v -> BiMap k v
+deleteR v bm = flipped $ deleteL v (flipped bm)
+
+keysSetL :: BiMap k v -> Set k
+keysSetL (BiMap f _) = Map.keysSet f
+
+keysSetR :: BiMap k v -> Set v
+keysSetR (BiMap _ b) = Map.keysSet b
+
+flipped :: BiMap k v -> BiMap v k
+flipped (BiMap f b) = BiMap b f

lib/unison-util-relation/unison-util-relation.cabal

@@ -17,6 +17,7 @@ source-repository head
 
 library
   exposed-modules:
+      Unison.Util.BiMap
       Unison.Util.BiMultimap
       Unison.Util.Relation
       Unison.Util.Relation3