Initial models 2: the recquel

.github/workflows/web-demos.yml

@@ -65,39 +65,39 @@ jobs:
           cp examples/index.html examples/style.css _build/web/
           cp -r examples/sync-demo/dist _build/web/sync
 
-      - name: Deploy PR preview to Netlify
-        id: deploy-preview
-        if: github.event_name == 'pull_request' && env.NETLIFY_AUTH_TOKEN != '' && env.NETLIFY_SITE_ID != ''
-        run: |
-          npx --yes netlify-cli@latest deploy \
-            --auth "$NETLIFY_AUTH_TOKEN" \
-            --site "$NETLIFY_SITE_ID" \
-            --dir _build/web \
-            --no-build \
-            --alias "pr-${{ github.event.pull_request.number }}" \
-            --message "PR #${{ github.event.pull_request.number }} web demos" \
-            --json > netlify-deploy.json
+      # - name: Deploy PR preview to Netlify
+      #   id: deploy-preview
+      #   if: github.event_name == 'pull_request' && env.NETLIFY_AUTH_TOKEN != '' && env.NETLIFY_SITE_ID != ''
+      #   run: |
+      #     npx --yes netlify-cli@latest deploy \
+      #       --auth "$NETLIFY_AUTH_TOKEN" \
+      #       --site "$NETLIFY_SITE_ID" \
+      #       --dir _build/web \
+      #       --no-build \
+      #       --alias "pr-${{ github.event.pull_request.number }}" \
+      #       --message "PR #${{ github.event.pull_request.number }} web demos" \
+      #       --json > netlify-deploy.json
 
-          cat netlify-deploy.json
-          deploy_url=$(node -e "const d = require('./netlify-deploy.json'); console.log(d.deploy_ssl_url || d.ssl_url || d.deploy_url || d.url)")
-          echo "deploy-url=$deploy_url" >> "$GITHUB_OUTPUT"
+      #     cat netlify-deploy.json
+      #     deploy_url=$(node -e "const d = require('./netlify-deploy.json'); console.log(d.deploy_ssl_url || d.ssl_url || d.deploy_url || d.url)")
+      #     echo "deploy-url=$deploy_url" >> "$GITHUB_OUTPUT"
 
-      - name: Comment with deploy preview URL
-        if: github.event_name == 'pull_request' && steps.deploy-preview.outputs.deploy-url != ''
-        uses: actions/github-script@v8
-        with:
-          script: |
-            const marker = '<!-- coln-web-demos-deploy-preview -->'
-            const body = `${marker}\nWeb demo preview: ${{ steps.deploy-preview.outputs.deploy-url }}`
-            const { owner, repo } = context.repo
-            const issue_number = context.issue.number
-            const comments = await github.rest.issues.listComments({ owner, repo, issue_number, per_page: 100 })
-            const existing = comments.data.find(comment => comment.body?.includes(marker))
-            if (existing) {
-              await github.rest.issues.updateComment({ owner, repo, comment_id: existing.id, body })
-            } else {
-              await github.rest.issues.createComment({ owner, repo, issue_number, body })
-            }
+      # - name: Comment with deploy preview URL
+      #   if: github.event_name == 'pull_request' && steps.deploy-preview.outputs.deploy-url != ''
+      #   uses: actions/github-script@v8
+      #   with:
+      #     script: |
+      #       const marker = '<!-- coln-web-demos-deploy-preview -->'
+      #       const body = `${marker}\nWeb demo preview: ${{ steps.deploy-preview.outputs.deploy-url }}`
+      #       const { owner, repo } = context.repo
+      #       const issue_number = context.issue.number
+      #       const comments = await github.rest.issues.listComments({ owner, repo, issue_number, per_page: 100 })
+      #       const existing = comments.data.find(comment => comment.body?.includes(marker))
+      #       if (existing) {
+      #         await github.rest.issues.updateComment({ owner, repo, comment_id: existing.id, body })
+      #       } else {
+      #         await github.rest.issues.createComment({ owner, repo, issue_number, body })
+      #       }
 
       - name: Deploy main to Netlify production
         if: github.event_name == 'push' && env.NETLIFY_AUTH_TOKEN != '' && env.NETLIFY_SITE_ID != ''

manual/trees/0001.tree

@@ -2,9 +2,11 @@
 
 \p{Coln is a database with an expressive language for schemas, queries, and migrations. This document forms the manual for Coln.}
 
-\transclude{002H}
-\transclude{0002}
-\transclude{000K}
-\transclude{000L}
-\transclude{000M}
-\transclude{0003}
+\ol{
+  \li{[[002H]]}
+  \li{[[0002]]}
+  \li{[[000K]]}
+  \li{[[000L]]}
+  \li{[[000M]]}
+  \li{[[0003]]}
+}

manual/trees/0002.tree

@@ -72,8 +72,4 @@
 
 \transclude{000B}
 
-\subtree[000I]{
-  \title{Organization}
-
-  \p{}
-}
+\transclude{000I}

manual/trees/000I.tree

@@ -0,0 +1,3 @@
+\title{Organization}
+
+\p{}

manual/trees/002K.tree

@@ -0,0 +1 @@
+\title{Developer documentation}

packages/coln-compiler/coln-compiler.cabal

@@ -30,19 +30,24 @@ library
     Coln.Core.Syntax
     Coln.Core.Value
     Coln.Diagnostics
+    Coln.Elaborator.Coercion
     Coln.Elaborator.Debug
     Coln.Elaborator.Diagnostics
     Coln.Elaborator.Environment
     Coln.Elaborator.Judgment
     Coln.Elaborator.Rules.Builtin
     Coln.Elaborator.Rules.Equality
     Coln.Elaborator.Rules.Function
+    Coln.Elaborator.Rules.Initial
+    Coln.Elaborator.Rules.Polarity
     Coln.Elaborator.Rules.Record
     Coln.Elaborator.Rules.Universe
     Coln.Elaborator.Rules.Variable
     Coln.Frontend.Diagnostics
     Coln.Frontend.Notation
     Coln.Frontend.Parser
+    Coln.Frontend.Parser.Expr
+    Coln.Frontend.Parser.Top
     Coln.Report
 
   hs-source-dirs: src

packages/coln-compiler/src/Coln/Backend/Lower.hs

@@ -73,6 +73,7 @@ instance Lower (V.El N) Term where
   lower :: CtxLen -> V.El N -> Term
   lower n = \case
     V.Neu ne -> lower n ne
+    V.InitNeu _ -> panic "can't lower init yet"
     V.Code _ -> panic "non set-level term"
     V.Lam _ _ -> panic "non set-level term"
     V.Cons ds -> Cons (lower n <$> ds)
@@ -99,6 +100,7 @@ separate n = \case
       let (shapes, props) = unzip $ go rt.capture (toList rt.fieldTypes)
       Ty (Tuple (withHead rt.fieldTypes shapes)) (And (withHead rt.fieldTypes props))
     Nothing -> panic "lowering neutral type"
+  V.InitDecode _ -> panic "can't lower init yet"
   V.Function _ -> panic "lowering non-set-level type: Function"
   V.Eq et -> \_ -> Ty Unit (Equal (lower n et.lhs) (lower n et.rhs))
   V.BuiltinTy t -> \_ -> Ty (BuiltinTy t) PTrue

packages/coln-compiler/src/Coln/Backend/TypeScript/Generate.hs

@@ -117,6 +117,7 @@ genEntryModule imports a ev = go 0 a ev
           case V.ebind V.decode ev' of
             V.Become a -> TS.DTypeDef $ genTypeDef access n a
             V.Describe a -> TS.DInterface $ genInterface access n a
+            V.BecomeWith _ -> panic "can't lower becomewith yet"
     Just $ TS.Module imports (TS.Exported <$> definitions)
   go n (V.Function ft) ev' = do
     let v = V.local (FId n) ft.dom
@@ -172,6 +173,7 @@ argName _ (V.CloConst _) = panic "closures from the layout process should have a
 genEl :: Access -> TSCtxShape -> V.El N -> TS.El
 genEl access cs = \case
   V.Neu n -> genSp cs n.spine $ genHead access cs n.head
+  V.InitNeu _ -> panic "can't lower init yet"
   V.Code a -> genTyVal access cs a
   V.Lam dom clo -> do
     let v = V.local (FId cs.len) dom

packages/coln-compiler/src/Coln/Core/Conversion.hs

@@ -62,6 +62,9 @@ instance DefEq (V.Ty N) where
     V.Decode n -> case a' of
       V.Decode n' -> defEq cs n n'
       _ -> throwUnequalTys cs a a' Nothing
+    V.InitDecode n -> case a' of
+      V.InitDecode n' -> defEq cs n n'
+      _ -> throwUnequalTys cs a a' Nothing
     V.Function f -> case a' of
       V.Function f' -> do
         unless (f.variant == f'.variant) $
@@ -123,6 +126,9 @@ instance DefEq V.DecodedNeutral where
 instance DefEq V.Neutral where
   defEq cs n n' = defEq cs (V.toBare n) (V.toBare n')
 
+instance DefEq V.InitNeutral where
+  defEq cs n n' = defEq cs (V.fullNeu n) (V.fullNeu n')
+
 canon :: V.El N -> V.El N
 canon v@(V.Neu n) = case V.behavior n.ty of
   V.LikeRecord _ -> V.Cons (V.unwrap n.expansion)
