Skip to content

Instantly share code, notes, and snippets.

@evincarofautumn

evincarofautumn/Stlc.hs

Created May 1, 2022 05:39
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save evincarofautumn/8c96ee4f806a54725647c2c97bc12f8f to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
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