Lambda the Ultimate

I know this is going to sound odd, but in my experience, only half of the value of typing is related to correctness. The other half that typing provides explicit, checkable, required documentation. Better, it's documentation that annotates the code inline and is intrinsically hyper-linked. Dynamic typing, soft typing, and even type-inference systems for strongly-typed languages all simply throw away the documentation value of types, or at best try to recreate it after the fact.

What makes you think inferring them is any worse at conveying information than explicitly writing them?

fun ensureInt x = x
val y = ensureInt 1.2

fun ensureInt (x : int) = x
val y = ensureInt 1.2

In the first case, the inference assumes that the function can be of any type. The second case will only allow an int. So if the intention of the function was to only allow integers, then inference will not restrict it to that type (ergo, the user has no documentation that the function should only take ints - ignoring the obvious name).

Oh, I see. In that case, you are correct, but you have to keep in mind those situations are rare and that type inference doesn't preclude type annotations when needed.

What makes you think inferring them is any worse at conveying information than explicitly writing them?

Because specifically written type annotations are always going to be more clear and more correctly expound the developers intent than inferred information. You may as well suggest that comments should be inferred from the code too. As much as clearly written code with good variable naming is, it isn't a complete replacement for suitable comments in terms of clearly documenting intent. Likewise, as good as inferred type information can be, it just isn't a replacement.

To put it another way, code documents, quite clearly, exactly what the program does, and good practice principles can help to make that easier to determine. What the code cannot, of itself, easily tell you, is what it is intended to do. You can, if you like, give hints with well chosen variable names, but in the end they can only ever be hints. With the addition of type annotations, contracts, and other documentation of programmer intent, things can rapidly become far clearer. Instead of having to infer details about the paramters that are to be passed to a function, you can read clearly documented statements about what the developer of the function intended. That clarity can be worth a lot.

Of course you don't always need this level of documentation; you might have a small team, or rather more discrete clearly delineated modules with little interaction, or any number of other things. On the other hand, there are a great many sorts of projects for which this sort of documentation is invaluable, and you'll often see it built in to languages designed for those sorts of large scale engineering projects: consider Ada package declarations, short forms for Eiffel classes, and even, I guess, things like JavaDoc (though I would suggest JMLDoc would be a better fit here really). There are reasons why languages like Ada are still preferred for large safety critical projects.

Because specifically written type annotations are always going to be more clear and more correctly expound the developers intent than inferred information.

No, not always. Explicit type annotations will sometimes be more specific, but more often than not they'll be the same in a system where type inference errs on the side of genericity. In such a system, the usual reasons for constricting the type to something other than what is inferred is either performance reasons or because the assumptions the inferencer makes are incorrect. The former is hardly ever a valid reason except in rare circumstances and the latter is due to incompatible types sharing an interface, e.g. 4%2 and "%s" % 2 in python. This can be solved by designing the interfaces in such a way that they aren't conflicting.

To put it another way, code documents, quite clearly, exactly what the program does, and good practice principles can help to make that easier to determine. What the code cannot, of itself, easily tell you, is what it is intended to do. You can, if you like, give hints with well chosen variable names, but in the end they can only ever be hints. With the addition of type annotations, contracts, and other documentation of programmer intent, things can rapidly become far clearer.

This is only partly true. You are correct in that code is susceptible to errors in communication, but that applies any time you try and convey something to the computer, including type annotations. What type annotations add is the concept of two layers of protection--by encoding what you mean twice, you might make it easier to spot discrepencies later on. I completely support this way of programming when it makes sense. For example, if you're working on a little project yourself it's likely you'll be able to spot type errors with or without them, so it generally doesn't matter then.

In such a system, the usual reasons for constricting the type to something other than what is inferred is either performance reasons or because the assumptions the inferencer makes are correct. The former is hardly ever a valid reason except in rare circumstances and the latter is due to incompatible types sharing an interface, e.g. 4%2 and "%s" % 2 in python. This can be solved by designing the interfaces in such a way that they aren't conflicting.

I'm fairly sure there are plenty of occasions where a suitably constructed set of descriptively named types, suitably constrained for the functions used, are going to add significant clarity and not simply be for optimization, nor to clarify syntactic interface confusion. I'm thinking, for example, of Ada's range types. There's also the matter of restricting the type simply to give it a different name as a matter of clarity of intent - that is, as documentation: this is the point you seem to ignore.

For example, if you're working on a project yourself on a little project it's likely you'll be able to spot type errors with or without them, so it generally doesn't matter then.

I would suggest, then, that rather than framing your argument as "why soft-typing is better", you may generate a little less heat and rather more light by discussing "in what roles is soft-typing the best choice?" Of course such a discussion would require a rather more detailed description of exactly what soft-typing system you are talking about.

(Fixed two types seen while reading your quotes. Thanks :)

I'm fairly sure there are plenty of occasions where a suitably constructed set of descriptively named types, suitably constrained for the functions used, are going to add significant clarity and not simply be for optimization, nor to clarify syntactic interface confusion. I'm thinking, for example, of Ada's range types.

That's correct, I'd forgotten about dependant types. Once you throw those in, the water starts to get a bit murky.

There's also the matter of restricting the type simply to give it a different name as a matter of clarity of intent - that is, as documentation: this is the point you seem to ignore.

That's usually accomplished by putting said function in a sutably named class, or inheriting from the class it's already in with a more descriptive class.

I would suggest, then, that rather than framing your argument as "why soft-typing is better", you may generate a little less heat and rather more light by discussing "in what roles is soft-typing the best choice?" Of course such a discussion would require a rather more detailed description of exactly what soft-typing system you are talking about.

Ah, but you see, I believe that soft typing is the best choice for all roles. I'll probably get a lot of flack for saying that, but I stand by it.

That's usually accomplished by putting said function in a sutably named class, or inheriting from the class it's already in with a more descriptive class.

I assume you're putting more context to this than I am, because that sounds like an overly general statement here.

An example would be something like specifying a measurement system. Basically, you'd just have a class for each kind, e.g. Feet, Inches, Meters, and have conversion functions in them. Along with adding documentation to the source code, it's also handy because the conversion functions come bundled with it.

You're still making assumptions, unless we're talking about a particular language. Classes rather than types would be a big example.

Type inference does nothing to indicate developer intent. It can only show you the actual semantics of the code. This is admittedly less of a loss of documentation value than in dynamic typing, but it's still problematic from a maintenance perspective. Often the only documentation on developer intent that a piece of legacy code has is type signatures and variable names (plus the odd comment that does more to obscure than illuminate).

Type inference does nothing to indicate developer intent. It can only show you the actual semantics of the code.

Correct.

Often the only documentation on developer intent that a piece of legacy code has is type signatures and variable names (plus the odd comment that does more to obscure than illuminate).

See my post above. Any interface with the computer is susceptible to communication errors, and type annotations and variable names are no exceptions. In small projects, it's generally easy enough to spot type errors without extra annotations, although they probably help enormously in larger projects.

I may have missed something in the terminology, but to me there is nothing in soft typing that says that it shouldn't involve declaring the types of functions. Actually I would think that becourse of the problems with inferencing types in such systems that it would be rather necissary.

My understanding is that such declarations were optional in soft-typing systems. "Optional" works out in practice to "your coworkers didn't bother when they were under deadline".

Yes it seems to be the standard, but i dont see anything inheritly in soft typing that says that it has to be this way.

This is also correct. I forgot to mention that soft typing doesn't necessarily imply optional type annotations. It's perfectly possible to having a softly typed language with explicit types, although I can't say I'd want to use it.

Some have proposed requiring type declaration of module singnatures, but leaving others optional. that might be a good compromise.

Well, that's roughly how people work with ML modules (as in SML and OCaml). The ML module system doesn't actually force you to write module signatures except for the formal parameters of functors. In practice, however, most people writing code in ML (including me) seem to explicitly write module signatures even when they are not using functors (and one reason for that is type abstraction).

This is also how the Erlang soft type system (linked elsewhere in this thread) works: an interface must be specified for modules, and the rest is done via inference. The difference, of course, is that if the interfaces aren't specified, then (I assume) there's no static typechecking.

This sort of thinking is deceptive. On the surface, it sounds perfectly logical, until you realize that, if you were to go around designing languages like this, it'd get to the point where you wouldn't be able to do anything useful with it to protect you from yourself! The added bit about the coworkers makes it sound a bit better, but again, this isn't something you can really design for. If you have inexperienced programmers, they're going to do inexperienced things. Type errors will not keep stupid programmers from writing stupid code, but rather the general community and coding standard will. For example, take a look at goto in C++: it's looked down upon so much that nobody dare use it, except the people who don't have any community interaction at all.

Of course, as has been pointed out before, if convention were sufficent, we wouldn't have types—and it's worth remembering that type theory didn't arise in programming in the first place, but arose to address incoherence in mathematical logic.

Richer type systems prevent whole classes of errors from happening to begin with (if you want to argue this point, don't bother; it isn't debatable, so if you—I mean the general "you," not Curtis—think it is, we won't be able to have a conversation about it). Static type systems enforce this prevention at the cost of rejecting some meaningful-but-not-typed-within-the-type-system programs. Soft type systems enforce this prevention where they can, allowing some meaningful-but-not-typed-within-the-type-system programs through, at the cost of allowing some meaningless-and-not-typed-within-the-type-system programs through, while dynamically-typed systems rely essentially entirely on the programmer for correctness. I see significant benefit to both static and soft typing over dynamic typing; where my questions lie revolves around how expressive the type systems are, how convenient they are to use, and how much control I have over what's considered an "error" vs. a "warning" in each system. Apart from that, I don't know what more there is to say, other than that I don't find O'Caml "inconvenient," I do find it extremely expressive, and I don't have any real-world soft type systems to compare with. This rather severely limits the extent to which I think I can fruitfully participate in this conversation—but that says precisely zip about whether the conversation has value in the general case or not.

Of course, as has been pointed out before, if convention were sufficent, we wouldn't have types—and it's worth remembering that type theory didn't arise in programming in the first place, but arose to address incoherence in mathematical logic.

Oh yes, I'm not saying that. Rather, I'm saying that forcing programmers to do something for their own good (or even for other people) doesn't work most of the time. What does work is, essentially, peer pressure, and that's something that you get with any language, explicit typing or not.

Oh yes, I'm not saying that. Rather, I'm saying that forcing programmers to do something for their own good (or even for other people) doesn't work most of the time. What does work is, essentially, peer pressure, and that's something that you get with any language, explicit typing or not.

I think you'll find, however, that the nature of the language, and the restrictions that it imposes, tends to inform the culture of the community that forms around the language. In theory Perl programmers could be every bit as disciplined and careful as Ada programmers (I'm sure there are some who are), but in practice that just isn't the case. As I said before, there are reasons why Ada is the preferred language for a lot of safety critical projects - perhaps you should consider what those reasons might be, and why, despite the fact that in principle you could just use Perl in a highly disciplined manner, people don't.

I think you'll find, however, that the nature of the language, and the restrictions that it imposes, tends to inform the culture of the community that forms around the language.

That's probably partly true, but I suspect the language itself doesn't have as much effect on the community as, say, the type of people the language attracts. I'd imagine the largest effect from the language isn't in what it restricts, but rather what facilities it provides. For example, lisp tends to attract fairly competent programmers because of its macros (and how mind-bending they can be), while OCaml tends to attract people who are concerned with correctness because of its rich type system.

and why, despite the fact that in principle you could just use Perl in a highly disciplined manner, people don't.

I have a friend (I use that term loosely) who would disagree with you, although I personally can't stand the language.

Curtis W: Rather, I'm saying that forcing programmers to do something for their own good (or even for other people) doesn't work most of the time.

This is very helpful; thanks for articulating this clearly.

I think this is a critical point, because IMHO it's true for the currently popular statically-typed languages—the C's, C++'s, Javas, C#'s, etc. of this world—but is orders of magnitude less true of the actual type-theoretic languages of this world—the MLs, Haskells, Epigrams, and so on. Heaven knows in my own travails I've just rolled my eyes at various things that I did to make the C++ or Java compiler happy. Sometimes it was relevant to the semantics of my software, sometimes it wasn't, and in any case it seemed capricious.

But my experience with O'Caml is totally different. At least 90% of the time, when I've "had to make the compiler happy," it really has been the case that I was trying to apply poorly-thought-out notions of typing from C++ or Java to a language that really "gets" types deeply. The question of downcasting is a good example: I spent a lot of time essentially trying to transliterate some C++ code using a factory class and downcasting to O'Caml and just couldn't make it work. After enough time of having it drilled into me that I was attempting to emulate variant types I broke down and used variant types, and the code got much cleaner, shorter, worked, and when I made mistakes refused to compile, instead of throwing exceptions at runtime. Then I needed to keep it extensible, which led me to polymorphic variants and eventually private row types, and now I really am talking about O'Caml-3.09-specific stuff that you could legitimately call "funky." :-) But it definitely keeps me working within the domain I'm addressing and in no way seems arbitrary or unhelpful or making-obeisance-to-the-stupid-compiler. That, I think, is the key difference between the heavily type-theory-based languages and the statically-typed-but-frustrating languages that we in the static type community are stuck with (commercially, anyway) today.

I think this is a critical point, because IMHO it's true for the currently popular statically-typed languages—the C's, C++'s, Javas, C#'s, etc. of this world—but is orders of magnitude less true of the actual type-theoretic languages of this world—the MLs, Haskells, Epigrams, and so on.

Definitely. I'm not saying that soft typing is immensely better than static typing. In fact, if there was a static version of python available (don't want .net) I'd gladly use it, although I have other problems with OCaml. As I've said before, really the only difference between OCaml's type system and soft typing, barring the type inferencer, is that you don't have to write code like this:

let value = match eval (get_input ()) with
`Int _ | `String _ as x -> x in
(* operate on value *)

But rather you can write code like this:

let value = eval (get_input ()) in
(* operate on value *)

Obviously this doesn't matter in cases where you need to do error checking, but it's fairly convenient when you're just writing a throw-away program or for RAD.

> I don't find O'Caml "inconvenient,"

Marc Stiegler and I are working on Emily - an object-capability variant of O'Caml. Most of the access control abstractions we've expressed in E can be expressed as easily in Emily, which is great. However, I see no way to express the membrane pattern[*] in Emily or O'Caml. If it can't be, this would be unfortunate, because many other access control abstractions build on essentially this pattern. The problem may not be specific to O'Caml, so let me pose it as a general challenge: Express the membrane pattern in any fully statically typed language. (I.e., languages like Java, with dynamic casts and reflection, don't count. In these languages, you can meet the challenge by escaping from the static type system.)

[*] Figure 9.3 on p.71 of http://www.cypherpunks.to/erights/talks/thesis/markm-thesis.pdf

(Btw, Paul, can you send me your email address? Mine is
erights -at- gmail.com
Thanks.)

Hi Mark! I haven't forgotten you or your thesis—just been busy with nasty work deadlines, parents' 50th anniversary, and trying to have a home life. :-) You can reach me at psnively -at- mac.com anytime.

OK, here's my initial cut, in O'Caml, with some additional comments, upon which I'll base my later full solution:

let membrane (x : 'a -> 'b) =
    let enabled = ref true
    in
      ((fun (y : 'a) -> if !enabled then x y else failwith "Disabled!"),
       (fun () -> enabled := true),
       (fun () -> enabled := false))

let protected, enabler, disabler = membrane (fun () -> Printf.printf "Testing, 1, 2, 3...\n")

# protected ();;
Testing, 1, 2, 3...
- : unit = ()
# disabler ();;
- : unit = ()
# protected ();;
Exception: Failure "Disabled!".
# enabler ();;
- : unit = ()
# protected ();;
Testing, 1, 2, 3...
- : unit = ()

let protected, enabler, disabler = membrane (fun x -> x + 5)

# protected 4;;
- : int = 9
# disabler ();;
- : unit = ()
# protected 4;;
Exception: Failure "Disabled!".
# enabler ();;
- : unit = ()
# protected 4;;
- : int = 9

The challenge isn't for static typing at all—it's for languages that don't support metaprogramming well. Obviously, the solution I've posted here is only good for functions taking a single argument and returning a single result. But of course, given an understanding of currying, it's obvious that it can, in principle, be extended to functions of arbitrary numbers of arguments. So the full O'Caml solution will have to be implemented as a syntax extension with camlp4. I intend to do this, and also to implement a full solution in Scala, taking advantage of its approach to syntactic extension, as a proof of concept/point of comparison.

You seem to have ignored the requirement to wrap the argument(s) and the return value of the wrapped procedure. That's where the static typing is going to really start hurting. Start ocaml with -rectypes and see how long it takes before your testing hangs during type inference... ;)

[Edit: not to mention the whole Ref.isData() thing, to which the easiest solution is something like a universal type...]

Heh. Good catch. The point is precisely that the requirement is to wrap function applications, and until I have the metaprogramming aspect of the problem solved, I can't do that (there's no way I can code the moral equivalent of isData() until then). In any case, as you can see, membrane is polymorphic on both the type of its parameter and its return type; there's no issue with wrapping any function from any type to any type with it.

I see the wink, but just to be quite clear: there's no need for recursive types in the solution; I'm completely confident that the problem can be solved with nothing more than induction on the AST and the appropriate application(s) of my membrane function.

Update: I feel somewhat vindicated already; I've confirmed that O'Caml desugars function applications with multiple arguments into applications of multiple functions of one argument anyway. There may be some trickiness I don't see yet around the return type; we'll see.

Update II: BTW, for those following along at home, it's relatively easy to fiddle around with O'Caml syntax interactively:

# #load "camlp4o.cma";;
        Camlp4 Parsing version 3.09.2

# #load "q_MLast.cmo";;
# let _loc = Lexing.dummy_pos, Lexing.dummy_pos;;
val _loc : Lexing.position * Lexing.position =
  ({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
    Lexing.pos_cnum = -1},
   {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
    Lexing.pos_cnum = -1})
# <:expr< x >>;;                      (* Give us the AST for the expression "x" *)
- : MLast.expr =
MLast.ExLid
 (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
    Lexing.pos_cnum = -1},
   {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
    Lexing.pos_cnum = -1}),
 "x")                                           (* AST for "literal id x," once you ignore pos info *)
# <:expr< (fun x y -> x + y) 4 5 >>;;
- : MLast.expr =
MLast.ExApp
 (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
    Lexing.pos_cnum = -1},
   {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
    Lexing.pos_cnum = -1}),
 MLast.ExApp
  (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
     Lexing.pos_cnum = -1},
    {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
     Lexing.pos_cnum = -1}),
  MLast.ExFun
   (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
      Lexing.pos_cnum = -1},
     {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
      Lexing.pos_cnum = -1}),
   [(MLast.PaLid
      (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
         Lexing.pos_cnum = -1},
        {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
         Lexing.pos_cnum = -1}),
      "x"),
     None,
     MLast.ExFun
      (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
         Lexing.pos_cnum = -1},
        {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
         Lexing.pos_cnum = -1}),
      [(MLast.PaLid
         (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
            Lexing.pos_cnum = -1},
           {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
            Lexing.pos_cnum = -1}),
         "y"),
        None,
        MLast.ExApp
         (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
            Lexing.pos_cnum = -1},
           {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
            Lexing.pos_cnum = -1}),
         MLast.ExApp
          (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
             Lexing.pos_cnum = -1},
            {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
             Lexing.pos_cnum = -1}),
          MLast.ExLid
           (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
              Lexing.pos_cnum = -1},
             {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
              Lexing.pos_cnum = -1}),
           "+"),
          MLast.ExLid
           (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
              Lexing.pos_cnum = -1},
             {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
              Lexing.pos_cnum = -1}),
           "x")),
         MLast.ExLid
          (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
             Lexing.pos_cnum = -1},
            {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
             Lexing.pos_cnum = -1}),
          "y")))]))]),
  MLast.ExInt
   (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
      Lexing.pos_cnum = -1},
     {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
      Lexing.pos_cnum = -1}),
   "4")),
 MLast.ExInt
  (({Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
     Lexing.pos_cnum = -1},
    {Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_bol = 0;
     Lexing.pos_cnum = -1}),
  "5"))

I haven't looked at this challenge in great detail (and I don't have the time right now), but if I'm reading the challenge correctly, then this problem of implementing membranes seems to be very similar to that of implementing something like serialization in a statically typed language. You are essentially given a type and you need to generate a wrapper (or membrene) for values of that type such that access to a value of the type can be enabled/disabled at run-time. The solution is essentially a type-indexed family of functions.

To implement a type-indexed family of functions in ML, I wouldn't start with a syntax extension, but with a combinator library. (In Haskell, one might go with a type class based solution.)

Here are a couple of pointers to articles on writing such combinator libraries: serialization, Embedded Interpreters, Embedding an Interpreted Language Using Higher-Order Functions and Types. There are many more.

Andreas beat me to posting a solution, but since I also wrote one (mostly on Sunday on a train, actually), I'll post it anyway. This is a bit more complete than Andreas' solution. In particular, this version supports defining membranes over an arbitrary number of mutually recursive datatypes. This is interesting in the sense that Kennedy's article on pickler combinators remarks that one needs to have a family of fixpoint combinators fix_n, which is unsatisfactory (it violates the Open-Closed Principle). This solution avoids the problem by using a kind of type-indexed fixpoint combinator. Finally, the Membrane.make function below simply takes a bool ref as an argument.

(* First some utilities. *)
fun const x _ = x
fun cross (f, g) (x, y) = (f x, g y)
fun dup x = (x, x)
fun id x = x
fun fail e _ = raise e
fun refFn rf = fn x => !rf x

datatype ('a, 'b) alt = INL of 'a | INR of 'b
fun pipe (f, g) = fn INL a => INL (f a)
                   | INR b => INR (g b)

datatype ('a, 'b) product = & of 'a * 'b
infix &

type ('a, 'b) embedding = ('a -> 'b) * ('b -> 'a)
type 'a uop = 'a -> 'a
type 'a fix = 'a uop -> 'a
type 'a thunk = unit -> 'a
type 'a effect = 'a -> unit

(* An extensible fixpoint mechanism. *)
signature FIX =
  sig
    type ('s, 'k) t
    val fix : ('a, 'b) t thunk -> 'b fix
    val tier : {new : 's thunk,
                knot : 's -> 'k,
                tie : ('s * 'k) effect}
               -> ('s, 'k) t
    val ^ : ('a, 'b) t thunk * ('c, 'd) t thunk
            -> (('a, 'c) product,
                ('b, 'd) product) t thunk
  end

