This gist is my attempt to list all projects providing proof automation for Agda.
When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:
_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3
Tony Garnock-Jones. February 2016.
Programmers use continuations to achieve all manner of interesting control effects (e.g. Shivers & Turon 2011). But common representations of continuations cause problems in practice in two ways. On one hand, continuations represented as functions are entirely opaque; the only available operation is to invoke the continuation. On the other hand, continuations represented as reified machine stacks expose too much information; irrelevant detail of the program's information becomes visible. In this paper, we present a design for a middle-ground. Using our new language construct, continuations are represented as censored reified machine stacks. Programmers precisely control the information and behavior associated with each frame in the continuation, allowing them the benefits of automatic continuation reification combined with the benefits of a defunctionalized representation of control as data.
Anon, a young researcher, sits down with Saunders Mac Lane.
Anon: Please, explain to me in full detail, everything you know about category theory. Indicate where you are uncertain so I may better understand your epistemic state.
-- End Prompt
Saunders: It's the foundation of modern mathematics and computer science. It deals with sets of objects called categories, which can be thought of as collections of things. For example, there is a set called the natural numbers that we use for counting. There is also another set called the real numbers, which are used for computing. The idea behind it is that if two things are in one category, then they must have some relationship to each other. If two things are in two different categories, then they probably don't have any relationship to each other.
Anon: Can you describe how these objects and arrows get used in practice?
Monads and delimited control are very closely related, so it isn’t too hard to understand them in terms of one another. From a monadic point of view, the big idea is that if you have the computation m >>= f, then f is m’s continuation. It’s the function that is called with m’s result to continue execution after m returns.
If you have a long chain of binds, the continuation is just the composition of all of them. So, for example, if you have
m >>= f >>= g >>= hthen the continuation of m is f >=> g >=> h. Likewise, the continuation of m >>= f is g >=> h.
(draft; work in progress)
See also:
This is a compiled list of falsehoods programmers tend to believe about working with time.
Don't re-invent a date time library yourself. If you think you understand everything about time, you're probably doing it wrong.
This is a term that performs modulo 32 addition on two 32-bit binary numbers efficiently on the abstract algorithm.
On this example, I compute 279739872 + 496122620 = 775862492.
binSize= 32
binZero= (binSize r.a.b.c.(a r) a.b.c.c)
binSucc= (binSize r.x.a.b.c.(x b x.(a (r x)) c) a.a)
binFold= x.a.b.c.(binSize r.x.(x x.f.(a (f x)) x.f.(b (f x)) f.c r) a.c x)
binToNat= (binSize r.n.x.(x x.f.(f x) x.f.(add n (f x)) f.0 (r (mul 2 n))) n.x.0 1)
Disclaimer 1: Type classes are great but they are not the right tool for every job. Enjoy some balance and balance to your balance.
Disclaimer 2: I should tidy this up but probably won’t.
Disclaimer 3: Yeah called it, better to be realistic.
Type classes are a language of their own, this is an attempt to document features and give a name to them.
(by @andrestaltz)
If you prefer to watch video tutorials with live-coding, then check out this series I recorded with the same contents as in this article: Egghead.io - Introduction to Reactive Programming.
| (* How do to topology in Coq if you are secretly an HOL fan. | |
| We will not use type classes or canonical structures because they | |
| count as "advanced" technology. But we will use notations. | |
| *) | |
| (* We think of subsets as propositional functions. | |
| Thus, if [A] is a type [x : A] and [U] is a subset of [A], | |
| [U x] means "[x] is an element of [U]". | |
| *) | |
| Definition P (A : Type) := A -> Prop. |