apskii

The Indexed Privilege Monad in Haskell, Scala, and C#

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.

Motivation

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

Introduction

Machinist Issue #2 asks:

Is it correct, that this stuff is completely obsolete now due to value classes or are there still some use cases? An example of using value class for zero-cost implicit enrichment: [...]

The short answer is that Machinist is not obsolete: value classes existed before the Machinist macros were implemented, and they do not solve the

	Require Import Utf8.

	Inductive subtype (a b : Set) : Set :=
	\| ST : (a -> b) -> subtype a b.

	Infix ":>" := subtype (at level 50).

	Definition st {x y} f := ST x y f.

	Definition unpack {a b : Set} (st : a :> b) :=

	class Box<T> { constructor(public value: T) {} }

	class A {}
	class B { foo() {} }

	var bb : Box<B> = new Box<B>(null);
	// This typechecks (it shouldn't; T is used both in a co- and contra-variant position, so it's invariant)...
	var ba : Box<A> = xb;

	ba.value = new A();

	{-# LANGUAGE DeriveFunctor #-}
	import Data.Functor.Foldable
	import qualified Data.Set as S

	data Solve a x = Conquer a \| Bottom \| Divide x x deriving (Functor)

	data Problem = Solution [Int] \| Problem [([Int], S.Set Int)]

	g n m = hylo phi psi $ Problem [([i], S.singleton i) \| i <- [1..n-1]] where
	psi (Solution is) = Conquer is

	window.console.clog = function(log){
	var message = typeof log === 'object' ? '%cLooks like you\'re trying to log an ' : '%cLooks like you\'re trying to log a ',
	style = 'background:url(http://i.imgur.com/SErVs5H.png);padding:5px 15px 142px 19px;line-height:280px;';
	console.log.call(console, message + typeof log + '.', style);
	};