something for irrelevance #16

New issue

Open

opened 2023-06-12 16:23:56 -04:00 by rhi · 1 comment

rhi commented

2023-06-12 16:23:56 -04:00

Owner

squash type?
prop?

- squash type? - prop?

rhi added the

language

label 2023-06-12 16:23:56 -04:00

rhi commented

2024-04-30 20:45:48 -04:00

Author

Owner

some notes i made a while ago

A ∷= ⋯ | Prop ℓ | ⌊A⌋ | ⌈A⌉

casebody ∷= ⋯ | ⌊x⌋ ⇒ s | ⌈x⌉ ⇒ s


  𝓀 < ℓ
---------------------
  Prop 𝓀 ⇐ Prop ℓ

  A ⇐ Type ℓ
--------------------------
  ⌊A⌋ ⇐ Prop ℓ

  P ⇐ Prop ℓ
-------------------------
  ⌈P⌉ ⇐ Type ℓ

  P ⇐ Prop ℓ
------------------------
  x ⤋ ⌷ ⇐ P

  p ⇐ P   shape P ⇒ ¶
-----------------------
      [p] ⇐ ⌈P⌉

  t ⇐ A   shape A ⇒ ★
-----------------------
      [t] ⇐ ⌊A⌋

----------------
  x ⤋ ⌷ ⇐ ⌈P⌉
  x ⤋ ⌷ ⇐ ⌊A⌋


(type-ish, prop-ish, unknown, function)
shape, 𝒮, 𝒯 ∷= ★ | ¶ | ? | 𝒮 → 𝒯

[𝒮 ∧ 𝒯] [⋀ 𝒮̄]
                  𝒮 ∧ 𝒮 = 𝒮
                  𝒮 ∧ ? = ? ∧ 𝒮 = 𝒮
  (𝒮₁ → 𝒯₁) ∧ (𝒮₂ → 𝒯₂) = (𝒮₁ ∧ 𝒮₂) → (𝒯₁ ∧ 𝒯₂)
                  𝒮 ∧ 𝒯 = ⊥ (otherwise)
                   ⋀ [] = ?

[shape A ⇒ 𝒮]
  e ⇒ Type ℓ
---------------
  shape e ⇒ ★

  e ⇒ Prop ℓ
---------------
  shape e ⇒ ¶

----------------------
  shape (Type ℓ) ⇒ ★
  shape (Prop ℓ) ⇒ ★
  shape ⌈P⌉ ⇒ ★
  shape ⌊A⌋ ⇒ ¶
  shape ℕ ⇒ ★   etc

     x : A ⊢ shape B ⇒ 𝒯
-----------------------------
  shape (0.(x : A) → B) = 𝒯

  shape A ⇒ 𝒮   x : A ⊢ shape B ⇒ 𝒯   π ≠ 0
---------------------------------------------
      shape (π.(x : A) → B) = 𝒮 ∧ 𝒯

  shape A ⇒ 𝒮   x : A ⊢ shape B ⇒ 𝒯
--------------------------------------
     shape ((x : A) × B) = 𝒮 ∧ 𝒯

                shape sᵢ ⇒ 𝒮ᵢ
-------------------------------------------------
  shape (case e return _ of { aᵢ ⇒ sᵢ }) ⇒ ⋀ 𝒮ᵢ
  etc

btw the point of the shape metafunction is that a shape is an output even when its argument's whole type is only checkable

some notes i made a while ago ``` A ∷= ⋯ | Prop ℓ | ⌊A⌋ | ⌈A⌉ casebody ∷= ⋯ | ⌊x⌋ ⇒ s | ⌈x⌉ ⇒ s 𝓀 < ℓ --------------------- Prop 𝓀 ⇐ Prop ℓ A ⇐ Type ℓ -------------------------- ⌊A⌋ ⇐ Prop ℓ P ⇐ Prop ℓ ------------------------- ⌈P⌉ ⇐ Type ℓ P ⇐ Prop ℓ ------------------------ x ⤋ ⌷ ⇐ P p ⇐ P shape P ⇒ ¶ ----------------------- [p] ⇐ ⌈P⌉ t ⇐ A shape A ⇒ ★ ----------------------- [t] ⇐ ⌊A⌋ ---------------- x ⤋ ⌷ ⇐ ⌈P⌉ x ⤋ ⌷ ⇐ ⌊A⌋ (type-ish, prop-ish, unknown, function) shape, 𝒮, 𝒯 ∷= ★ | ¶ | ? | 𝒮 → 𝒯 [𝒮 ∧ 𝒯] [⋀ 𝒮̄] 𝒮 ∧ 𝒮 = 𝒮 𝒮 ∧ ? = ? ∧ 𝒮 = 𝒮 (𝒮₁ → 𝒯₁) ∧ (𝒮₂ → 𝒯₂) = (𝒮₁ ∧ 𝒮₂) → (𝒯₁ ∧ 𝒯₂) 𝒮 ∧ 𝒯 = ⊥ (otherwise) ⋀ [] = ? [shape A ⇒ 𝒮] e ⇒ Type ℓ --------------- shape e ⇒ ★ e ⇒ Prop ℓ --------------- shape e ⇒ ¶ ---------------------- shape (Type ℓ) ⇒ ★ shape (Prop ℓ) ⇒ ★ shape ⌈P⌉ ⇒ ★ shape ⌊A⌋ ⇒ ¶ shape ℕ ⇒ ★ etc x : A ⊢ shape B ⇒ 𝒯 ----------------------------- shape (0.(x : A) → B) = 𝒯 shape A ⇒ 𝒮 x : A ⊢ shape B ⇒ 𝒯 π ≠ 0 --------------------------------------------- shape (π.(x : A) → B) = 𝒮 ∧ 𝒯 shape A ⇒ 𝒮 x : A ⊢ shape B ⇒ 𝒯 -------------------------------------- shape ((x : A) × B) = 𝒮 ∧ 𝒯 shape sᵢ ⇒ 𝒮ᵢ ------------------------------------------------- shape (case e return _ of { aᵢ ⇒ sᵢ }) ⇒ ⋀ 𝒮ᵢ etc ``` btw the point of the `shape` metafunction is that a shape is an output even when its argument's whole type is only checkable