I’ve been using Python for a while and playing with its recent static type system.
When I discovered ways to do type-level programming (e.g. I implemented a list that knows its length, updates it correctly, does bounds checking, etc… all at type-checking time) I was told that I was “abusing” Python’s type system.
Indeed, I discovered some interesting tricks that then went away in later versions of the type checker I was using. The author of that type checker was quite dismissive of my work, so I gave up instead of looking for eventual workarounds.
TypeScript’s type system, although unsound, is quite powerful for type-level programming (e.g. I implemented a simple language in it (i.e. parser + interpreter)), but, unfortunately, I don’t like JS very much.
Before diving into Scala, I’d like to know whether what I want to do is possible or not (but I’ll probably move to Scala anyway).
Instead of avoiding mutability, I’d like to control it. I don’t need anything too fancy. I’d simply like to split classes’ (or types’, in general) interfaces into at least 2 (overlapping) versions: read-only (r) and read-write (w).
(Sorry for using Python terminology.) As an example, let’s say we have a list[int]. After the split, we get list_r[int] and list_w[int]. The former is read-only and the latter read-write. Note that, since list is a pre-existing type, we’ll need a lift function to lift a regular list to a list_*. Now let’s define the following function:
def f(xs: list_r[int], ys: list_w[int]) -> list_w[int]:
...
Here’s an example of the behavior I want:
rl: list_r[int] = lift([1, 2, 3]) # also `lift([1, 2, 3], 'r')`
wl: list_w[int] = lift([4]) # also `lift([4], 'w')`
f(rl, rl) # error: can't convert a list_r into a list_w
f(rl, wl) # error: write access needs explicit permission
f(rl, w(wl))
f(wl, w(wl)) # note the w -> r coercion
f(rl, w(rl)) # error: can't convert a list_r into a list_w
Also, note that list_r[T] is covariant in T, as it should.
The actual system had 4 access modes:
r: read-only accessw: read-write accessrk: keep in read-only modewk: keep in read-write mode
“keep” tells a function that it can keep the value. Without “keep”, a function must completely forget about that value before returning. This holds recursively, of course.
This is also useful to eliminate redundant copies. For instance, a constructor may require a list_wr[T], which means that it may keep and use the list indefinitely, without having to make a copy.
The read-only and read-write qualities are actually enforced:
def f(xs: list_r[int], ys: list_w[int]) -> list_w[int]:
xs.sort() # error: no in-place sorting allowed
xs[0] = 4 # error
...
ys.sort() # error: permission needed
w(ys).sort()
w(ys)[0] = 3
return xs # error: can't convert list_r to list_w
return xs.copy() # NOTE: `copy` always returns a list_w
Note that, at runtime, list_r and list_w (and list_rk and list_wk) are just regular lists, and lift and w just identity functions. This is all just a static type mechanism.
The “permission part” is the trickiest to implement. I used an ugly hack:
@lock
def f[L](_: L, xs: list_r[int], ys: list_w[int, L]) -> list_w[int, L]:
...
I use lock to create an “external” signature for f. The callers will see the following signature:
def f(xs: list_r[int], ys: list_w[int, _Unlocked]) -> list_w[int, None]
L is a type param for a “lock”. When created by lift or directly by list_w, L is just None. To appease the external signature, the caller must use w for ys, which converts ys from a list_w[int, None] to a list_w[int, _Unlocked]. Note that the return type must have L = None or that list_w would be pre-authorized, which is something we don’t want.
OTOH, the implementation of f sees a generic list_w[int, L] and so it must use w to pass ys to other functions. In particular, f can’t call itself by forwarding its args:
@lock
def f[L](_: L, xs: list_r[int], ys: list_w[int, L]) -> list_w[int, L]:
f(xs, ys) # type error: needs explicit write permission
f(xs, w(ys))
Of course, the example above recurses forever, but that’s beside the point 
In case you’re wondering, that _: L is a hack I need to get a hold of the type param in lock so that I can specialize it into _Unlocked for the args, and None for the return value. In Python there’s no way to manipulate a signature in a general way.
I can’t get the latest version of the type checker to replace L with the intended types anymore, which broke my code 
That’s apparently my fault, since I was relying on undefined behavior. In my defense, most of Python type system’s behavior is undefined. Unless I’m doing really basic stuff, I always get different results with different type checkers. I’ve had enough.
BTW, implementing w (+ r, rk and wk) is easy enough, but lift is problematic because it operates on a type we don’t control. The obvious solution is function overloading (list → list_w, set → set_w, etc…), but it’s an inefficient one, as overloading resolution is usually cubic in the number of overloads, and, even worse, one would’ve to import all the supported types at once. I opted for local lifts. For instance, let’s say a file uses list, set, and dict. We just create a local lift as follows:
lift = Lift[list_w | set_w | dict_w]()
Lift’s implementation is full of “abuses”, of course!
Hoping you’re still with me, my question is the following:
Can I implement something like that in Scala?
No pseudo-code there! Even `…` is part of the language.
