Have you ever had to write code that made a complex series of succesive modifications to a single piece of mutable state? (Almost certainly yes.)
Did you ever wish you could make the compiler tell you if a particular operation on the state was illegal at a given point in the modifications? (If you're a fan of static typing, probably yes.)
If that's the case, the indexed state monad can help!
Motivation
The indexed state monad is not the only indexed monad out there; it's not even the only useful one. In this tutorial, we will explore another indexed monad, this time one that encapsulates the full power of delimited continuations: the indexed continuation monad.
The relationship between the indexed and regular state monads holds true as well for the indexed and regular continuation monads, but while the indexed state monad allows us to keep a state while changing its type in a type-safe way, the indexed continuation monad allows us to manipulate delimited continuations while the return type of the continuation block changes arbitrarily. This, unlike the regular continuation monad, allows us the full power of delimited continuations in a dynamic language like Scheme while still remaining completely statically typed.
We've already looked at two different indexed monads in our tour so far, so let's go for a third whose regular counterpart isn't as well known: the privilege monad.
The regular privilege monad allows you to express constraints on which operations a given component is allowed to perform. This lets the developers of seperate interacting components be statically assured that other components can't access their private state, and it gives you a compile-time guarantee that any code that doesn't have appropriate permissions cannot do things that would require those permissions. Unfortunately, you cannot easily, and sometimes cannot at all, build code in the privilege monad that gains or loses permissions as the code runs; in other words, you cannot (in general) raise or lower your own privilege level, not even when it really should be a
| module Lens where | |
| open import Level | |
| open import Function | |
| open import Relation.Binary | |
| open import Data.Product | |
| open import Relation.Binary.Product.Pointwise | |
| open import Data.Sum | |
| open import Relation.Binary.Sum | |
| open import Data.Empty | |
| open import Function.Inverse |
| IT'S SHOWTIME | |
| HEY CHRISTMAS TREE isLessThan100 | |
| YOU SET US UP @NO PROBLEMO | |
| HEY CHRISTMAS TREE n | |
| YOU SET US UP 0 | |
| HEY CHRISTMAS TREE multiple | |
| YOU SET US UP @NO PROBLEMO | |
| STICK AROUND isLessThan100 |
| {-# LANGUAGE ForeignFunctionInterface #-} | |
| {-# LANGUAGE JavaScriptFFI #-} | |
| {-# LANGUAGE UnliftedFFITypes #-} | |
| {-# LANGUAGE GHCForeignImportPrim #-} | |
| {-# LANGUAGE TypeSynonymInstances #-} | |
| {-# LANGUAGE FlexibleInstances #-} | |
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE PolyKinds #-} | |
| {-# LANGUAGE DeriveDataTypeable #-} | |
| {-# LANGUAGE TypeFamilies #-} |
context: this is a draft for planned edits / cleanups to the current mac build directions
have apple command line tools installed, as well as mactex, and your favorite OS X package manager (which for the rest of these directions we assume is brew)
since we assume we're using brew, install it!
Recently, Rust 1.26 was released, and with it came stable access to a heavily desired feature: impl Trait.
For those unfamiliar, impl Trait lets you write something like this:
fn foo<'a, A, B>(x: &'a mut A) -> impl Bar<'a, B> { ... }and have it be translated to something like this:
This document was originally written several years ago. At the time I was working as an execution core verification engineer at Arm. The following points are coloured heavily by working in and around the execution cores of various processors. Apply a pinch of salt; points contain varying degrees of opinion.
It is still my opinion that RISC-V could be much better designed; though I will also say that if I was building a 32 or 64-bit CPU today I'd likely implement the architecture to benefit from the existing tooling.
Mostly based upon the RISC-V ISA spec v2.0. Some updates have been made for v2.2
The RISC-V ISA has pursued minimalism to a fault. There is a large emphasis on minimizing instruction count, normalizing encoding, etc. This pursuit of minimalism has resulted in false orthogonalities (such as reusing the same instruction for branches, calls and returns) and a requirement for superfluous instructions which impacts code density both in terms of size and
I'm writing this post to publicly come out as trans (specifically: I wish to transition to become a woman).
This post won't be as polished or edited as my usual posts, because that's kind of the point: I'm tired of having to edit myself to make myself acceptable to others.
I'm a bit scared to let people know that I'm trans, especially because I'm not yet in a position where I can transition (for reasons I don't want to share, at least not in public) and it's really shameful. However, I'm getting really