structure Fix :> FIX =
  struct
    datatype ('s, 'k) t =
             T of {new : 's thunk,
                   knot : 's -> 'k,
                   tie : ('s * 'k) effect}

    fun fix t f =
        let val T {new, knot, tie} = t ()
            val slot = new ()
            val knot = f (knot slot)
        in tie (slot, knot)
         ; knot
        end

    val tier = T

    fun lt ^ rt =
        fn () =>
           let val T lt = lt ()
               val T rt = rt ()
           in T {new = fn () =>
                          #new lt () & #new rt (),
                 knot = fn ls & rs =>
                           #knot lt ls & #knot rt rs,
                 tie = fn (ls & rs, lk & rk) =>
                          (#tie lt (ls, lk)
                         ; #tie rt (rs, rk))}
           end
  end

(* Membranes *)
infixr -->

signature MEMBRANE =
  sig
    type 'a t

    exception Membrane

    val make : 'a t -> bool ref -> 'a uop

    val iso : ('a, 'b) embedding -> 'b t -> 'a t

    val T : ((bool ref -> 'a uop) ref, 'a t) Fix.t thunk

    val unit : unit t
    val bool : bool t
    val int : int t
    val real : real t
    val string : string t

    val + : 'a t * 'b t -> ('a, 'b) alt t
    val * : 'a t * 'b t -> ('a, 'b) product t

    val list : 'a t -> 'a list t
    val option : 'a t -> 'a option t

    val --> : 'd t * 'r t -> ('d -> 'r) t
  end

structure Membrane :> MEMBRANE =
  struct
    datatype 'a t = IN of bool ref -> 'a uop

    exception Membrane

    fun make (IN a) = a

    fun iso (a2b, b2a) (IN b) =
        IN (fn e => b2a o b e o a2b)

    fun T () =
        Fix.tier
          {new = fn () => ref (fail (Fail "fix type")),
           knot = fn fe => IN (refFn fe),
           tie = fn (fe, IN fe') =>
                    fe := (fn e =>
                              let val fx = ref (fail (Fail "fix value"))
                              in fe := const (refFn fx)
                               ; fx := fe' e
                               ; !fx
                              end)}

    local
      val data = IN (fn _ => id)   (* One might also want to expose this. *)
    in
      val unit = data
      val bool = data
      val int = data
      val real = data
      val string = data
    end

    local
      fun mk f (IN a) = IN (f o a)
    in
      (* These don't actually have to be primitive. *)
      fun list ? = mk List.map ?
      fun option ? = mk Option.map ?
    end

    local
      fun mk f (IN l, IN r) = IN (f o cross (l, r) o dup)
    in
      fun op + ? = mk pipe ?
      fun op * ? = mk cross ?
      val op * = fn ? => iso (fn a & b => (a, b),
                              fn (a, b) => a & b)
                             (op * ?)
    end

    fun (IN d) --> (IN r) =
        IN (fn e =>
               let val d = d e
                   val r = r e
               in fn f =>
                     r o f o
                     (fn x => if !e then d x
                              else raise Membrane)
               end)
  end

Here is an example:

datatype re   = A of int -> real uop
              | B of sive * cur * int
              | C of cur
     and cur  = D of int -> real | E of sive
     and sive = F of re | G

fun uop t = let open Membrane in t --> t end

val re & cur & sive =
    let open Fix Membrane
    in (fix (T^T^T))
         (fn re & cur & sive =>
             iso (fn A a => INL (INL a)
                   | B (b1, b2, b3) => INL (INR (b1 & b2 & b3))
                   | C c => INR c,
                  fn INL (INL a) => A a
                   | INL (INR (b1 & b2 & b3)) => B (b1, b2, b3)
                   | INR c => C c)
                 ((int --> uop real) + sive * cur * int + cur) &
             iso (fn D d => INL d | E e => INR e,
                  fn INL d => D d | INR e => E e)
                 ((int --> real) + sive) &
             iso (fn F f => INL f | G => INR (),
                  fn INL f => F f | INR () => G)
                 (re + unit))
    end

val enabled = ref true
val foo = Membrane.make cur enabled (E (F (A (fn i => fn r => r + real i))))

My point about recursive types was just that if you take your conversion of the original function one obvious step further, to include the wrapping of the argument and the return value, you naturally end up with something like this:

let membrane (target : 'a -> 'b) =
  let rec enabled = ref true
  and wrap f (x : 'a) = if !enabled then wrap (f (wrap x)) else failwith "disabled"
  in wrap target, (fun () -> enabled := true), (fun () -> enabled := false)

...which won't type, because the recursive call to 'wrap' on the return value of f has no base case to stop infinite regression. To experience the full effect of this problem, you have to run ocaml with -rectypes, otherwise you just get a misleadingly benign type error. That's the only sense in which recursive types are relevant, i.e. I wasn't suggesting that they're part of the solution here.

This issue corresponds to the currying issue which you say you're going to solve with camlp4. However, since the wrapping is dynamically associated with functions on which 'membrane' has been called, camlp4 seems of limited use here, except possibly to sugar a solution involving e.g. tagged values. Perhaps that's what you have in mind, but then you're essentially implementing a little dynamic language, which seems to me like more of an exercise in Turing completeness than a way to statically type this problem. For example, we might do this:

type e_val = Func of (e_val -> e_val) | Val of int

let membrane target =
  let rec enabled = ref true
  and wrap = function Func f -> Func (wrap_fun f) | Val x  -> Val x
  and wrap_fun f = fun x -> if !enabled then wrap (f (wrap x)) else failwith "disabled"
  in wrap target, (fun () -> enabled := true), (fun () -> enabled := false)

This version works, it fully and correctly wraps its arguments, and handles functions with multiple (curried) arguments, albeit by using the impoverished e_val type (which could of course easily be extended).

Now you could use camlp4 to sugar the usage of e_val in client code, but that would create a nice little dynamically-typed language, and I doubt you'd be able to sleep soundly after that!

I think Vesa's point boils down to something similar, i.e. you're looking at a solution which involves embedding dynamic language features. However, the difference compared to the serialization case is that a membrane potentially affects function calls throughout a program, not just at the "edges" of the program where serialization and deserialization occurs.

My point was just that, once you realize that all O'Caml functions are functions of a single argument with a single result under the hood, and that the protection function around the function passed to the membrane can be polymorphic in both its argument and its return type, 99% of the rest of the solution is just folding an N-argument function application's AST into the membrane function. The only bit that I still have to put some thought into is the function's return type. I don't think I can determine whether the return type is a function type at pre-processing time, so I either need to a) wrap it anyway, or b) find a way to determine at compile time whether it's of a function type or not, only wrapping if it is. Perhaps there's a way with the module system, but I'm not going to dig into that until I know I have to.

In any case, my even larger point remains: this isn't a typing problem; it's a metaprogramming problem (and in fact, if I knew MetaOCaml better, I might just bail and solve the problem in it). Your e_val solution isn't polymorphic, as I think you alluded to, and isn't transparent to client code, as you said. The major point of the code I posted was that, given a function of one argument, you can indeed wrap it transparently, and since all functions in O'Caml are of one argument, by definition you can wrap them transparently. There's no need to deal with recursion in the type system; the recursion we're interested in occurs in dealing with the syntax, as the fact that O'Caml functions of N arguments are always converted to N functions of one argument via syntactic transformation attests. The syntax also tells us whether we're dealing with a function application or not, at least for the argument, but again, not for the return value (obviously—you can identify a function application syntactically, but the return type doesn't exist yet), so if there's going to be hair anywhere, it'll be there, and that may be sufficient to necessitate a move to MetaOCaml. But even if it does, the problem still won't be a static typing problem. :-)

The major point of the code I posted was that, given a function of one argument, you can indeed wrap it transparently, and since all functions in O'Caml are of one argument, by definition you can wrap them transparently.

The problem is that the code you posted was incomplete in an important respect: it didn't deal with wrapping the return value. As such, it will only show what you claim it shows once you've also shown how to wrap the return value (and, for that matter, the argument).

The only bit that I still have to put some thought into is the function's return type.

Indeed. :oP

The syntax also tells us whether we're dealing with a function application or not, at least for the argument, but again, not for the return value (obviously—you can identify a function application syntactically, but the return type doesn't exist yet), so if there's going to be hair anywhere, it'll be there

You've correctly identified the source of hair, and also why camlp4 won't let you cut that hair.

In any case, my even larger point remains: this isn't a typing problem; it's a metaprogramming problem
[...]
and that may be sufficient to necessitate a move to MetaOCaml. But even if it does, the problem still won't be a static typing problem. :-)

The issue may be on a blurry boundary of static types and metaprogramming, but static types are certainly a big part of it. Consider the following as a dynamically-typed program (non-essentials elided):

let wrap x = if is_data(x) then x else (fun y -> wrap (x (wrap y)))

This works fine in a dynamically-typed language, because the is_data test allows an exit from the recursion of wrap. In my earlier example, the e_val type's Val base case served the same purpose.

Now imagine that OCaml had an is_data function (incidentally violating MarkM's prohibition on reflection). The above code still wouldn't type correctly — try writing out its OCaml type. Being able to reflect on data isn't enough by itself.

You're trying to avoid these problems by avoiding the recursive calls to wrap, but that simply means that your function doesn't do what it's supposed to do — it makes membranes with holes. Attempting to correct your function's semantics by applying a syntactic transformation (particularly from outside the function) is addressing the problem at the wrong level, and will only end up more complicated than it would otherwise be. To resolve the problem, you have to address the static typing issues, one way or another.

Anton van Straaten: You're trying to avoid these problems by avoiding the recursive calls to wrap, but that simply means that your function doesn't do what it's supposed to do — it makes membranes with holes. Attempting to correct your function's semantics by applying a syntactic transformation (particularly from outside the function) is addressing the problem at the wrong level, and will only end up more complicated than it would otherwise be. To resolve the problem, you have to address the static typing issues, one way or another.

First, let's stipulate everything above this; I think we're basically on the same page.

I'm avoiding the recursive calls to wrap because they don't need to be recursive in the sense of wrap being universally quantified or somehow "instantiated" per type of function that it's wrapping; it's sufficient to have a polymorphic wrap given the parameter type and return type of the function being wrapped. The only reason I might have to care about a universally-quantified wrap is because of the unavailability of one, the other, or both of those types. So my thesis is that attempting to create such a recursive wrap is operating at the wrong level due to a weak metaprogramming system—make the type information available at compile time and that complexity goes away completely. A wrap that is parameterized by the types that it wraps, or one that uses universal quantification—those sound like the "more complicated than it would otherwise be" parts to me. But talking about metaprogramming vs. higher-order types... hmmm... I think my Lisp roots are showing. ;-)

I'm avoiding the recursive calls to wrap because they don't need to be recursive in the sense of wrap being universally quantified or somehow "instantiated" per type of function that it's wrapping; it's sufficient to have a polymorphic wrap given the parameter type and return type of the function being wrapped.

What kind of polymorphism are you thinking of here? The reason I ask is that one way or another, in addition to wrapping the function itself, you need to wrap the argument to the function, as well as wrap the function's return value, i.e. three wraps need to take place, each wrapping values with potentially different types. This is similar to the problem of creating a three-element list containing three different types of value: also something that you can't do with a plain Hindley-Milner polymorphic type such as 'a list.

So my thesis is that attempting to create such a recursive wrap is operating at the wrong level due to a weak metaprogramming system—make the type information available at compile time and that complexity goes away completely.

I agree that that the recursive wraps that I've given are "operating at the wrong level", in the sense that they result in having to use tagged unions throughout the code, when you really want the membrane feature to be more transparent. To make it more transparent, you can build the feature into the language. However, this comes back to the exercise in Turing completeness which I mentioned earlier. The challenge isn't whether it's possible to design a statically-typed language which supports membranes — I'm sure that's possible. The question is whether you can implement membranes reasonably in a statically-typed language such as OCaml.

Because of the issues I've raised, I'm theorizing that any solutions with camlp4 or MetaOCaml are not going to be simple tweaks, such as some kind of type-parameterized template to generate membranes — that won't work, because the results of any syntactic transformation still have to operate within the OCaml type system, and will face the same problems. Rather, solutions will be pervasive ones involving global transformation, creating a language with greater expressive power, in the Felleisen sense, than OCaml.

Anton van Straaten: The question is whether you can implement membranes reasonably in a statically-typed language such as OCaml.

Quite right, so my response is: is using camlp4 or MetaOCaml "reasonable?" In some respects, this challenge strikes me as somewhat unfair; the E code conflates operating on ASTs, reflection, and dynamic typing, but the statically-typed code must eschew operating on ASTs and reflection? Another question is: since wrapping functions vs. not wrapping data is an optimization, rather than affecting observational equivalence, it seems like I should be able to ignore it. If I don't need to determine whether a parameter or result type is a function or not, then it really does come down to a simply polymorphic membrane-building function of one argument that a relatively simply syntax extension can apply to any decurried function at all.

Anton van Straaten: Because of the issues I've raised, I'm theorizing that any solutions with camlp4 or MetaOCaml are not going to be simple tweaks, such as some kind of type-parameterized template to generate membranes — that won't work, because the results of any syntactic transformation still have to operate within the OCaml type system, and will face the same problems.

I strongly suspect that this isn't true: at the pre-processing level, it seems to me that I can wrap a function with type 'a -> 'b around the parameter to the passed function, the return value of the passed function, and the passed function itself, and since I'm doing it at pre-processing time, by the time the compiler sees it, it will infer three distinct (but potentially equal) instantiations of 'a and 'b, without conflicts. In other words, type variables at pre-processing time should (I think!) be quite analogous to using gensyms to achieve hygiene in traditional Lisp (vs. Scheme!) macrology. But this hypothesis remains to be tested.

Anton van Straaten: Rather, solutions will be pervasive ones involving global transformation, creating a language with greater expressive power, in the Felleisen sense, than OCaml.

That might be true—my immediate reaction to Mark upon seeing the challenge the first time was to make the general observation that to do object-capability security in a statically-typed language might require so rich a type system as to require dependent types. Oleg Kiselyov and Chung-chieh Shan's Lightweight static capabilities tends to support this view by applying their work on lightweight dependent types to the question of capabilities, but I don't see a direct solution to the membrane pattern in the paper, and I haven't yet attempted to construct such a solution based on their work myself. Perhaps that would be a more fruitful approach than a metaprogramming solution. As I said, I think my Lisp roots are showing!

Quite right, so my response is: is using camlp4 or MetaOCaml "reasonable?"

I'm not saying you can't use those tools, but if you have to use them to do global transformations to e.g. hide tagged unions under the hood, then you're designing a new language. Such a language would need to have its data types marshalled in order to interoperate with ordinary OCaml code, for example — you couldn't just open a module in an ordinary OCaml program and create or use membranes. To me, that's not solving the challenge as stated. If it were, then my solution with e_val already does something similar, and could be sugared and even type inferenced in order to turn it into a statically-typed, membrane-supporting language. If that's a valid solution, then it's already been sketched with sufficient detail to be completed without requiring any invention, and MarkM should be happy. But that's just a case of implementing one Turing-complete language using another, which isn't very interesting.

As I see it, the challenge would be solved if you could implement a solution of the kind described here:

Anton van Straaten: Because of the issues I've raised, I'm theorizing that any solutions with camlp4 or MetaOCaml are not going to be simple tweaks, such as some kind of type-parameterized template to generate membranes — that won't work, because the results of any syntactic transformation still have to operate within the OCaml type system, and will face the same problems.

I strongly suspect that this isn't true: at the pre-processing level, it seems to me that I can wrap a function with type 'a -> 'b around the parameter to the passed function, the return value of the passed function, and the passed function itself, and since I'm doing it at pre-processing time, by the time the compiler sees it, it will infer three distinct (but potentially equal) instantiations of 'a and 'b, without conflicts.

However, you haven't given enough detail for me to see how you plan to do this. All you really need to do is show what the generated OCaml code for the full wrapping of a procedure, its argument, and its return value would look like. The actual implementation in camlp4 or MetaOCaml ought to be an implementation detail.

As one example of what hasn't been made clear, it sounds as though you're suggesting wrapping arguments and return values at the site of an application, as opposed to inside the wrapped function. However, in order to do that, you have to test whether the function being applied has been wrapped. Whether a function is wrapped or not is a dynamic property, though, at least in the OCaml type system. So you're presumably going to need function values to be tagged to indicate whether they're wrapped, and then you'll need to generate code which will test a function for wrapped-ness and conditionally wrap the argument and return value. That code has to exist at runtime, i.e. it can't be optimized away at compile time, unless you're planning on developing an entire static typing system that can statically determine whether a function is wrapped. So now you're talking about something in which values are packaged in tagged unions, and sugar is needed to make client code usable — very much like the solution I gave. What's the distinction? Again, if that's a solution, then the problem has already been solved.

In some respects, this challenge strikes me as somewhat unfair; the E code conflates operating on ASTs, reflection, and dynamic typing, but the statically-typed code must eschew operating on ASTs and reflection?

The challenge highlights a limitation of certain classes of static type systems. If you design an augmented type system which overcomes the limitation, you still haven't addressed the limitation of the original class of type system.

First, I'll strive for brevity by stipulating everything that I don't quote. Second, Anton, thanks for an extremely helpful and informative discussion—this is exactly why I love LtU. I feel like I'm finally actively contributing to work towards a meaningful understanding of the intersection static typing, dynamic typing, and metaprogramming, all in a context that I'm passionate about—capability security. It's very exciting!

Anton van Straaten: However, you haven't given enough detail for me to see how you plan to do this. All you really need to do is show what the generated OCaml code for the full wrapping of a procedure, its argument, and its return value would look like. The actual implementation in camlp4 or MetaOCaml ought to be an implementation detail.

As one example of what hasn't been made clear, it sounds as though you're suggesting wrapping arguments and return values at the site of an application, as opposed to inside the wrapped function.

Excellent points, and you're right; I was allowing myself to become confused by the need to determine whether an argument was a function or not as to when I could do that. So I do need to change my focus to function definition time rather than function application time. But the point is moot—I can no more determine whether the return value is of function type at definition than I can at application time. I'm still not satisfied that this matters—again, it's a performance optimization as to whether data gets wrapped or not—but it's worth trying to implement the exact pattern, optimizations and all.

Anton van Straaten: The challenge highlights a limitation of certain classes of static type systems. If you design an augmented type system which overcomes the limitation, you still haven't addressed the limitation of the original class of type system.

I may have misunderstood the challenge; I took Mark to mean "here's a challenge for any static type system," not "here's a challenge for extant statically-typed languages X, Y, and/or Z." A little reflection on the pattern strongly suggests that it could be easily typed even in the simply-typed lambda calculus given the ability to perform a semantics-preserving source-to-source transformation on a decurried function definition, and I continue to believe this: the only thing stopping me is the lack of return-type information at pre-processing time in camlp4, and that's only due to the performance optimization of checking to see whether an argument or return value is a function or not—if I can just wrap everything, the challenge disappears. "Checking to see whether an argument or return value is a function" sure sounds like reflection to me, and hence sounds like it's about metaprogramming, because there are areflective dynamic languages as well as reflective static ones. So the next natural step would be to explore the pattern in MetaOCaml, and I may very well do just that. If nothing else, it would be interesting to see the extent to which metaprogramming with a relatively simple type system might allow one to express things that, lacking such a metaprogramming facility, require a considerably more powerful type system, or at least a considerably more complex embedding in the simpler type system.

In any case, I want to be clear that if the claim wasn't "you can't do this in any static type system," but rather was "you can't easily do this in most extant static type systems," then, as usual, we agree—but then, I hope no one thinks I'm a big fan of most extant static type systems by this time! :-)

So I do need to change my focus to function definition time rather than function application time.

It might be worth re-examining my earlier code examples now, since they're very relevant to what you need to do. Note that it's function wrapping time that's actually important, i.e. no matter how you do it, there's stuff you need to do somewhere inside the implementation of 'membrane'.

But the point is moot—I can no more determine whether the return value is of function type at definition than I can at application time.

Which is precisely why and where tags come in.

I'm still not satisfied that this matters—again, it's a performance optimization as to whether data gets wrapped or not—but it's worth trying to implement the exact pattern, optimizations and all.

It sounds as though you might be ignoring the need for a base case. Look at my example using e_val: there needs to be a case to handle function values and a case to handle data values. The latter is critical, as a base case, to prevent runaway recursion. This has nothing to do with performance optimizations. IMO, the comment in Mark's code ("don't bother wrapping it") is a little misleading — it only looks like a performance optimization because the tagging is hidden in the language implementation, and because the algorithm wasn't expressed using an obvious pattern match on the type.

Besides, wrapping data has other bad consequences — changing its type, for a start. Even if you could get around that issue, you'd still a need a separate case for it, and a way to distinguish it from wrapped functions, since data doesn't take arguments, so both its wrapping and unwrapping would be different.

I know you want to say that all this pesky machinery shouldn't be necessary, and I'm perfectly willing to stop insisting that it is, as soon as I see a sketch of a plausible mechanism to avoid it.

Regarding the nature of the challenge, I have no special insight into what Mark had in mind. However, I distinguish between three situations:

1. Implementing membranes within an existing static type system, in a usable way (e.g. it's not usable if all values have to become tagged unions). I interpreted Mark's challenge as asking about a way to do this, and I've been arguing that this isn't really possible.
2. Implement membranes using a tagged union (or "the moral equivalent") and sugaring it to be more palatable. This amounts to building the membrane pattern into the type system of a new language. The resulting language and its type system may still not allow the membrane pattern to be transparently implemented within the language, but that doesn't matter because the feature is already built into the language. If Mark's goal is simply to come up with a statically-typed version of E, then at least w.r.t. the membrane issue, this option is perfectly viable. If you're talking about a solution like this, then I agree it's possible, even easy.
3. Find or implement a type system which is capable of expressing membranes "within" the system (as in point 1) in a transparent way, i.e. not requiring a global transformation of client code. I believe this will need significant features beyond what a Hindley-Milner style system provides, and we haven't really been discussing this, afaict. This option might be interesting as an exercise in advanced type systems, but it doesn't seem necessary w.r.t. the requirements of E.

the only thing stopping me is the lack of return-type information at pre-processing time in camlp4

The only thing stopping you is the issue of handling the return type, period. Forget camlp4 or MetaOCaml, they're just distractions at this point. If the generated code will ultimately be OCaml, then you should be able to construct an example in pure OCaml. That'll allow you to ignore any limitations which camlp4 might have, and focus on solving the underlying problem.

if I can just wrap everything, the challenge disappears.

Easy as that, huh? If so, an example would be nice.

Implementing membranes within an existing static type system, in a usable way (e.g. it's not usable if all values have to become tagged unions). I interpreted Mark's challenge as asking about a way to do this, and I've been arguing that this isn't really possible.

As Vesa already pointed out, this is a simple instance of a type-indexed function. Even in the absence of more advanced features like intentional type analysis, such functions can be simulated with suitable combinators. So here is a simple solution in plain SML (if I understand the problem correctly):

exception Membrane

fun bool flag b = b
fun int flag n = n
fun (t1*t2) flag (x1,x2) = (t1 flag x1, t2 flag x2)

infixr -->
fun (t1-->t2) flag f x =
    if !flag
    then t2 flag (f (t1 flag x))
    else raise Membrane

fun membrane t x =
    let
	val enabled = ref true
    in
	(t enabled x, fn() => enabled:=true, fn() => enabled:=false)
    end

Obviously, this approach is extensible and does not require any tagging.

Here is a sample transcript demonstrating higher-order membranes:

> val (inc,enInc,disInc) = membrane(int-->int) (fn i=>i+1);
val inc : int -> int = _fn
val enInc : unit -> unit = _fn
val disInc : unit -> unit = _fn
> val (dec,enDec,disDec) = membrane(int-->int) (fn i=>i-1);
val dec : int -> int = _fn
val enDec : unit -> unit = _fn
val disDec : unit -> unit = _fn
> inc(dec 4);
val it : int = 4
> disInc();
val it : unit = ()
> inc(dec 4);
Uncaught exception
   Membrane
> enInc();
val it : unit = ()
> inc(dec 4);
val it : int = 4
> fun compose f g x = f(g x);
val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = _fn
> val (compose',enCompose,disCompose) = membrane((int-->int)-->(int-->int)-->int-->int) compose;
val compose' : ('2 -> '3) -> ('4 -> '2) -> '4 -> '3 = _fn
val enCompose : unit -> unit = _fn
val disCompose : unit -> unit = _fn
> val id = compose' inc dec;
val id : int -> int = _fn
> id 4;
val it : int = 4
> disCompose();
val it : unit = ()
> id 4;
Uncaught exception
   Membrane
> disInc();
val it : unit = ()
> id 4;
Uncaught exception
   Membrane
> enCompose();
val it : unit = ()
> id 4;
Uncaught exception
   Membrane
> enInc();
val it : unit = ()
> id 4;
val it : int = 4

As Vesa already pointed out, this is a simple instance of a type-indexed function. Even in the absence of more advanced features like intentional type analysis, such functions can be simulated with suitable combinators. So here is a simple solution in plain SML (if I understand the problem correctly)

That's an extremely cool solution — thanks for taking the time to do the example, without which it probably still wouldn't have sunk in for me. It's a nice example of "any problem can be solved by adding an extra layer of indirection", with the added benefit in this case that the indirection can presumably be optimized away at compile time. I hadn't realized that type-indexed functions required so little type system machinery.

Nothing new here, just using type classes. It may be cleaner to have separate classes to use for values and actions so that the actions one could have the type: checkAction :: MembraneAction b => IORef Bool -> (a -> IO b) -> a -> IO b which is probably more convenient, though this would take some (mild) HList style type hackery to avoid overlapping instances. I did a similar translation here with regards to the Embedded Interpreter's paper Vesa referenced.

import Data.IORef

class Membrane t where
    check :: IORef Bool -> t -> IO t

instance Membrane Int where
    check ref x = return x

instance Membrane Bool where
    check ref x = return x

instance (Membrane a, Membrane b) => Membrane (a,b) where
    check ref (a,b) = liftM2 (,) (check ref a, check ref b)

instance (Membrane a, Membrane b) => Membrane (a -> IO b) where
    check ref f = do
        enabled <- readIORef ref
        if enabled then
            return (\x -> check x >>= f >>= check)
          else
            fail "disabled"

membrane :: Membrane t => t -> IO (IO t, IO (), IO ())
membrane x = do
    ref <- newIORef True
    return (check ref x, setIORef True, setIORef False)

#2 isn't relevant because membranes would then be a primitive of this new language. The issue isn't membranes specifically. The issue is the ability to support access control abstraction patterns. If the membrane can't be implemented in the new language, then membrane-like patterns still wouldn't be available in the new language.

The solution which Andreas posted seems to meet the challenge. It should work in just about any statically typed functional language, since it needs nothing more than ordinary combinators. (The example defined a couple of infix operators, but they can also just be defined as ordinary functions.)

It also looks as though it ought to be very efficient, since a call to 'membrane' to wrap a function f should compile down to a function containing nothing more than (back in OCaml):

fun x -> if !flag then f x else failwith "Disabled"

I haven't verified that a compiler will actually do that, but the transformation looks straightforward enough, and everything needed to reduce to the above form is statically known at the time 'membrane' is called to wrap a function.

Yep, this is cool. I can't honestly say that I understand it completely—do I need to define "flag" for every type? If so, how does that actually solve the problem transparently? But clearly this works for the types defined, and I may simply be misunderstanding the implementation.

I see we also have a preliminary result in Haskell. This is exciting, and exactly what I hoped to see after my Let's Do It! post!

Yes, you need to define one function for every type. In the example, those functions are named after the type, and 'flag' is just an argument, not a function. Note that the functions themselves don't know anything about the type they correspond to [they all have type 'a -> 'b -> 'b]. They just give the type system something to discriminate on. (Thus taking care of the return type issue I was going on about!)

Re transparency, my concern was whether things like values and function applications would have to be wrapped. That's not the case here. Since only one function needs to be defined per type, it seems transparent enough to me. If a user needs a type which hasn't already been defined, they can simply define it. Also, there are various ways you could support something like this more directly in a language (back to MetaOCaml now...)

Here's an OCaml version. I haven't bothered to define the tuple type function, which wasn't being used, and I hastily prepended @ to the arrow to make it right associate. I blame any resulting ugliness on OCaml. ;)

let bool flag b = b
let int flag n = n

let (@-->) t1 t2 flag f x =
    if !flag
    then t2 flag (f (t1 flag x))
    else failwith "Disabled"

let membrane t x =
    let enabled = ref true
    in t enabled x, (fun () -> enabled := true), fun () -> enabled := false

let (inc,enInc,disInc) = membrane (int @--> int) (fun i -> i+1)
let (dec,enDec,disDec) = membrane (int @--> int) (fun i -> i-1)
let compose f g x = f(g x)
let (compose',enCompose,disCompose) = membrane ((int @--> int)@-->(int @--> int) @--> int @--> int) compose
let id = compose' inc dec

See Encoding Types in ML-like Languages, which is extremely educational, at least to me.

Update: Earlier on LtU, TypeCase: A Design Pattern for Type-Indexed Functions, which cites "Encoding Types in ML-like Languages."

FYI, I just wrote the following note on combining type-indexed values using functors in Standard ML. It addresses a limitation of the so called value-dependent encoding of type-indexed values in ML.

Anton van Straaten: Note that the functions themselves don't know anything about the type they correspond to [they all have type 'a -> 'b -> 'b]. They just give the type system something to discriminate on. (Thus taking care of the return type issue I was going on about!)

Right—the whole approach is described quite well in "Encoding Types in ML-like Languages," which I link to here. Very clever!

Anton: Re transparency, my concern was whether things like values and function applications would have to be wrapped. That's not the case here. Since only one function needs to be defined per type, it seems transparent enough to me. If a user needs a type which hasn't already been defined, they can simply define it. Also, there are various ways you could support something like this more directly in a language (back to MetaOCaml now...)

That's what I want to know: what next? We've got some good sketches, I think, but let's be honest; what we really want to be able to write is just "let membrane, enabler, disabler = make_membrane (my_function)" and have it work. If I understand "Encoding Types in ML-like Languages" correctly, this can be done just with Hindley-Milner type inference with a little care, but it's also amenable to a multi-stage solution a là MetaOCaml as well as a higher-order polymorphism (modules/typeclasses) solution. The latter sounds to me a lot like what Oleg Kiselyov and Chung-chieh Shan did in Lightweight Static Capabilities, but I'm not entirely sure that they're equivalent.

Anton: Here's an OCaml version. I haven't bothered to define the tuple type function, which wasn't being used, and I hastily prepended @ to the arrow to make it right associate. I blame any resulting ugliness on OCaml. ;)

Rightly so—O'Caml's handling of operator association is lame.

Can you do compose' polymorphically, or do you need a version for every combination of types?

The examples posted by Andreas, and my OCaml version of that, require a version for every combination of types.

I don't think you can make it polymorphic, because membrane is a stateful abstraction. State and polymorphism do not mix well, and the problem here is somewhat akin to ML's value restriction.

This does not mean that you cannot make type-indexed functions polymorphic in general - you just have to make the "type" parameters explicit.

We don't really require a version for every combination of types, do we? We use the type-indexing only to keep track of whether a value is functional, right? So rather than int, bool, etc., we can just define a single "prim" or "atom" combinator, and then we only need to define a compose membrane for each separate functional shape, rather than for every type:

[...]
let a flag x = x
let compose f g x = f(g x)
let (compose',enCompose,disCompose) = membrane ((a @--> a)@-->(a @--> a) @--> a @--> a) compose
let id = compose' inc dec

(Of course, "a" isn't a type variable. In particular, there's no constraint that all the types are the same.)

We still will have to define lots of instances of compose, obviously, but fewer than before... It seems to me that the biggest risk of this approach is that it's very, very easy to make mistakes: if I end up using compose' at a higher-order type than I declared, I can end up slipping through the membrane quite easily. This is an advantage of using the type-specific combinators, but without type annotations, they don't help either (int and bool above both have type 'a -> 'b -> 'b)...

(I haven't been following this discussion terribly closely, so I may be completely mistaken.)

Of course, you can share one combinator for all base types, but unfortunately, that does not change the problem: When you look at the type inferred for compose' in your example then you'll notice that it is not polymorphic -- precisely because of ML's value restriction!

There is no way that the same instance can be shared for multiple types in ML's type system. I believe it would work with slightly more general, System-F-style polymorphism, where polymorphic types are not restricted to prenex form. For example:

fun membrane () =
  let
     val flag = ref true
     fun membrane' t x = (t flag x, fn() => flag:=true, fn() => flag:=false)
  in
     membrane'
  end

It seems that it would be safe to type this function as

unit -> forall 'a 'b.((bool ref -> 'a -> 'b) -> 'a -> 'b * (unit -> unit) * (unit -> unit))

but that is beyond current ML (MLF should allow it, though; likewise the moral equivalent in Haskell under GHC's extensions).

[Edit: fixed typos and syntax in code example]

Thanks for the explanation... Obviously I didn't dig quite deep enough to expose my own ignorance. :)

I should have pointed out that there are at least the following work-arounds:

- You can turn the function into a functor:

functor Membrane() =
struct
   val flag = ref true
   fun membrane t x = t flag x
   fun en() = flag:=true
   fun dis() = flag:=false
end

(* Example: *)

structure M = Membrane()
val inc = M.membrane(int-->int) (fn x => x+1)
val not = M.membrane(bool-->bool) (fn x => not x)
val _ = M.dis()

This has the desired behaviour: every instantiation of the functor creates a new, fully polymorphic instance of the membrane function that will share a single flag among all calls.

- In OCaml, you could use polymorphic records:

type membrane = {membrane : 'a 'b.(bool ref -> 'a -> 'b) -> 'a -> 'b; en : unit -> unit; dis : unit -> unit}

let membrane () =
    let flag = ref true in
    let membrane' t x = t flag x in
    {membrane=membrane'; en=(fun() -> flag:=true); dis=(fun() -> flag:=false)}

(* Example: *)

let m = membrane ()
let inc = m.membrane (int@-->int) (fun x -> x+1)
let not = m.membrane (bool@-->bool) (fun x -> not x)
let _ = m.dis ()

If you just want multiple separate membranes to share the same flag, you can achieve it either by passing the flag (ref cell) explicitly (like in the version I posted) rather than allocating a fresh one in the membrane function, or you can write separate enable and disable functions that call the corresponding functions of multiple membranes.

Andreas has answered the question, but here's a code example that shows the lack of polymorphism in compose', after executing the code in the parent comment:

let appa x = "a" :: x;;
let appb x = "b" :: x;;
let appab = compose' appa appb;;

The last line fails with an error "This expression has type string list -> string list but is here used with type int -> int". The compose' function is inferred to have a type based on ints as soon as static analysis of compose' inc dec occurs. So you can't use the same compose' function to compose different types of function, even if they have the same functional shape.

I'm not entirely sure of what the meaning of a polymorphic compose (or anything polymorphic) would actually be in this context. Especially considering parametricity. Can someone elaborate on that?

At any rate, one can make the type parameters explicit:

val enable = ref true

fun compose (a, b, c) =
    let
      open Membrane
      val t = iso (fn c => c o (fn op & x => x),
                   fn c => c o op &)
                  ((b --> c) * (a --> b) --> a --> c)
    in
      make t enable op o
    end

One can reasonably call the above a polymorphic compose. It has the specification (type):

val compose : 'a Membrane.t * 'b Membrane.t * 'c Membrane.t
              -> ('b -> 'c) * ('a -> 'b) -> 'a -> 'c

To me the Membrane abstraction seems a little ad hoc, because access control is performed dynamically. I'm not entirely familiar with the motivation and intended uses of the Membrane (or similar) pattern (maybe I should read the thesis, but I don't have the time for that before next week), so I don't know whether that is precisely what is needed, but I nevertheless wonder whether one could solve similar problems using monads (or arrows) (or linear types). Using monads, one would essentially create a transaction during which access would be granted. Before a transaction was started and after the transaction would be finished, access to the controlled operations and data would be impossible. So, have less dynamic alternatives been considered?

Alice needs to give Bob a revocable reference to Carol, so she could later (possibly never) cancel it if Bob shouldn't be able to use it anymore. There's no static scope for this. Without this it's impossible to have true object capabilities (i.e. they would suffer from the Irrevocability Myth).

Richer type systems prevent whole classes of errors from happening to begin with (if you want to argue this point, don't bother; it isn't debatable, so if you—I mean the general "you," not Curtis—think it is, we won't be able to have a conversation about it).

This issue isn't actually quite as simple as you want to make it. Richer type systems allow more programs to be typed. This can work both ways unless you specify more precisely what "richer" means. On one hand, a richer type system may allow one to express more specific constraints on types. On the other hand, a richer type system may allow one to use less specific constraints on types. This latter kind of "richness" can actually open the door for errors that the "poorer" type system would have prevented.

See here for a note on a specific feature of a type system.

Vesa Karvonen: On the other hand, a richer type system may allow one to use less specific constraints on types. This latter kind of "richness" can actually open the door for errors that the "poorer" type system would have prevented.

Sorry for the sloppy terminology, because I think you raise a good point: one could argue that a type system could be made "richer" by the addition of a "top" type if it didn't have such a type before, while such an addition could indeed be used to impose weaker constraints. So I should have said "richer in the sense of allowing more specific types to be expressed, whether by annotation or inference." Thanks for cleaning up after me!

The added bit about the coworkers makes it sound a bit better, but again, this isn't something you can really design for. If you have inexperienced programmers, they're going to do inexperienced things.

I strongly disagree. It is a senior developer's job to specifically design systems so that the inevitable errors introduced by junior developers are quickly found, and their damage to the code-base limited. That's part of why junior developers are assigned discrete pieces of work with well-defined interfaces. While review, coding standards, and training are a large part of this, you absolutely can design, code, and test so as to limit the damage caused by inexperienced co-workers. If senior developers are really good, they can design and code in such a way as to teach their juniors to become better developers, beyond the effects of mere imitation. (To bring this back to the original response, the documentation and correctness effects of explicit typing are both invaluable to this pedagogical effort.)

More pointedly, it is the fate of most successful systems to be eventually maintained and extended by inexperienced software developers. Building a system so that it can only be maintained by experienced software developers is a sign of short-term thinking, and poor design. I wish I could say it was rare.

I strongly disagree. It is a senior developer's job to specifically design systems so that the inevitable errors introduced by junior developers are quickly found, and their damage to the code-base limited. That's part of why junior developers are assigned discrete pieces of work with well-defined interfaces. While review, coding standards, and training are a large part of this, you absolutely can design, code, and test so as to limit the damage caused by inexperienced co-workers. If senior developers are really good, they can design and code in such a way as to teach their juniors to become better developers, beyond the effects of mere imitation. (To bring this back to the original response, the documentation and correctness effects of explicit typing are both invaluable to this pedagogical effort.)

Yes, I completely agree. When I said "design for," I meant in reference to languages.

More pointedly, it is the fate of most successful systems to be eventually maintained and extended by inexperienced software developers. Building a system so that it can only be maintained by experienced software developers is a sign of short-term thinking, and poor design. I wish I could say it was rare.

As do I, but it's rather hard to deal with this as a language designer. You can give them facilities to make their code clear and concise, but you can't force them to use them.

As do I, but it's rather hard to deal with this as a language designer. You can give them facilities to make their code clear and concise, but you can't force them to use them.

The trick isn't to give them facilities, it's to make it easier to use those facilities correctly than to use them incorrectly. It's all about arranging incentives. That's the problem I have with soft typing. The short-term incentive to write untypable nonsense that happens to work can be very high during crunch times, and in pretty much any soft-typing system I can imagine, slapping together untyped nonsense will be easier than creating comprehensible code. Relying on peer pressure and standards to overcome that incentive strikes me as rather unwise, particularly when the flexibility payoff you describe seems so small.

The problem is, you're basically saying most popular statically typed languages, even strongly typed ones like OCaml, do the same. What you describe isn't just a property of soft typing--it occurs in any language that only issues warnings when you don't explicitly handle certain conditions. If what you were saying is true, don't you think people would've caught on and starting using languages that were more strict?

If that wasn't proof enough, I'll even disprove you theoretically. Let's analyze the example you gave:

The short-term incentive to write untypable nonsense that happens to work can be very high during crunch times, and in pretty much any soft-typing system I can imagine, slapping together untyped nonsense will be easier than creating comprehensible code.

Let's think about the situations in this might occur: you're coding away, and you get to a situation where you have to get input from some other function. Let's say this other function returns different types of values depending on what the user inputs, but you only care about one of those types. Because we're using one of those "untyped" softly typed language we can just go ahead and assume that the type is correct--after all, if it isn't, it'll just throw an exception automatically.

Now, let's compare this to a language which requires you to handle the other cases. You go through and code it and find out it doesn't compile. What happened? You forgot a case. So, you put the check in, get it to compile, and realize this version does the exact same thing as the one with the soft type language.

Now, let's compare this to a language which requires you to handle the other cases. You go through and code it and find out it doesn't compile. What happened? You forgot a case. So, you put the check in, get it to compile, and realize this version does the exact same thing as the one with the soft type language.

Right, except in that case there is now an explicit check in the code, reminding you (and everyone else) that you are cutting a corner. There's accountability, a paper trail, and something that makes you look kind of stupid in a code review. It also stays in the code, neatly annotated in the VCS, so that downstream maintenance knows that you cut a corner. The incentives, in that case, are to care.

In the soft type case, everything looks neat and clean, unless you happen to run the checker. Even then, checkers produce enough false positives that no one's going to look down their nose at you if you believe that this "just can't happen". After all, you wouldn't be using a soft-type system in the first place if you didn't want to do things where type correctness wasn't mechanically decidable. Downstream maintenance doesn't know if you cut the corner, or if the code you're calling changed out from under you. This increases their time to do root cause when something goes wrong, and makes assignment of responsibility more difficult, and thus less likely to be done correctly. The incentives, in this case, is to blame issues on miscommunication, thus avoiding responsibility. This is easy to do since the language actually encourage miscommunication, admittedly with the payoff of increasing individual productivity.

The code in the cases you describe has exactly the same semantics. The processes that go into creating it and the impact on maintenance are completely different.

I think the point is that it only has the same semantics to the computer!

Right, except in that case there is now an explicit check in the code, reminding you (and everyone else) that you are cutting a corner. There's accountability, a paper trail, and something that makes you look kind of stupid in a code review. It also stays in the code, neatly annotated in the VCS, so that downstream maintenance knows that you cut a corner. The incentives, in that case, are to care.

That depends. Most soft type systems probably issue warnings. In the best possible case, you have warnings presented to you as you type them by the editor, which seems like it would be a pretty good reminder to me. In the worst possible case, there are no warnings at all, but I'm not going to try and defend that, since if you're going to write a soft type system, you might as well go all the way and provide a decent programming environment as well, since the soft typing practically requires it. You could even say that about type inferencing, too, but that's a bit easier to deal with in editors.

So how do you tell, months after the fact, just who ignored the warnings first? In the strong typing case, responsibility is clear to anyone who reads the code, and easily traceable. In the soft typing case, it's hard to see who caused the problem, and responsibility evaporates like morning dew.

Basically what you're describing is a system that allows localized type hacks, and removes any responsibility for documenting them. Now I've got less difficulty with localized type hacks than some here, and will happily use reflection, RTTI, cast/instanceof where necessary. On the other hand, I'm very glad that such hacks require special syntax, and stand out like a sore thumb when compared to type-safe code. Allowing type hacks to become implicit, and not require specific in-code responsibility be taken for them, sounds like it will only end in tears.

How does showing a warning change any of what you're talking about at all? If the programmer has to do it explicitly, it's obviously his responsibility. If there's a warning in the programmer's code, it's obviously his fault. I'm not sure I understand your argument: what's the difference?

That's not because that such cases exists that soft-typing should be the default. I personnaly favor strict typing with type inference. In the haXe programming language, you can have dynamicly typed code blocks by using the "untyped" keyword. Only at the place you really need it.

The short-term incentive to write untypable nonsense that happens to work can be very high during crunch times

Problem is, if you're really in a crunch time, the alternative is usually well-designed, well-typed nonsense that happens to not work. Most customers I know would rather have a shitty piece of software that gets 80% of the job done than no software at all (outside of mission-critical areas).

You still have a problematic incentive: given a tight deadline, the programmer will either reach for a different tool (eg. scripting language) or circumvent the type system entirely (eg. by encoding all variables as strings; yes, people do this). There's nothing a language designer can do about this, because the programmer will just reach for a different language. It's not like we can force people to use our languages (well, unless we're the DoD, and look how that turned out).

It's really a project management issue. Managers have to realize that good software takes time, and the only way they're going to get good software is to allot that time. The language designer's job is to support the programmers that are willing and able to do a good job, not to strongarm the ones that aren't. They'll just go use some other language.

I believe I mentioned automatically inferring the most generic type before. That's not very descriptive of what my type system does, although I'm not sure if my language is at all representative of what you'd find in another soft type system. Basically, the container doesn't actually have any specific type of element (you might call it an 'any' type), but rather it can be inferred that every element of said container must have a 'draw' method. At least, that's how it would work if 'collection' was an argument to the function. Local variables in my language automatically have the type 'any'--the only use of defining it any farther than that is for optmisation by the compiler, but that doesn't have anything to do with type checking.

edit: There's one other use for inferring local variables, and that would be to show the type to the programmer.

uhm, the 'any' type would always be the most generic type, so you would realy just get a dynamic type system that way.

That is correct. You'd end up with basically dynamic typing for local variables, but parameters can be inferred and checked based on the function body.

I dont see how or why the interference whould work diffrently for diffrent variables. But you said

automatically inferring the most generic type before. .. At least, that's how it would work if 'collection' was an argument to the function.

and the most generic type would always be 'any'.

I dont see how or why the interference whould work diffrently for diffrent variables. But you said

If you infer the most general type of a variable based on its own function you'll find that its values will always be valid for its type, since they were used to construct it in the first place. Local variables don't need to be checked because of this, but if they're passed to another function the inferred values for that variable can be used to possibly detect type mismatch errors at compile time, or at least warn about one.

automatically inferring the most generic type before. .. At least, that's how it would work if 'collection' was an argument to the function.

and the most generic type would always be 'any'.

Not for arguments, no. The most generic type for an argument can be determined by how it's used in the function.

Anyway, discussing such things probably won't be helpful because of the lack of information on my type system. It's best to stick with the generic topic of soft typing.

Was trying to keep the example as simple as possible, but if it's parameters, then a simple modification of the example would still require an inference of type:

def drawme(pcollection):
   for each in pcollection:
      each.draw()

That really has nothing to do with soft typing, but rather nominal vs structural subtyping. Correct me if I'm wrong, but OCaml has the same behaviour I was talking about in that it will accept any object with a draw method due to its structural subtyping.

But then I don't know enuf about how OCaml would handle different classes in a collection if the collection is not declared to be of a certain base subclass. Closest approximation that I can get based on my current knowledge of the language:

class virtual drawable =
   object (self)
      method virtual draw : unit
   end

class pencil =
   object (self)
      method draw =
         Printf.printf "art\n"
   end

class gun =
   object (self)
      method draw =
         Printf.printf "bang\n"
   end

let main () =
   let (collection: drawable list) = [
      (new pencil :> drawable);
      (new gun :> drawable)] in

      List.iter (fun each ->
         each#draw;
      ) collection;;

main ();;

But here I had to explicitly declare a base interface class of drawable before it would allow me to put the different subclasses into a collection. Perhaps Paul can show me the error of my ways - or better yet, show how to use variant types to handle the duck typing.

Actually, in this simple case, you can get away with just:

class pencil = object method draw = Printf.printf "art\n" end;;
class gun = object method draw = Printf.printf "bang\n" end;;
let main _ = let collection = [new pencil; new gun] in List.iter (fun each -> each#draw) collection;;
main ();;

The reason for this is that pencil and gun are both of type < draw : unit >.

Things can get a bit trickier, though:

class pencil =
object
  method draw = Printf.printf "art\n"
  method foo = Printf.printf "foo\n"
end

class gun =
object
  method draw = Printf.printf "bang\n"
  method bar = Printf.printf "bar\n"
end

let main _ =
  let collection = [new pencil; new gun]
  in
    List.iter (fun each -> each#draw) collection;;
This expression has type gun but is here used with type pencil
Only the first object type has a method bar

Here, "this expression" refers to "new gun," of course. This is the "heterogeneous list" problem, of course. My solution to it was:

class type drawable = object method draw : unit end;;

class pencil =
object (self : #drawable)
  method draw = Printf.printf "art\n"
  method foo = Printf.printf "foo\n"
end;;

class gun =
object (self : #drawable)
  method draw = Printf.printf "bang\n"
  method bar = Printf.printf "bar\n"
end;;

let main _ =
  let collection = [((new pencil) :> drawable); ((new gun) :> drawable)]
  in
    List.iter (fun each -> each#draw) collection;;

It's worth emphasizing that the list is the issue, not the function!

(fun x -> x#draw)(new pencil);;
(fun x -> x#draw)(new gun);;

both work, even when pencil and gun are of different types, because the type of (fun x -> x#draw) is < draw : 'a; .. > -> 'a, i.e. a function taking any object implementing at least a draw method taking any type, and returning any type. The ".." is an "anonymous row variable" that covers any other (potential) methods that this function cares nothing about.

With respect to non-object approaches, Code reuse through polymorphic variants is a brilliant piece of work, and it gets even better with private row types and modules in Private row types: abstracting the unnamed. Highly recommended.

Have to add the different methods to get the effect I was looking for, which is the requirement that the type of the collection requires an explicit type.

and the most generic type would always be 'any'.

Curtis W, you are missing Felicia Li Svilling's point here. What she is saying is that the term "most generic" doesn't properly describe the kind of type you want. Consider a subtyping lattice where the type "Object" or "Any" is at the top. What you want to infer for a set of types is the least upper bound in that lattice.

What you want to infer for a set of types is the least upper bound in that lattice.

...if your types form a lattice in the first place. Unfortunately, this often is not the case. I hence feel that Curtis is making all kinds of naive assumptions that just don't hold up to reality. Type systems are an incredibly subtle field, and one should really be careful about making any claims without having a conrete system and proved all the nasty bits about soundness, principality, decidability, tractability and so on. But others have said that already...

Darn, I got it backwards. Sorry! (That is, assuming Any is at the top.) You don't want the least upper bound (or join), but the greatest lower bound (or meet).

...if your types form a lattice in the first place. Unfortunately, this often is not the case.

Yes. The type system has to be carefully constructed for useful greatest lower bounds to exist.

That's not very descriptive of what my type system does...

Yeah, my mistake, that answer was way too specific. Just assume that I said this instead:

Soft typing really has little to do with that example, but rather the type of inference does. For example, it might infer it to be of type Pencil|Gun, where | denotes a union type.

That's fine as far as it goes. But it doesn't address my other point:

It's also hard to have a discussion about the "advantages" of soft-typing without having some idea of what the proposed soft-typing system is and is not capable of doing.

I see that Chris has raised similar concerns in another comment.

So long as the conversation stays about soft typing in general I don't see any reasons for concern. Granted, soft typing isn't the most well documented concept on the internet, so I suppose I should post what I mean by it. From c2.com:

Where the type checker can prove that the program is type safe, all is fine and dandy. Where the type checker can't prove correctness it informs the programmer and inserts appropriate type checks, but doesn't reject the program.

I'm also assuming structural subtyping, although depending on the topic that may or may not be relevant. The above philosphy basically means that, in places one would have to cast in languages like C that aren't handled by structural subtyping, it's done automatically.

I'm afraid I don't really see what you're trying to achieve with this conversation, beyond saying "soft typing can be useful" . Soft typing "in general" makes different trade offs than static typing. Within the broad class of static typing systems, different static typing systems provide different capabilities. Similarly, different soft typing systems provide different capabilities (see for example the discussion in this paper of the different capabilities provided by different soft typing systems for Erlang). Making any deeper statement than "soft typing and static typing make different trade offs" requires being explicit about which specific static and soft typing systems we're discussing, and probably a context in which those type systems are to be used, so that we can consider which trade offs make more sense in the given context.

I'm afraid I don't really see what you're trying to achieve with this conversation, beyond saying "soft typing can be useful" . Soft typing "in general" makes different trade offs than static typing.

And those would be?

Within the broad class of static typing systems, different static typing systems provide different capabilities. Similarly, different soft typing systems provide different capabilities (see for example the discussion in this paper of the different capabilities provided by different soft typing systems for Erlang). Making any deeper statement than "soft typing and static typing make different trade offs" requires being explicit about which specific static and soft typing systems we're discussing, and probably a context in which those type systems are to be used, so that we can consider which trade offs make more sense in the given context.

When discussing abstract topics like this, it's important to keep comparisons "clean" by keeping everything equivalent except for that which you're comparing. Making any statements about car engines any deeper than "they're engines" is impossible on the basis that they could be in different cars.

And those would be?

Documented in the existing literature. Essentially it boils down to the quantity and kind of run-time errors you are willing to allow. Which is why context is important in discussing the "advantages" of one system over another.

When discussing abstract topics like this, it's important to keep comparisons "clean" by keeping everything equivalent except for that which you're comparing.

Making any statements about car engines any deeper than "they're engines" is impossible on the basis that they could be in different cars.

Documented in the existing literature. Essentially it boils down to the quantity and kind of run-time errors you are willing to allow. Which is why context is important in discussing the "advantages" of one system over another.

The "quantity and kind" of run-time errors is defined by the definition that I posted, or at least it is indirectly. Any statement that can be proven false at compile time is an error. Anything else isn't. It's that simple.

Which is all very well, except that you are making some fairly concrete claims, such as "...really the only difference between OCaml's type system and soft typing, barring the type inferencer, is...", without actually providing any concrete information on the soft typing system in question.

No, I'm making a fairly concrete comparison. It's not very detailed to notice, but in order to make a comparison like that I ignored every other difference other than static vs soft type system. I had to mention structural subtyping for clarification reasons, though, because I was dealing with an actual language. I think the problem here is that it's not believable that the information I'm using is derivable from the definitions of soft typing I've posted. Of course, that's the essence of arguing in general--try to disprove the other's assumptions, so I leave you all to disprove me if you feel I'm wrong.

But I think it actually highlights the issue I was trying raise. If you're going to discuss the advantages of, for example, pure internal combustion engines vs. hybrid engines, it is helpful to provide some information on (a) the performance characteristics of the two engines and

Already provided. Again, the problem doesn't seem to be that I'm not providing enough information, but rather that you don't believe all the information I've provided is grounded.

(b) the use to which the engines will be put.

Ah, but I've already proven that the environment doesn't matter. See the posts dealing with soft typing and inexperienced programmers.

Whether the engines being compared will be used for racing or for commuting makes a big difference as to which engine will be considered

Ah, but by now you've broken the analogy: if soft typing is a specific feature of the engine, it's already been proven that said feature does not depend upon any outside conditions.

Any statement that can be proven false at compile time is an error.

for each in collection:
   each.someRoutine()

Dynamic languages can really be dynamic, in that the someRoutine may be (a) attached to an object on the fly (i.e. it is not defined in the source of the class); or (b) proxied through a does not respond type of event; or (c) it may just be a type error. If you declare it a type error, the dynamic PL advocates are going to take issue with the fact that you are calling it unimposing.

From a dynamic PL standpoint (unimposing), how do I know a call like the following is an error?

for each in collection:
each.someRoutine()

It depends. What is collection defined as?

Not to get into too much detail, but one of the properties of dynamic languages is that methods can be attached or detached at run time. And even if a method does not exist, the class can have a method that catches all calls to an unknown method (a proxy class with no statically defined methods is not uncommon - one which handles the messages from any number of class types). A complete analysis of the program flow would soon run into the halting-problem, as one tries to decide whether the message (method call) is valid at any particular point in the program. So the question is whether you can actually prove that a method does or does not exist in the face of such dynamism?

Of course, none of this is intractable if one is willing to accept certain tradeoffs. That is, you can't prove statically that the method exists, so you either (a) flag a compile error or warning; or (b) provide hint capabilities within the type annotation to declare the programmer intent.

That would fall in the category of uncheckable at runtime, which means probably the latter part of a (a warning) and b would be the most likely course of action, although b is, of course, optional.

Nastier: in case of mutability, you can't prove it won't later be removed.

The "quantity and kind" of run-time errors is defined by the definition that I posted, or at least it is indirectly. Any statement that can be proven false at compile time is an error. Anything else isn't. It's that simple.

Write an article about it then, post it on your web site / blog, and link to it in this thread. We want to avoid guessing games here. An article should make your ideas explicit, and most importantly, checkable.

I think the problem here is that it's not believable that the information I'm using is derivable from the definitions of soft typing I've posted.

The issue of believability is secondary to the issue of how likely it is that someone else could come to the same conclusions you've come to, with the minimal information you've posted.

Of course, that's the essence of arguing in general--try to disprove the other's assumptions, so I leave you all to disprove me if you feel I'm wrong.

See the quote by Chris Rathman under Discussion Quality, starting with "There is a difference between the concept of a debate versus the concept of exchanging ideas." You apparently feel that you're putting forward an interesting idea. However, you've omitted so many details that it's difficult to evaluate the idea, and so this turns into a debate with a particularly low signal/noise ratio. If you want to advance an idea, and can't point to references to explain it (C2 sound bites aren't sufficient), then the onus is on you to provide details, not bit by bit in comments, but in a coherently argued article.

Write an article about it then, post it on your web site / blog, and link to it in this thread. We want to avoid guessing games here. An article should make your ideas explicit, and most importantly, checkable.

Ok :-)

The issue of believability is secondary to the issue of how likely it is that someone else could come to the same conclusions you've come to, with the minimal information you've posted.

I suppose my line of reasoning could be a bit clearer, and I see this is where an article/paper comes in handy.

See the quote by Chris Rathman under Discussion Quality, starting with "There is a difference between the concept of a debate versus the concept of exchanging ideas." You apparently feel that you're putting forward an interesting idea.

Actually, the main point of this thread was to continue the discussion that forked off of the parallel class hierarchies thread. If you feel that I haven't provided enough information, though, I will gladly try and improve that in an article/paper.

So long as the conversation stays about soft typing in general I don't see any reasons for concern.

Curtis: unfortunately, as a number of people have pointed out, large parts of this discussion seem to be about a notion of soft typing which you have in mind, which as far as anyone else can tell, isn't documented or implemented anywhere. Until that changes, please avoid speculating about the properties of such systems. Such speculation has a high likelihood of being wrong, but without details to examine, others can't properly assess your claims.

Please read point 4(b) of our nascent Policies.

You'd be welcome to discuss your experiences after having implemented a system which illustrates your ideas, as Derek Elkins suggested.

Curtis: unfortunately, as a number of people have pointed out, large parts of this discussion seem to be about a notion of soft typing which you have in mind, which as far as anyone else can tell, isn't documented or implemented anywhere. Until that changes, please avoid speculating about the properties of such systems. Such speculation has a high likelihood of being wrong, but without details to examine, others can't properly assess your claims.

Could you please point to where I've done this? I corrected the one that was pointed out, although I believe I've kept the rest of the discussion related purely to the definition of soft typing. In cases where it's impossible to answer with just this, I've tried to list the different methods with which it could be done, or at least explain that it's not related directly to the discussion.

This entire thread is about a notion of soft typing which you hold, which doesn't seem to correspond very closely to any extant soft typing system. If you could point to a single real system, or paper about a system, which has the kinds of properties you've been talking about, that would make an enormous difference. The very brief characterizations you've given, such as the connection to structural subtyping, and the quote from C2, are too general to allow you to make claims like "The above philosphy basically means that, in places one would have to cast in languages like C that aren't handled by structural subtyping, it's done automatically," or "Soft typing can catch the same amount of provable errors at compile time as static typing." All of these things might be possible in some particular combination of language and soft typing system, but not necessarily together: for example, re the former quoted claim, automatic casting has implications for what kind of type inference is possible, and can reduce the number of type errors that can be detected, which would make the latter quoted claim false.

Particularly silly is "I believe that soft typing is the best choice for all roles." I imagine you must at least mean "...will in the future be the best choice...", once someone develops a soft typing system which users find compelling. There's a large gap between the utopian vision of soft typing you appear to hold, and the state of the art. You need to account for that gap with more than handwaving.

You made it very clear in this comment that you are thinking in terms of a particular language and soft type system that you're working on. This quote puts the problem in a nutshell: "That's not very descriptive of what my type system does, although I'm not sure if my language is at all representative of what you'd find in another soft type system." I suspect this perspective is coloring your comments more than you realize. Since none of us have seen the language or type system in question, it's difficult to discuss the subject meaningfully.

If you're not ready to release code, perhaps you could do as I suggested in this comment and contrast the kind of system you're thinking of with one of the existing soft typing systems. Also keep in mind that the nature of the underlying language is critical.

This entire thread is about a notion of soft typing which you hold, which doesn't seem to correspond very closely to any extant soft typing system. If you could point to a single real system, or paper about a system, which has the kinds of properties you've been talking about, that would make an enormous difference. The very brief characterizations you've given, such as the connection to structural subtyping, and the quote from C2, are too general to allow you to make claims like "The above philosphy basically means that, in places one would have to cast in languages like C that aren't handled by structural subtyping, it's done automatically," or "Soft typing can catch the same amount of provable errors at compile time as static typing."

Those can both be proven true based on the definition I've already given. Let's start with the first one, working off what I posted from c2:

Where the type checker can prove that the program is type safe, all is fine and dandy. Where the type checker can't prove correctness it informs the programmer and inserts appropriate type checks, but doesn't reject the program.

Think about this: it basically means that whenever there's a type error that's not provably true at compile time, the compiler doesn't grief the programmer about it. How does this apply to casting? It doesn't, or rather, casting can be used in languages like C for completely unrelated purposes, but the kind I'm talking about is exactly one type: downcasting. Downcasts in C/C++, e.g. void* -> int*, and most other popular languages are not done automatically mostly because they can't check them. Soft languages don't have this pitfall by definition--if they can't prove it false beforehand, they'll let it through and possibly warn the user, hence automatic downcasts.

The second statement about catching the same amount of provable errors is also provable by definition: soft type systems catch statements that are provably erroneous at compile time and defer the rest to runtime. If you were to take the exact same code and run it through a statically typed compiler, you'd find that it would produce more errors overall, but it would still have the same amount of provable errors.

Particularly silly is "I believe that soft typing is the best choice for all roles." I imagine you must at least mean "...will in the future be the best choice...", once someone develops a soft typing system which users find compelling.

I was speaking of the concept in general, of course. It makes so sense to talk in reference to time when speaking of singular, abstract concepts like this: it will always and has always been the best choice in theory when considered by itself, or at least that's my argument.

You made it very clear in this comment that you are thinking in terms of a particular language and soft type system that you're working on. This quote puts the problem in a nutshell: "That's not very descriptive of what my type system does, although I'm not sure if my language is at all representative of what you'd find in another soft type system." I suspect this perspective is coloring your comments more than you realize. Since none of us have seen the language or type system in question, it's difficult to discuss the subject meaningfully.

To which I later replied:

Just assume that I said this instead:

Soft typing really has little to do with that example, but rather the type of inference does. For example, it might infer it to be of type Pencil|Gun, where | denotes a union type.

I'd say that's a fairly general statement. I certainly managed to keep "my" out of it ;-)

What if I said that I accidentally reused the same method name of draw() and that they really have two totally different meanings. One draws on a canvas, whereas the other shoots to kill. What if I as the programmer made a mistake in treating these two as some invisible type called "drawable".

Ok, so we'll assume for a minute that the code does not really contain a type error. The next question is how you go about naming these inferred types? So now we got the compiler trying to connect all the duck typing together and make it give us a meaningful name. Simple enough in this case since there's only one method involved. But what if I start adding new methods and all the methods aren't shared in all the different places? Seems to me that you have a distinct possibility in a combinatorial explosion in the possible types that can be inferred. And these types are not part of the standard library, nor are they defined by the user (as in above). And if I read you right, the inferred types are interfaces, which can themselves be variously classed and subclassed (as opposed to sum types).

Bottom line for me is that you can evangelize for soft-typing all you want. The question is whether an implementation can be proven to (a) catch all the same type errors that are caught in static languages; and (b) it would be unimposing. That is you claim all the advantages in the static vs. dynamic debate, with none of the disadvantages. Sounds enticing, but I'll await for an implementation before I can agree to these postulates.

The question is whether an implementation can be proven to (a) catch all the same type errors that are caught in static languages; and (b) it would be unimposing. That is you claim all the advantages in the static vs. dynamic typing debate with none of the disadvantages.

As I have referenced a couple of times, my view is that they cannot satisfy both those constraints (where "unimposing" is taken to be about as "lightweight" as dynamic typing). In fact, I stated in that thread that quite the opposite, I think soft typing leads to almost all the disadvantages and none of the advantages in the static v. dynamic debate.

To Curtis W: Implement something that illustrates (and makes concrete) your ideas. Since you claim that it follows readily from structural subtyping, which is more or less well understood, you should be able to use previous research and quickly make a prototype "toy" implementation of a language that illustrates your typing ideas. You should be able to knock it out in probably less than a week assuming you already have the necessary background. The goal of this would not be to be the be-all-end-all language, but to simply present your ideas.

Actually, this is an excellent idea. I think I might do just that.

What if I said that I accidentally reused the same method name of draw() and that they really have two totally different meanings. One draws on a canvas, whereas the other shoots to kill. What if I as the programmer made a mistake in treating these two as some invisible type called "drawable".

This is a good point, but again it depends on the type of inferencer you use. The kind that I was talking about earlier requires that, if two types have the same interface, they must be compatible semantically. This can be related to type annotation vs inference, in that you can use the former to provide an extra layer of protection if necessary, but it's not required.

This is a good point, but again it depends on the type of inferencer you use. The kind that I was talking about earlier requires that, if two types have the same interface, they must be compatible semantically.

is this requirement, given the structurally subtyped nature of soft typing, feasable?

i might misunderstand your definition of soft typing, but in structurally subtyped systems problems like the one given above are bound to occur (which is why, compared to strict typing, they always loose in terms of expressiveness).

is this requirement, given the structurally subtyped nature of soft typing, feasable?

I'm not sure I understand. That requirement is precisely because of the structural subtyping. Maybe you were confused by my use of the word "interface" to mean the functions which operate on the types.

i am more confused by the general notion of the requirement itself. how do you guarantee semantical compatibility but for imposing the requirement onto the programmer. this basically leaves you with the problem inherent to all structurally subtyped systems, like the Drawable example in the original posting.

differently said: what is the difference between statically checked structural subtyping and soft typing?

In haXe, using typeful structural subtyping, that would be the following :

class Pencil {
    public function new() { }
    public function draw() { trace("art"); }
}

class Gun {
    public function new() { }
    public function draw() { trace("bang"); } 
}

class Test {
    static function main() {
         var collection = new List<{ draw : Void -> Void }>();
         collection.add(new Pencil();
         collection.add(new Gun());
         for( each in collection )
              each.draw();
    }
}

You can also define a typedef shortcut for the anonymous type :

typedef CanDraw = {
     function draw() : Void;
}

And then create a List<CanDraw>.

First, is this a type error?

Depending on your type system yes, but by inspection, no (as both objects implement the desired "draw" behaviour).

Second, if it is not a type error, what is the type of the collection?

Typing first-class messages has been challenging, but this paper seems to have hit the sweet spot, which should also correctly type your example:

http://www.eros-os.org/pipermail/e-lang/2005-June/010711.html