Open3

読者コミュニティ|TypeScriptの代数的部分型模型

ピン留めされたアイテム
PADAone🐕PADAone🐕

内容更新情報

このスタックでは「TypeScriptの代数的部分型模型」の更新情報を追記しています。最新の更新3つ以外は非表示にしています。

PADAone🐕PADAone🐕

2024-03-24

追加内容

  • 『圏論による模型』の章において、終対象・始対象、同型性、部分圏の埋め込みなどの話を追加しました
  • 『束論による模型(2)』の章において Elixirの集合論型の話を追加しました
  • 『集合論による模型』の章において型の濃度差による型挿入の話を追加しました

修正内容

また『集合論による模型』の章において指摘されていたオブジェクト型のハッセ図表現で考慮すべき要素が抜けていたところを修正しました。間違った内容を書いてしまいすみません🙇‍♂️
なお当該の指摘箇所を修正したことで「束ではないこと」の証拠がなくなってしまったので、章内で考えている構造については少なくても束になることが判明しています。ただ、型の集合全体が束になるかどうかはまだ明らかであると言える証拠が現時点ではまだ言えないため、一部の記述が間違っている可能性が高いです。束論の章(1)の方は集合論に合わせて一部修正していますが、束論の(2)の方はまだ修正が追いついていないところもあるのでそちらにも注意してください。

今回の修正内容は以下のPRで差分確認できます。
https://github.com/yo-goto/zenn-public-repo/pull/45