@@ -137,6 +143,9 @@ instance DefEq (V.El N) where
     V.Neu n -> case canon v' of
       V.Neu n' -> defEq cs n n'
       _ -> throwUnequalEls cs v v' Nothing
+    V.InitNeu n -> case canon v' of
+      V.InitNeu n' -> defEq cs n n'
+      _ -> throwUnequalEls cs v v' Nothing
     V.Code a -> case canon v' of
       V.Code a' -> defEq cs a a'
       _ -> throwUnequalEls cs v v' Nothing

packages/coln-compiler/src/Coln/Core/Evaluation.hs

@@ -43,6 +43,9 @@ instance Compile S.El V.El where
     S.Proj t x -> do
       let k = compile t
       \vs -> V.proj (k vs) x
+    S.Init t -> do
+      let k = compile t
+      \vs -> V.BecomeWith $ \n -> V.InitNeu (V.InitNeutral n (k vs) V.Id)
     S.Lit l -> \_ -> V.Lit l
     S.Is t -> do
       let k = compile t

packages/coln-compiler/src/Coln/Core/Globals.hs

@@ -17,6 +17,7 @@ data GlobalEntry = GlobalEntry
   { syn :: S.El D
   , val :: V.El N
   , ty :: V.Ty N
+  , mode :: Mode
   }
 
 data Globals = Globals

packages/coln-compiler/src/Coln/Core/Layout.hs

@@ -71,7 +71,7 @@ layout p sc a
         let a = V.EltOf (TableName sc.realm p) (fromList $ zip (toList sc.names) (toList sc.bound))
         (gt, M.code (M.fromVTy sc.len a))
       V.NoRules -> panic "cannot layout type with no rules"
-      V.LikeBuiltinTy _; V.LikeU _ -> panic "non-theory type"
+      V.LikeBuiltinTy _; V.LikeU _; V.LikeInductive _ -> panic "non-theory type"
   | (levelOf a).mlevel == Set = do
       let gt = Leaf (Fun (toList sc.names) (toList sc.ctx) (readb sc.len a))
       let v = V.tableLookup (TableName sc.realm p) (fromList $ zip (toList sc.names) (toList sc.bound)) a

packages/coln-compiler/src/Coln/Core/Memoed.hs

@@ -30,6 +30,7 @@ class Core el ty | el -> ty, ty -> el where
   lam :: (V.HasEvaluation c) => V.Locals -> ty N -> S.Abs el c -> el c
   cons :: (V.HasEvaluation c) => Dict (el c) -> el c
   proj :: el N -> Name -> el N
+  init :: ty N -> el D
   lit :: Literal -> el N
   is :: el N -> el D
   univ :: Universe -> ty N
@@ -55,6 +56,8 @@ instance Core El Ty where
       (V.epure $ V.Lam dom.val (V.CloConst body.val))
   cons d = M (S.Cons $ (.stx) <$> d) (V.epure $ V.Cons $ (.val) <$> d)
   proj x f = M (S.Proj x.stx f) (V.proj x.val f)
+  init a =
+    M (S.Init a.stx) (V.BecomeWith $ \n -> V.InitNeu (V.InitNeutral n a.val V.Id))
   lit l = M (S.Lit l) (V.Lit l)
   is x = M (S.Is x.stx) (V.Become x.val)
   univ u = M (S.U u) (V.U u)
@@ -90,11 +93,13 @@ instance (V.HasEvaluation c) => LevelOf (Ty c) where
     SDescriptive -> case ty.val of
       V.Describe ty' -> levelOf ty'
       V.Become ty' -> levelOf ty'
+      -- This is kind of a hack, but shouldn't appear in practice in any case
+      V.BecomeWith f -> levelOf (f $ V.BareNeutral (V.LocalVar (FId 0)) V.Id)
 
 instance Readback (Memoed a b c) (a c) where
   readb _ m = m.stx
 
-mkGlobal :: Name -> V.Ty N -> El D -> GlobalEntry
-mkGlobal n ty x = do
+mkGlobal :: Name -> V.Ty N -> El D -> Mode -> GlobalEntry
+mkGlobal n ty x m = do
   let neu = V.reflect (V.GlobalVar n neu) V.Id ty (Just x.val)
-  GlobalEntry x.stx neu ty
+  GlobalEntry x.stx neu ty m

packages/coln-compiler/src/Coln/Core/Params.hs

@@ -109,7 +109,11 @@ functionMLevelFor v1 v2 = case (v1, v2) of
   (Theory, _) -> pure TheoryTop
   (Top, _) -> Nothing
 
