nad / partiality-monad Goto Github PK
View Code? Open in Web Editor NEWLicense: MIT License
License: MIT License
------------------------------------------------------------------------ -- Code related to the paper "Partiality, Revisited: The Partiality -- Monad as a Quotient Inductive-Inductive Type" -- -- Thorsten Altenkirch, Nils Anders Danielsson and Nicolai Kraus ------------------------------------------------------------------------ -- Note that this is a version of the code that does not quite match -- the description in the paper. Some key changes (there might be -- others): -- -- * The partiality monad is not postulated, but defined as a QIIT -- (Agda's cubical features are used). The types and eliminators are -- marked as "abstract", so the eliminators do not compute. -- -- * Rewrite rules are no longer used. Instead the propositional -- truncation and set quotient operators are defined as -- (non-abstract) QITs. -- -- * The set quotient operator that is used can be applied to -- arbitrary binary relations, not only propositional ones. {-# OPTIONS --cubical --sized-types #-} module README where -- Note that our definition of the partiality monad and some of the -- results are heavily inspired by the section on Cauchy reals in the -- HoTT book (first edition). -- The partiality algebra code uses ideas and concepts from "Inductive -- types in homotopy type theory" by Awodey, Gambino and Sojakova, -- "Inductive Types in Homotopy Type Theory" by Sojakova, "Quotient -- inductive-inductive types" by Altenkirch, Capriotti, Dijkstra and -- Nordvall Forsberg, and Gabe Dijkstra's PhD thesis. ------------------------------------------------------------------------ -- Pointers to results from the paper -- In order to more easily find code corresponding to results from the -- paper, see the following module. Note that some of the code -- referenced below is not discussed at all in the paper. import README.Pointers-to-results-from-the-paper ------------------------------------------------------------------------ -- Partiality algebras -- Partiality algebras. import Partiality-algebra -- Some partiality algebra properties. import Partiality-algebra.Properties -- Partiality algebra categories. import Partiality-algebra.Category -- Eliminators and initiality. import Partiality-algebra.Eliminators -- Monotone functions. import Partiality-algebra.Monotone -- ω-continuous functions. import Partiality-algebra.Omega-continuous -- Strict ω-continuous functions. import Partiality-algebra.Strict-omega-continuous -- Fixpoint combinators. import Partiality-algebra.Fixpoints -- Pi with partiality algebra families as codomains. import Partiality-algebra.Pi ------------------------------------------------------------------------ -- The partiality monad -- A quotient inductive-inductive definition of the partiality monad. import Partiality-monad.Inductive -- Specialised eliminators. import Partiality-monad.Inductive.Eliminators -- A function that runs computations. import Partiality-monad.Inductive.Approximate -- An alternative characterisation of the information ordering, along -- with related results. import Partiality-monad.Inductive.Alternative-order -- Monotone functions. import Partiality-monad.Inductive.Monotone -- ω-continuous functions. import Partiality-monad.Inductive.Omega-continuous -- The partiality monad's monad instance. import Partiality-monad.Inductive.Monad -- The partiality monad's monad instance, defined via an adjunction. import Partiality-monad.Inductive.Monad.Adjunction -- Strict ω-continuous functions. import Partiality-monad.Inductive.Strict-omega-continuous -- Fixpoint combinators. import Partiality-monad.Inductive.Fixpoints ------------------------------------------------------------------------ -- Some examples -- A function that, given a stream, tries to find an element -- satisfying a predicate. import Search -- Examples involving simple λ-calculi. import README.Lambda ------------------------------------------------------------------------ -- An alternative definition of the delay monad -- The delay monad, defined using increasing sequences of potential -- values. import Delay-monad.Alternative -- Various properties. import Delay-monad.Alternative.Properties -- Theorems relating the coinductive definition of the delay -- monad to the alternative one and to another type. import Delay-monad.Alternative.Equivalence -- Termination predicates. import Delay-monad.Alternative.Termination -- Information orderings. import Delay-monad.Alternative.Partial-order -- Weak bisimilarity. import Delay-monad.Alternative.Weak-bisimilarity -- Two eliminators for Delay-monad.Alternative.Delay (A / R). import Delay-monad.Alternative.Eliminators ------------------------------------------------------------------------ -- The delay monad quotiented by weak bisimilarity -- The delay monad quotiented by weak bisimilarity. import Partiality-monad.Coinductive -- A partial order. import Partiality-monad.Coinductive.Partial-order -- An alternative definition of the partiality monad: a variant of the -- delay monad quotiented by a notion of weak bisimilarity. import Partiality-monad.Coinductive.Alternative ------------------------------------------------------------------------ -- A proof of equivalence -- The partiality monads in Partiality-monad.Inductive and -- Partiality-monad.Coinductive are pointwise equivalent, for sets, -- assuming extensionality and countable choice. import Partiality-monad.Equivalence ------------------------------------------------------------------------ -- ω-cpos -- Pointed and non-pointed ω-cpos. import Omega-cpo -- The code in the following three modules is based on a suggestion -- from Paolo Capriotti. -- A quotient inductive-inductive definition of the lifting -- construction on ω-cpos. import Lifting -- An alternative but equivalent definition of the partiality monad -- (but only for sets), based on the lifting construction in Lifting. import Lifting.Partiality-monad
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.