You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Laymans explanation of delimited continuations with examples of using them for exception handling and nondeterministic programming.
Delimited Continuations
Delimited continuations manipulate the control flow of programs. Similar to control structures like conditionals or loops they allow to deviate from a sequential flow of control.
We use exception handling as another example for control flow manipulation and later show how to implement it using delimited continuations. Finally, we show that nondeterminism can also be expressed using delimited continuations.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Elm Destructuring (or Pattern Matching) cheatsheet
Should be work with 0.18
Destructuring(or pattern matching) is a way used to extract data from a data structure(tuple, list, record) that mirros the construction. Compare to otherlanguages, Elm support much less destructuring but let's see what it got !
How to formulate and prove the statement "all functions are continuous" in an effectful functional language?
Are all functions continuous?
Mathematical background
Brouwer's statement "all functions are continuous" can be formulated without reference to
topology as follows.
Definition: A functional f : (N → N) → N is continuous at a : N → N when there
exists m : N such that, for all b : N → N, if ∀ k < m, a k = b k then f a = f b.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
What is the Strict Aliasing Rule and Why do we care?
(OR Type Punning, Undefined Behavior and Alignment, Oh My!)
What is strict aliasing? First we will describe what is aliasing and then we can learn what being strict about it means.
In C and C++ aliasing has to do with what expression types we are allowed to access stored values through. In both C and C++ the standard specifies which expression types are allowed to alias which types. The compiler and optimizer are allowed to assume we follow the aliasing rules strictly, hence the term strict aliasing rule. If we attempt to access a value using a type not allowed it is classified as undefined behavior(UB). Once we have undefined behavior all bets are off, the results of our program are no longer reliable.
Unfortunately with strict aliasing violations, we will often obtain the results we expect, leaving the possibility the a future version of a compiler with a new optimization will break code we th
I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.
Q: What is cubical type theory?
A: It’s a type theory giving homotopy type theory its computational meaning.
Q: What is homotopy type theory then?
A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.
When making this website, i wanted a simple, reasonable way to make it look good on most displays. Not counting any minimization techniques, the following 58 bytes worked well for me:
main {
max-width:38rem;
padding:2rem;
margin: auto;
}