Lambda the Ultimate

I breezed through the paper. It looks like they could take a proof-carrying-code-like approach and use the type checking as an aid to safety verification.

It's pretty easy to make this decidable when you control the source language and can impose a strict discipline. What's actually implemented is more than a standard (flow-insensitive) type system, but not _that_ much more involved.

Paper on Sing# language features.

The basic idea is that types can be annotated with states. For example, let's say you have a "Connection" type with three possible states: "Begin", "Connected", "End". Given a protocol object whose type is "Connection!Begin", you can call the "Connect(...)" method. After that method returns, the type is "Connection!Connected" and the compiler will no longer allow calls to "Connect(...)", but will allow calls to "Send(...)" and "Receive(...)".

They make this statically enforceable by restricting aliasing. I don't remember the details, but it was something like "if you want to track the object's state statically, then the compiler has to know about all aliases of the object".

Yes, organizing the classes/types to ensure valid state transitions is handy, but you still can't enforce proper usage statically without some kind of linear or alias type system. What if you needed an explicit Close() funtion (putting it in a finalizer isn't always acceptable); can you think of a way to ensure that a client can't call Conn.Send() after calling Close() in ordinary ML? It's the aliasing that's the problem, and I can't think of any way to do it.

The closest I've gotten, is that Modem have only one operation, Process(), which accepts a function that takes a Conn, and once that function finishes executing, the connection is closed automatically. Of course, with mutable references this can be circumvented, since the Conn reference can then escape the scope of the Process() function; of course, this usage is fairly bizarre in itself, but it's not statically preventable, which is what I'm looking for.

You've gotten quite close. The next step is to make the parameter to Process() a monad instead of a plain function and lift operations on a connection to the monad. This way the user can't get a handle to the connection at all so there is no way have aliases. This is a fairly well known trick. I recall seeing posts on this on at least some O'Caml mailing list and, IIRC, on comp.lang.functional quite recently.

Thanks for the suggestion. I've been going through some of the documentation on Monads, and I understand the Haskell monad signature. I'm not familiar with type classes however, so I'm not sure how a Monad is implemented/overridden (or whatever the terminology might be). Does each instance of a monad need a custom implementation for bind, return, etc. or is a monad a simple polymorphic type?

Are you aware of any monad implementations in SML or OCaml? Or perhaps some demonstration code in C# or Java? I haven't been able to find anything that maps clearly to the Haskell monad signature at that link, so I'm having a bit of trouble mapping to C#.

Does each instance of a monad need a custom implementation for bind, return, etc.

Yes (in general; sharing may be possible in particular cases).

Are you aware of any monad implementations in SML or OCaml?

Take a look at the Syntax extension for Monads in Ocaml. Or, if you're comfortable with Scheme, try Oleg's Monadic Programming in Scheme.

The basic monad signature can be expressed in OCaml like this:

module type MONAD =
  sig
    type monad 'a = 'abstract;
    value unit : 'a -> monad 'a;
    value bind : monad 'a -> ('a -> monad 'b) -> monad 'b;
  end;

(That's using OCaml's revised syntax, because I was working with the new version of Camlp4 when I wrote this. Also, 'unit' is used instead of 'return' because of a keyword conflict in OCaml.)

The implementation of the identity monad would then look like this:

module Identity_Monad : MONAD =
  struct
    type monad 'a = 'a;
    value unit a = a;
    value bind m k = k m;
  end;

And here's a Maybe monad:

module type MAYBE_MONAD =
  sig
    include MONAD;
    value fail : monad 'a;
  end;

module Maybe : MAYBE_MONAD =
  struct
    type monad 'a = option 'a;
    value unit a = Some a;
    value fail = None;

    value bind m k = match m with
      [ None   -> None
      | Some x -> k x ];
  end;

Thanks for the very clear explanation. I've created monad interfaces and implementations of the identity and maybe monads in C# for my FP# library. I look forward to playing with monads to learn more. :-)

Perhaps of interest to others: the translation from a single module in OCaml ends up requiring two interfaces in C#. If C# permitted static methods on interfaces, only one interface would be needed. I'd appreciate any comments on the correctness of my implementation.

Edit: altered the implementation to use a single abstract base to reduce the boilerplate. Also added the Plus monad.

It's been discussed here before:

mutating types

Sing# shows clearly that the notion of type extends to individual values, as I have previously discussed here in LtU. Much of the problems that exist in today's mainstream languages is that they completely miss that concept. FP languages are vastly better in this domain.