Skip to content

Instantly share code, notes, and snippets.

@evincarofautumn

evincarofautumn/Stlc.hs

Created May 1, 2022 05:39
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save evincarofautumn/8c96ee4f806a54725647c2c97bc12f8f to your computer and use it in GitHub Desktop.
Save evincarofautumn/8c96ee4f806a54725647c2c97bc12f8f to your computer and use it in GitHub Desktop.
Download ZIP
Overcomplicated STLC
Raw
Stlc.hs
{-# 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