Created
May 1, 2022 05:39
-
-
Save evincarofautumn/8c96ee4f806a54725647c2c97bc12f8f to your computer and use it in GitHub Desktop.
Overcomplicated STLC
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# Language | |
| BlockArguments, | |
| DataKinds, | |
| DerivingStrategies, | |
| GADTs, | |
| InstanceSigs, | |
| LambdaCase, | |
| PatternSynonyms, | |
| PolyKinds, | |
| RankNTypes, | |
| ScopedTypeVariables, | |
| StandaloneDeriving, | |
| TypeOperators, | |
| UnicodeSyntax | |
| #-} | |
| {-# Options_GHC | |
| -Wall | |
| -Wno-unticked-promoted-constructors | |
| #-} | |
| import Control.Category (Category(..)) | |
| import Data.Kind (Type) | |
| import Prelude hiding ((.), id) | |
| main ∷ IO () | |
| main = pure () | |
| -------------------------------------------------------------------------------- | |
| -- ASCII Aliases | |
| -------------------------------------------------------------------------------- | |
| type Ctx0 = Γ₀ -- \Gamma_0 \x0393\x2080 | |
| type Ctx1 c = Γ₁ c -- \Gamma_1 \x0393\x2081 | |
| type SubCtx c1 c2 = c1 ⊆ c2 -- \subseteq \x2286 | |
| type T0 = T₀ -- \Tau \x03A4\x2080 | |
| type T1 t = T₁(t) -- \Tau_ \x03A4\x2081 | |
| type Term c t = c ⊢ t -- \vdash \x22A2 | |
| type Value c t = c ⊨ t -- \vDash \x22A8 | |
| type c `Ni` t = c ∋ t -- \ni \x220B | |
| type t `In` c = t ∈ c -- \in \x2208 | |
| type c2 ~> c1 = c2 ↝ c1 -- \leadsto \x219D | |
| type c1 <~ c2 = c1 ↜ c2 -- \leadsfrom \x219C | |
| pattern (:<~) ∷ (γ₁ ⊨ τ) → (γ₂ ↝ γ₁) → (γ₂ & τ ↝ γ₁) | |
| pattern c1 :<~ c2 = c1 :↜ c2 | |
| pattern Del0 ∷ '[] ↝ γ₁ | |
| pattern Del0 = Δ₀ | |
| pattern Lam0 ∷ T₀ → E → E | |
| pattern Lam0 t e = Λ₀ t e | |
| pattern Lam1 ∷ T₁(α) → (γ & α ⊢ β) → (γ ⊢ α :→ β) | |
| pattern Lam1 t e = Λ₁ t e | |
| pattern (:->) ∷ T₀ → T₀ → T₀ | |
| pattern a :-> b = a :→ b | |
| pattern N0 ∷ T₀ | |
| pattern N0 = TN₀ | |
| pattern T0 ∷ T₀ | |
| pattern T0 = TT₀ | |
| pattern K0 ∷ T₀ | |
| pattern K0 = TK₀ | |
| pattern (:=>) ∷ T₁(α) → T₁(β) → T₁(α :→ β) | |
| pattern a :=> b = a :⇒ b | |
| pattern N1 ∷ T₁(TN₀) | |
| pattern N1 = TN₁ | |
| pattern T1 ∷ T₁(TT₀) | |
| pattern T1 = TT₁ | |
| pattern K1 ∷ T₁(TK₀) | |
| pattern K1 = TK₁ | |
| pattern CtxEqZ ∷ (γ ⊆ γ) | |
| pattern CtxEqZ = ΓEqZ | |
| pattern CtxLt ∷ (γ₁ ⊆ γ₂) → (γ₁ ⊆ γ₂ & τ) | |
| pattern CtxLt p = ΓLt p | |
| pattern CtxEqS ∷ (γ₁ ⊆ γ₂) → (γ₁ & τ ⊆ γ₂ & τ) | |
| pattern CtxEqS p = ΓEqS p | |
| wmap ∷ (Affine p) ⇒ (γ₁ ⊆ γ₂) → (p γ₁ α) → (p γ₂ α) | |
| wmap = (↪) | |
| -------------------------------------------------------------------------------- | |
| -- Fixities | |
| -------------------------------------------------------------------------------- | |
| infix 1 ↜, <~ | |
| infix 1 ↝, ~> | |
| infix 1 ⊢ | |
| infix 1 ⊨ | |
| infix 2 ∈ | |
| infix 2 ∋ | |
| infix 2 ⊆ | |
| infixr 4 :→, :-> | |
| infixr 4 :⇒, :=> | |
| infixr 5 :↜, :<~ | |
| infixl 5 & | |
| infixl 5 :& | |
| infixr 6 ↪ | |
| -------------------------------------------------------------------------------- | |
| -- Types | |
| -------------------------------------------------------------------------------- | |
| data T₀ where -- untyped types | |
| (:→) ∷ T₀ → T₀ → T₀ -- function type | |
| TN₀ ∷ {} → T₀ -- natural type | |
| TT₀ ∷ {} → T₀ -- value kind | |
| TK₀ ∷ {} → T₀ -- type kind | |
| data T₁(τ ∷ T₀) where -- and their typed kin | |
| (:⇒) ∷ T₁(α) → T₁(β) → T₁(α :→ β) | |
| TN₁ ∷ {} → T₁(TN₀) | |
| TT₁ ∷ {} → T₁(TT₀) | |
| TK₁ ∷ {} → T₁(TK₀) | |
| type Γ₀ = [T₀] -- untyped typing context | |
| type (γ ∷ Γ₀) & (τ ∷ T₀) = τ ': γ | |
| data Γ₁(γ ∷ Γ₀) where -- typed typing context | |
| Γ₀ ∷ {} → Γ₁('[]) -- nil | |
| (:&) ∷ Γ₁(γ) → T₁(τ) → Γ₁(γ & τ) -- cons | |
| data (γ₁ ∷ Γ₀) ⊆ (γ₂ ∷ Γ₀) where -- context inclusion proof | |
| ΓEqZ -- base case: contexts are equal (reflexivity) | |
| ∷ {} | |
| -- ───────────── | |
| → γ ⊆ γ | |
| ΓLt -- one context is a subcontext of another | |
| ∷ γ₁ ⊆ γ₂ | |
| -- ───────────── | |
| → γ₁ ⊆ γ₂ & τ | |
| ΓEqS -- inductive case: contexts have a common supercontext | |
| ∷ γ₁ ⊆ γ₂ | |
| -- ─────────────── | |
| → γ₁ & τ ⊆ γ₂ & τ | |
| type τ ∈ γ -- in | |
| = γ ∋ τ -- ni | |
| data (γ ∷ [κ]) ∋ (α ∷ κ) where -- context containment proof | |
| -- made of a fancy index | |
| SZ ∷ {} -- zero, head of context | |
| -- ───────── | |
| → α ∈ γ & α | |
| SS ∷ α ∈ γ -- the variable is in another castle | |
| -- ───────── | |
| → α ∈ γ & β | |
| data E where -- an untyped term | |
| L₀ ∷ A₀ → E -- literal | |
| V₀ ∷ Int → E -- variable | |
| Λ₀ ∷ T₀ → E → E -- abstraction | |
| A₀ ∷ E → E → E -- application | |
| -- typed term, per a context | |
| data (γ ∷ Γ₀) ⊢ (τ ∷ T₀) where | |
| L₁ -- typed literal | |
| ∷ A₁(τ) | |
| -- ───── [lit] | |
| → γ ⊢ τ | |
| V₁ -- typed variable | |
| ∷ τ ∈ γ | |
| -- ───── [var] | |
| → γ ⊢ τ | |
| Λ₁ -- typed abstraction | |
| ∷ T₁(α) | |
| → γ & α ⊢ β | |
| -- ────────── [abs] | |
| → γ ⊢ α :→ β | |
| A₁ -- typed application | |
| ∷ γ ⊢ α :→ β | |
| → γ ⊢ α | |
| -- ────────── | |
| → γ ⊢ β | |
| data A₀ where -- atomic elements | |
| Zero₀ ∷ A₀ -- natural zero | |
| Succ₀ ∷ A₀ -- natural successor | |
| Nat₀ ∷ A₀ -- type of naturals | |
| Star₀ ∷ A₀ -- kind of types inhabited by values | |
| Box₀ ∷ A₀ -- kind of types inhabited by types | |
| Arr₀ ∷ A₀ -- function type constructor | |
| -- | |
| data A₁(τ ∷ T₀) where -- and their typed kin | |
| Zero ∷ A₁(TN₀) | |
| Succ ∷ A₁(TN₀ :→ TN₀) | |
| Nat ∷ A₁(TT₀) | |
| Star ∷ A₁(TT₀) | |
| Box ∷ A₁(TK₀) | |
| Arr ∷ A₁(TT₀ :→ TT₀ :→ TT₀) | |
| data (γ ∷ Γ₀) ⊨ (τ ∷ T₀) where -- valuation of a term in a model | |
| Constant ∷ | |
| { inconstant | |
| ∷ A₁(τ) -- from a typed atom | |
| -- ───── -- obtain | |
| } → γ ⊨ τ -- a constant value of that type | |
| Natural ∷ | |
| { unnatural | |
| ∷ γ ⊢ TN₀ -- from a natural term | |
| -- ────── -- obtain | |
| } → γ ⊨ TN₀ -- a natural value | |
| Neutral -- a neutral application | |
| ∷ γ ⊨ α :→ β -- comprises a function | |
| → γ ⊨ α -- and argument | |
| -- ────────── -- | |
| → γ ⊨ β -- yet to reduce | |
| Close ∷ | |
| { open | |
| ∷ ∀γ₂ -- for any | |
| . Γ₁(γ₂) -- valid context | |
| → γ₁ ⊆ γ₂ -- in which it finds itself | |
| → γ₂ ⊨ α -- therein applied to an argument | |
| → γ₂ ⊨ β -- therein gives its result | |
| -- ─────────── -- | |
| } → γ₁ ⊨ α :→ β -- a closure | |
| type γ₂ ↝ γ₁ -- thence hither | |
| = γ₁ ↜ γ₂ -- hither thence | |
| data (γ₁ ∷ Γ₀) ↜ (γ₂ ∷ Γ₀) where -- an environment | |
| Δ₀ | |
| ∷ {} | |
| -- ──────── | |
| → '[] ↝ γ₁ -- empty | |
| (:↜) | |
| ∷ γ₁ ⊨ τ -- if there is a thing | |
| → γ₂ ↝ γ₁ -- and where it is may be here | |
| -- ─────────── | |
| → γ₂ & τ ↝ γ₁ -- then the thing may be here | |
| -------------------------------------------------------------------------------- | |
| -- Classes & Instances | |
| -------------------------------------------------------------------------------- | |
| class Affine (p ∷ Γ₀ → κ → Type) where -- context-indexed constructors | |
| (↪) -- whose demands can be weakened | |
| ∷ γ₁ ⊆ γ₂ | |
| → p γ₁ α | |
| -- ─────── | |
| → p γ₂ α | |
| instance Affine (∋) where | |
| (↪) | |
| ∷ γ₁ ⊆ γ₂ | |
| → τ ∈ γ₁ | |
| -- ─────── | |
| → τ ∈ γ₂ | |
| (↪) = \ case | |
| ΓEqZ → id | |
| ΓLt p → \ x → SS (p ↪ x) | |
| ΓEqS p → \ case | |
| SZ → SZ | |
| SS x → SS (p ↪ x) | |
| instance Affine (⊢) where | |
| (↪) | |
| ∷ γ₁ ⊆ γ₂ | |
| → γ₁ ⊢ α | |
| → γ₂ ⊢ α | |
| (↪) p = \ case | |
| L₁ a → L₁ a | |
| V₁ x → V₁ (p ↪ x) | |
| Λ₁ α e → Λ₁ α (ΓEqS p ↪ e) | |
| A₁ e₁ e₂ → A₁ (p ↪ e₁) (p ↪ e₂) | |
| instance Show (γ ⊨ τ) where | |
| showsPrec p = showParen (p > 10) . \ case | |
| Constant a → showString "Constant " . showsPrec 10 a | |
| Natural n → showString "Natural " . showsPrec 10 n | |
| Neutral f x → showsPrec 11 f . showString " " . showsPrec 10 x | |
| Close _f → showString "Close (error \"⟨closure⟩\")" | |
| instance Affine (⊨) where | |
| (↪) | |
| ∷ γ₁ ⊆ γ₂ | |
| → γ₁ ⊨ τ | |
| -- ─────── | |
| → γ₂ ⊨ τ | |
| (↪) p = \ case | |
| Constant a → Constant a | |
| Natural n → Natural (p ↪ n) | |
| Neutral e₁ e₂ → Neutral (p ↪ e₁) (p ↪ e₂) | |
| Close f → Close \ γ q → f γ (q . p) | |
| instance Category (⊆) where | |
| id ∷ γ ⊆ γ | |
| id = ΓEqZ | |
| (.) | |
| ∷ γ₂ ⊆ γ₃ | |
| → γ₁ ⊆ γ₂ | |
| → γ₁ ⊆ γ₃ | |
| ΓEqZ . f = f | |
| g . ΓEqZ = g | |
| ΓLt p . f = ΓLt (p . f) | |
| ΓEqS p . ΓLt q = ΓLt (p . q) | |
| ΓEqS p . ΓEqS q = ΓEqS (p . q) | |
| instance Affine (↜) where | |
| (↪) | |
| ∷ γ₁ ⊆ γ₂ | |
| → γ₃ ↝ γ₁ | |
| -- ─────── | |
| → γ₃ ↝ γ₂ | |
| (↪) p = \ case | |
| Δ₀ → Δ₀ | |
| v :↜ e → (p ↪ v) :↜ (p ↪ e) | |
| deriving stock instance Show (A₁(τ)) | |
| deriving stock instance Show (T₁(τ)) | |
| deriving stock instance Show (γ ∋ α) | |
| deriving stock instance Show (γ ⊢ τ) | |
| deriving stock instance Show (γ₁ ⊆ γ₂) | |
| deriving stock instance Show A₀ | |
| deriving stock instance Show E | |
| deriving stock instance Show T₀ | |
| -------------------------------------------------------------------------------- | |
| -- Evaluation | |
| -------------------------------------------------------------------------------- | |
| (!) | |
| ∷ γ₂ ↝ γ₁ | |
| → τ ∈ γ₂ | |
| -- ─────── | |
| → γ₁ ⊨ τ | |
| (v :↜ _δ) ! SZ = v | |
| (_v :↜ δ) ! SS x = δ ! x | |
| Δ₀ ! _ = error "impossible" | |
| reify | |
| ∷ Γ₁(γ) | |
| → T₁(τ) | |
| → γ ⊨ τ | |
| -- ───── | |
| → γ ⊢ τ | |
| reify γ = \ case | |
| TN₁ → unnatural | |
| α :⇒ β → \ v → Λ₁ α (reify γ' β (open v γ' (ΓLt id) (reflect γ' α (V₁ SZ)))) | |
| where | |
| γ' = γ :& α | |
| TT₁ → \ (Constant Star) → L₁ Star | |
| TK₁ → \ (Constant Box) → L₁ Box | |
| reflect | |
| ∷ Γ₁(γ) | |
| → T₁(τ) | |
| → γ ⊢ τ | |
| -- ───── | |
| → γ ⊨ τ | |
| reflect _γ = \ case | |
| TN₁ → Natural | |
| α :⇒ β → \ e → Close \ γ' p → reflect γ' β . A₁ (p ↪ e) . reify γ' α | |
| TT₁ → \ (L₁ Star) → Constant Star | |
| TK₁ → \ (L₁ Box) → Constant Box | |
| eval | |
| ∷ ∀γ₁ γ₂ τ | |
| . Γ₁(γ₁) | |
| → γ₂ ↝ γ₁ | |
| → γ₂ ⊢ τ | |
| -- ─────── | |
| → γ₁ ⊨ τ | |
| eval γ δ = eval' | |
| where | |
| eval' | |
| ∷ ∀τ' | |
| . γ₂ ⊢ τ' | |
| -- ─────── | |
| → γ₁ ⊨ τ' | |
| eval' = \ case | |
| L₁ a → Constant a | |
| V₁ x → δ ! x | |
| Λ₁ _α e → Close \ γ' p v → let δ' = v :↜ p ↪ δ in eval γ' δ' e | |
| A₁ e₁ e₂ → let | |
| v₂ = eval' e₂ | |
| in case eval' e₁ of | |
| Constant Succ → Natural $ A₁ (L₁ Succ) (unnatural v₂) | |
| Close f → f γ id v₂ | |
| v₁ → Neutral v₁ v₂ | |
| normalize | |
| ∷ ∀γ₁ γ₂ τ | |
| . Γ₁(γ₁) | |
| → T₁(τ) | |
| → γ₂ ↝ γ₁ | |
| → γ₂ ⊢ τ | |
| → γ₁ ⊢ τ | |
| normalize γ τ δ = reify γ τ . eval γ δ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment