Lambda the Ultimate

As people might have noticed I've been somewhat interested in how to type

g = \f x y. (f x, f y)

Now you might think HM, as implemented in various languages, does a nice job typing that. Ocaml gives the most readable result as

# let g f x y = (f x, f y);;
val g : ('a -> 'b) -> 'a -> 'a -> 'b * 'b = 

Or you could go higher rank and type it

g :: (forall a b. a -> b) -> a -> b -> (c, d)
g = \f x y -> (f x, f y)

But, for various reasons, I want to type it

def g: (a -> f a) -> b -> c -> (f b, f c) =
    [f, x, y -> (f x, f y)]

Since I am lazy and assume everything has been done in literature somewhere, does anyone have a reference with a typing system like that?

PS. 'Solved' in Haskell. Courtesy of Sjoerd Visscher, Haskell allows for quantification over type constructors; though I want to avoid explicit quantifcation.

g :: (forall a. a -> f a) -> b -> c -> (f b, f c)
g f x y = (f x, f y)

PPS. Gashe noticed that Haskell is unable to recognize that f should sometimes be unificated with 'id = /\a. a'

*Main> g (+ 2) 3 4

:27:4:
    Couldn't match type `a' with `f0 a'
      `a' is a rigid type variable bound by
          a type expected by the context: a -> f0 a at :27:1
    Expected type: a -> f0 a
      Actual type: a -> a
    In the first argument of `g', namely `(+ 2)'
    In the expression: g (+ 2) 3 4
    In an equation for `it': it = g (+ 2) 3 4

Suppose like Rust & C/C++, we want to support references that point to the inside of another value. A reference<t> is something that can be dereferenced (deref : reference<t> -> t). A reference may also be mutable, so that we can set its value. It may also support other operations, such as walking a data structure. Examples:

1. Given a struct x { a:int, b:int }, we can obtain a reference y=&x.a. Later on, we can read from that reference.
2. Given a sum type, we can pattern match on it and obtain a reference to the value inside of it.
3. Given an array, we can obtain an iterator of the array. We can dereference the iterator to obtain the current value, and we can call next() to obtain a reference to the next item. The same goes for an iterator over a tree.

Note that "reference" in the sense I'm using is not necessarily just a pointer. A tree iterator may maintain a stack of parent nodes in order to be able to traverse a singly linked tree.

There's one nasty problem with references, which is that in the presence of mutation they can lead to memory unsafety or run time errors. Examples:

1. Given the sum type (Either Int String), and x = Left 3, we can pattern match on x and obtain a reference r to the value 3 inside it. If we then mutate x := Right "foo", now the reference r is no longer valid. If r is represented as a plain old pointer, then if we dereference it we will try to read an int where now a string is stored.
2. Given a tree iterator over some tree, we can go to somewhere in the middle of the tree. If we now mutate the tree, the iterator may no longer be valid.

As you can see, it's not just a problem with pointers. Even in a language like Java, you have problems with iterators when the underlying data structure is mutated. At run time they may throw ConcurrentModificationException.

Rusts type system attempts to prevent these kind of errors statically, but Rusts type system isn't fully finalized yet and it is quite complicated. I was wondering if there is existing literature on this problem and perhaps there is some elegant way to prevent this with types. It would probably involve linear types and capabilities.

If such a thing does not exist yet, one thing I can think of is to require a linear capability in order to mutate the value, and in order to obtain a reference to the inside of the value you must give up this capability. In return you get a capability that allows you to read the references. If you later want to mutate again, you have to give up the capability to read the references. Is this a good approach? Why/why not?