Polarity
Install
Publications
Docs
FAQ
Github
Polarity
A research language focused on dependent data and codata types
GitHub
Discord
Try Polarity
Select an example...
Lawful Functor Class
Martin-Löf Equality Type
Set Interface
STLC Type Soundness
Strong Existentials Demystified
Tutorial
Π Is Not Built-In
λ-Encoding: Church
λ-Encoding: Fu & Stump
λ-Encoding: Parigot
λ-Encoding: Scott