Higher Logics

Extending the work in my last post , I've developed a way to express an almost type-safe, general monad in C# . Similar to my module translation, the single monad object becomes a pair of co-operating objects, only one of which the monad implementor must define. Since C# cannot abstract over type constructors, I had to exploit the only feature that could accomodate the flexibility I needed: C#'s dynamic typing. // The Monad object, indexed by a singleton type that implements the // monad operations. public sealed class Monad<M, T> where M : struct, IMonadOps<M> { ... } // An object that implements operations on the monad's encapsulated // state. public interface IMonadOps<M> where M : struct, IMonadOps<M> { /// Return the encapsulated state for the monad's zero value. object Zero<T>(); // Return the encapsulated state for the 'unit' operation. object Unit<T>(T t); // Perform a bind operation given th...

I've found other monad tutorials very frustrating. They are typically written in expressive languages with type inference, which permits concise descriptions, but obscures the underlying type structure. I've been struggling with writing something close to a monad in C# for quite some time, simply because none of these tutorials give a sufficiently complete description of a monad's structure. Suprisingly, the Wikipedia page on monads helped clarify what I was missing. Here is the general structure of a monad all these tutorials use : -- the type of monad m type m a = ... -- return is a type constructor that creates monad instances return :: a → m a -- bind is a function that combines a monad instance m a with a -- computation that produces another monad instance m b from a's -- to produce a new monad instance m b bind :: m a → (a → m b) → m b So the monad type 'm', has a function 'return' that constructs instances of that type, and 'bind' which c...

The venerable Oleg Kiselyov once posted about the "best" collection traversal API . Let's call this ideal iterator a "SuperFold". LTU also covered his article . Essentially, a SuperFold is a left fold with early termination support. Any cursor can then be automatically derived from the SuperFold. The converse is not true. Additional arguments are made in the above paper and in the LTU thread, so I won't repeat them here. Without further ado, I present the SuperFold for my purely functional list in C# : //OCaml signature: ((T → B → bool * B) → B → B) → (T → B → bool * B) → B → B B SuperFold<B>( Fun<Fun<T, B, Pair<bool, B>>, B, B> self, Fun<T, B, Pair<bool, B>> proc, B seed) { bool cont; proc(head, seed).Bind(out cont, out seed); return cont ? self(proc, seed) : seed; } While quite simple, it's not as efficient as it should be since C#/.NET doesn't support proper tail calls. You can see in that so...

As Chung-chieh Shan pointed out , my encoding of modules in C# is somewhat limited. In particular, I cannot abstract over type constructors, which is to say, C# is missing generics over generics. Consider the Orc.NET interpreter: class Orc { class Exp<T> { ... } public Exp<U> Seq<T,U>(Exp<T> e1, <U>) { ... } public Exp<T> Par<T>(Exp<T> e1, Exp<T>) { ... } public Exp<T> Where<T>(Exp<T> e1, Exp<Promise<T>>) { ... } } This is the result of my translation, which was necessitated by the "Where" method. Where introduces a dependency which currently cannot be expressed with ordinary C# constraints, so the module encoding is necessary. The above interface is a direct, faithful implementation of the Orc semantics. The implementation I currently have is an interpreter for those semantics. What if I want to provide a compiler instead? The interface should remain the same , but the implementation ...

I've written about the limitations of C#'s equational constraints before . Truth is, I now believe that any such limits can be circumvented by a relatively simple translation. The result is less "object-oriented", as it requires a set of cooperating objects instead of being encapsulated in a single object. Let's take a simple, unsafe list flattening operation described in Generalized Algebraic Data Types and Object-Oriented Programming (GADTOOP) . This can be expressed in OCaml as: let List = struct type 'a t = Nil | Cons of 'a * 'a t let append l a = Cons(a, l) let flatten la = Cons(a, l) -> append a (flatten l) | Nil -> Nil end The argument to flatten, la, is a list of lists of type 'a. However, there is no way to express this in C# without unrestricted equational constraints as I described earlier. Here is the translation to C# from GADTOOP: public abstract class List<T> {... public abstract List<T> Append(Lis...

In previous posts, I had commented on certain non-sensical limitations in the C# type system, particularly with regard to equational constraints on generic type parameters ; these unfortunate limitations significantly reduce the expressiveness of well-typed solutions. Microsoft Research had actually already tackled the problem in their 2006 paper Variance and Generalized Constraints for C# Generics . Taking inspiration from Scala, they generalize class and method parameter constraints with arbitrary subtyping relations, and they further add use-constraints on generic methods. This increased expressiveness should address the problems I alluded to in my previous posts; if only the changes were integrated into the .NET VM and C#... :-) [Edit: figures that LTU already covered this paper ]

The benefits of advanced programmings languages are sometimes difficult to grasp for everyday programmers. The features of such languages and how they relate to industrial software development are sometimes hard to understand, especially since the arguments are couched in terms such as "referential transparency", "totality", "side-effect-free", "monads", "non-determinism", "strong static typing", "algebraic data types", "higher-order functions", "laziness/call-by-need", and so on. Many of these features are attributed to "pure" languages, but purity is also a nebulous concept. I will explain the importance of a number of these features and how they impact the everyday programmer's life. The Benefits of Referential Transparency Referential transparency (RT) is a simple principle with profound consequences. Essentially, RT dictates that functions may access only the parameters they...