-data FunctionVariant = FunctionVariant {mlevel :: FunctionVariantMLevel, hlevel :: HLevel}
+data FunctionVariant = FunctionVariant
+  { mlevel :: FunctionVariantMLevel
+  , hlevel :: HLevel
+  , domainMode :: Mode
+  }
   deriving (Eq, Show)
 
 instance Pretty FunctionVariant where
@@ -183,3 +187,12 @@ data TableName = TableName {realm :: RealmId, path :: Path}
 
 instance DPretty TableName where
   dpretty tn = concatWith (surround dot) (dpretty <$> toList tn.path)
+
+-- Mode
+--------------------------------------------------------------------------------
+
+data Mode = Inductive | Conjunctive
+  deriving (Show, Eq, Ord)
+
+instance DPretty Mode where
+  dpretty = pretty . show

packages/coln-compiler/src/Coln/Core/Print.hs

@@ -55,6 +55,7 @@ instance ToNotation (El e) where
       N.Tuple [field y t | (y, t) <- toList d] ()
      where
       field y t = N.Infix (N.Ident y ()) (N.Keyword ":=" ()) (toNotation xs t)
+    Init t -> N.Juxt (N.Keyword "init" ()) (toNotation xs t)
     Lit (LitInt i) -> N.Int i ()
     Lit (LitString s) -> N.String s ()
     Is t -> toNotation xs t -- invisible
@@ -102,6 +103,7 @@ instance ToNotation TypeBehavior where
     LikeFunction ft -> toNotation xs (Function ft)
     LikeRecord rt -> toNotation xs (Record rt)
     LikeBuiltinTy bt -> toNotation xs (BuiltinTy bt)
+    LikeInductive t -> toNotation xs t
     NoRules -> N.Keyword "NoRules" ()
 
 toNotationTele :: [Name] -> [Ty N] -> [N.Ntn0]

packages/coln-compiler/src/Coln/Core/Readback.hs

@@ -36,6 +36,8 @@ instance Readback (V.Description V.El) (S.El D) where
   readb n = \case
     V.Describe v -> readb n v
     V.Become v -> S.Is (readb n v)
+    V.BecomeWith f ->
+      S.Is (readb (n + 1) (f (V.BareNeutral (V.LocalVar (FId n)) V.Id)))
 
 readbClo :: (Readback (V.Evaluation a c) (b c)) => CtxLen -> V.Ty N -> V.Clo a c -> S.Abs b c
 readbClo n dom = \case
@@ -45,6 +47,7 @@ readbClo n dom = \case
 instance (V.HasEvaluation c) => Readback (V.El c) (S.El c) where
   readb n = \case
     V.Neu ne -> readb n ne.spine $ readb n ne.head
+    V.InitNeu ne -> readb n ne.spine $ readb n ne.name
     V.Code a -> S.Code (readb n a)
     V.Lam dom body -> S.Lam (readb n dom) $ case V.scase @c of
       SNominative -> readbClo n dom body
@@ -92,6 +95,7 @@ instance (V.HasEvaluation c) => Readback (V.Ty c) (S.Ty c) where
   readb n = \case
     V.U u -> S.U u
     V.Decode ne -> S.Decode $ readb n ne.spine $ readb n ne.head
+    V.InitDecode ne -> S.Decode $ readb n ne.spine $ readb n ne.name
     V.Function f -> S.Function $ readb n f
     V.Record r -> S.Record $ readb n r
     V.Eq eq -> S.Eq $ readb n eq
@@ -103,5 +107,6 @@ instance Readback V.TypeBehavior S.TypeBehavior where
     V.LikeU u -> S.LikeU u
     V.LikeRecord rt -> S.LikeRecord $ readb n rt
     V.LikeFunction ft -> S.LikeFunction $ readb n ft
+    V.LikeInductive ne -> S.LikeInductive $ readb n ne.spine $ readb n ne.name
     V.LikeBuiltinTy bt -> S.LikeBuiltinTy bt
     V.NoRules -> S.NoRules

packages/coln-compiler/src/Coln/Core/Syntax.hs

@@ -23,6 +23,7 @@ data El :: Case -> Type where
   App :: El N -> El N -> El N
   Cons :: Dict (El c) -> El c
   Proj :: El N -> Name -> El N
+  Init :: Ty N -> El D
   Lit :: Literal -> El N
   Is :: El N -> El D
   Lookup :: TableName -> Dict (El N) -> Ty N -> El N
@@ -58,5 +59,6 @@ data TypeBehavior
   = LikeU Universe
   | LikeFunction (FunctionType Ty)
   | LikeRecord (RecordType Ty)
+  | LikeInductive (El N)
   | LikeBuiltinTy BuiltinTy
   | NoRules