Lambda the Ultimate

I think your statements about strong type systems need a similar qualifier to the one you're recommending for him ("in language Y"), and I think your conclusions in the last paragraph are off.

IMO types should allow you to express whatever properties you wish to express. Your observations just show that with sufficiently expressive types, you need the ability to cast away some of the finer details of a type and to leave unproven certain claims made by the type annotations. This is not the same as switching to dynamic types. Many of these uninferrable properties cannot be practically be checked dynamically (e.g. because they involve quantifiers).

Some things can be quite awkward to type, for example fixpoint combinators.

This is one of these myths that somehow refuse to die out. ;) Fixpoint combinators can be typed quite easily -- if you want to. The Z combinator (strict version of Y) written as is in OCaml:

# let z f = let w = fun x -> f (fun v -> x x v) in w w;;
val z : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>

This is executed with the -rectypes option that turns on (implicitly) recursive types in OCaml. What does this option do? Switch to a more complicated typing mechanism?

No, it does nothing like that -- instead, it merely turns off the usual occurrence check in HM type inference. In other words, it switches to a simpler algorithm (at least given the graph structure for types that OCaml is using anyways).

Here is the old story of rectypes again: OCaml 1.00 back in the days allowed implicitly recursive types by default. More programs could be typed. But users complained! The reason was that too many programs were considered well-typed. In practice, in almost all cases where you get a recursive type it is not intended, and just leads to far more obscure errors downstream.

The moral is that type system design is not about allowing as many programs as possible -- that would be trivial to achieve: just make everything have the same type, which is exactly what dynamic languages do. Good type system design is about setting up rules that are most likely to help the programmer in the 99% of common cases.

For the remaining 1%, you can still write the Z combinator, even without rectypes. You only have to be more explicit about the type recursion:

# type 'a recfun = Rec of ('a recfun -> 'a);;
type 'a recfun = Rec of ('a recfun -> 'a)
# let z f = let w = fun (Rec x) -> f (fun v -> x (Rec x) v) in w (Rec w);;
val z : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>

It's easy to understand why programmers might hate static typing if their main exposure to it was, for example: Pascal, Java 1.3, and C++. :)

These days, it seems that for every complaint about static type systems, there is a statically typed language that avoids the problem. Unfortunately, they aren't (yet) all the same language.

I sometimes wonder whether a type safety analysis should be free to infer more precise types than the user/module declarations such that, in many cases, a concrete program can be proven safe without proving it future-compatible or subject to substitution. My intuition is that such a feature could relax one of the common remaining complaints about static typing - that there is so much redundancy of expression and structure in the type system and program code.

These days, it seems that for every complaint about static type systems, there is a statically typed language that avoids the problem. Unfortunately, they aren't (yet) all the same language.

Complexity?

There are simple static type systems. :)

The code you have to write in those languages isn't simple compared to what you'd write in a dynamically typed language. They're either inexpressive which makes the code you have to write complex, or they're turing tarpits, which makes the code you have to write complicated.

Indeed. This example supports what you quoted from me above. :)

I wonder if we'll ever manage simplicity in a much more precise type system. I wonder if pluggable and structural type systems might be part of the answer, i.e. avoiding the entangled semantics that come from typeful dispatch, and avoiding the rigidity and brittleness that comes from naming intermediate types.

I don't think that we'll manage the same level of simplicity as dynamically typed languages, but I don't think that would be a good thing either. Dynamic typing is simpler because it doesn't force you to think about types. But often thinking about types is a good thing. When you write a function it helps to think about what kind of inputs are acceptable and what kind of outputs are acceptable. In dynamically typed languages, especially those with some kind of typecase (which in practice is all of them), you often see the problems associated with not thinking about types. Instead of having to sit down and rethink the problem and your abstractions, you can just bring out the typecase hammer and solve it ad hoc. The simplest example of this is null sentinel values. In dynamically typed languages you often see functions that either return some type T or null. This works most of the time until T itself can be null. In a proper statically typed language you are forced to think about the problem and come to the correct solution, namely Option. [of course some statically typed languages make the same mistake, since they implement a limited form of dynamic typing specifically for null: dynamically typed languages implicitly work with a sum type of all types, languages like Java implicitly work with a sum type of the actual type and null]

So there is a line between simple and simplistic. Can we be simple, so that we don't have to think about types when they don't really matter, but not simplistic so that we do have to think about types when they do matter? To an extent, yes. This is already somewhat possible because of type inference. However, as soon as you run into code for which the compiler can't find a type, the illusion is dispelled. I think that making a distinction between "can't prove that this code is type correct" and "this code is definitely type incorrect" would help a lot, especially as you get into stronger types.

Pluggable type systems in the sense that you can strengthen the algorithms used by the type checker with additional decision procedures so that code that previously fell into the class "can't prove that this code is type correct" now falls into either "this code is type correct" or "this code is type incorrect", may certainly be a good idea. But I do not believe in pluggable type systems in the sense of starting with a dynamically typed language, and then layering some kind of static analysis on top. I think dynamically typed languages get metadata (= types) fundamentally wrong. When you have xs : List[Int] in a statically typed language, you have the data xs and the metadata List[Int] that describes the representation and what you can do with xs. In a traditional dynamically typed language you have xs which has type tag List, and inside that list are a bunch of values which happen to have type tag Int. There is no way to accurately describe a list of integers as metadata in a dynamically typed language that tags values that way. This means that you have to invent some additional mechanism to describe that, so now you have two metadata systems. It's better to have a single expressive and extensible language for metadata about values at the basis of the language, as you have in statically typed languages.

This doesn't mean that those types have to be checked at compile time. It's perfectly possible to attach metadata like List[Int] to variables like xs and check dynamically that you don't pass xs to a function that expects List[String]. In fact you can check full dependent types dynamically that way. For instance when you have a function f with dependent type f : (x:T) -> g x, and that is applied to some value v in f v then at run time you first check if v has attached type T' that is compatible with T, and if so then you call f on v and you call g on v, and you attach the type (g v) as metadata to the value (f v). So this way you formulate the whole semantics of the type system as something that happens at run time. The static part of the type system then becomes a set of decision procedures that try to prove for each sub-expression whether or not that will raise a type error at run time. One problem with this approach that I haven't figured out is how to do type classes/implicit parameters in such a language, since you do not have the necessary information to do that at compile time, and doing it at run time also has complications that I won't go into here.

About nominal vs structural typing, I think that is a distinction that should be left to the programmer on a case by case basis. Structural by default, but there should be some construct to wrap an existing type into a nominally typed "box". For example you may wish to represent a datetime as an Int indicating the number of milliseconds since 1970. There should be some way to wrap an int in something so that you get a type error if you confuse a regular int with a datetime. The same goes for records/objects. Just because two things are represented as a record with values of the same type, doesn't mean that it makes sense to pass one where the other is expected, so you should be able to wrap that in a nominal box to make sure that you get a type error if you do. Haskell does this well with newtype.

I agree with most of your points. I don't like this idea, though:

So this way you formulate the whole semantics of the type system as something that happens at run time.

I don't think we want to muck up the dynamics of the language, which we should strive to keep as simple as possible, with static meta-information. Even if you did solve the problem of instance selection in this system.

I've given vague sketches of how my type system works before, and I'll continue to be vague, but I'm now more convinced it's a good idea. The kernel of the idea is to start with a powerful logic like dependent type theory (I'm using a new variant of type theory for reasons I won't go into here) as providing a core semantics. Then you expose a type system as arbitrary term annotations that behave according to simple mechanical rules which you can prove correct with the respect to the underlying logic.

So it's a very pay-as-you-go or prove-the-theorems-you-want-to approach. You can cast between types (have a Nat and need a non-zero Nat?) without changing your type signatures, with those casts leaving assertions to be checked in the underlying logic. I'm also a firm believer in being able to assert things without proof, whether through types or a stand alone assertions. So I think this approach answers most (all?) objections that the dynamic type guys have, except possibly simplicity.

I'm interested in what you've been developing. Could you perhaps blog about your variant of dependent type theory?

I guess a blog couldn't hurt, but I haven't hammered out the details just yet. Particularly around impredicativity and parametricity. I feel like I'm close, but I've had a high work load lately and I haven't gotten it figured out.

Pay as you go is exactly the motivation for modeling the semantics at run time. In any pay as you go system you need to have some form of dynamic checking so you're going to have that in your dynamic semantics anyway. The nice thing about taking the dynamic checking as the basis of the semantics is that it automatically determines the set of sound static checkers. If the static checker is a conservative approximation to what happens at run time then it is correct.

(An extra advantage is that if you have this run time metadata everything can be represented unboxed. You don't need to tag on additional size information and information about where the pointers are. In this sense the metadata is exact. This is different than the representation of e.g. OCaml or Haskell, which use a metadata at run time which is more like what dynamically typed languages do namely tag each value separately rather than tagging each variable with metadata that describes the whole structure of the value.)

I've given vague sketches of how my type system works before, and I'll continue to be vague, but I'm now more convinced it's a good idea. The kernel of the idea is to start with a powerful logic like dependent type theory (I'm using a new variant of type theory for reasons I won't go into here) as providing a core semantics. Then you expose a type system as arbitrary term annotations that behave according to simple mechanical rules which you can prove correct with the respect to the underlying logic.

This is indeed quite vague :) Can you go into a little bit more detail? As I read it, the description you give here could also fit to any existing static type system that has a Curry-Howard correspondence?

In any pay as you go system you need to have some form of dynamic checking so you're going to have that in your dynamic semantics anyway.

I meant 'pay' to refer to programmer time, not run time. I guess I should have left it as prove-what-you-want-to. I'm thinking of an approach to programming where you first get it working and then shift to making it fast and proving it right. Dynamic checking is not necessarily part of the semantics in what I have in mind.

Another limitation of dynamic checking as the basis of typing is that you can't express as much. There are useful propositions with quantifiers that you can't really check at run-time, but that you can prove correct. And there are lots of useful propositions with quantifiers that you cannot realistically check at run-time because it would be too slow. Things like "this reference isn't present in this collection at this time".

As I read it, the description you give here could also fit to any existing static type system that has a Curry-Howard correspondence

Maybe the part I didn't explain well is that the mapping from type annotation to logic is programmable at the language level. I'm not just saying that there is a formalization of the type system into dependent type theory. I'm saying the type library creator gets to pick the map.

Another limitation of dynamic checking as the basis of typing is that you can't express as much.

Isn't it more correct to say that dynamic checking as a different expressiveness from static checking? A static type system, for example, can reason about possible future or past execution, while a dynamic type system can leverage very precise knowledge about "now."

Things like "this reference isn't present in this collection at this time".

If the collection is a hash set, then the dynamic check is O(1).

What I meant is that dynamic typing cannot express as much as static typing. You're right that there are some properties that you can check with dynamic typing that you cannot prove statically, but you can still state them statically, even if you have to use dynamic checks to verify that they hold at run-time.

On the other count, you're right. I was imagining the collection to be a list. Oh well... there are lots of examples of properties you can easily state but not easily check. How about asserting that two sets are disjoint?

Most of the time my professional work, in the last dozen years, has involved deciding things as efficiently as possible about bytes that show up in network packets. A surprisingly large fraction of this involves finding intersections of sets. One goal is to make every operation as close an approximation to constant time as possible. (Lately I'm working on IPsec, which can seem like a previously unknown circle of hell in Dante's Inferno.)

I know you probably don't mean this question seriously. But in practice seeing whether sets are disjoint occurs a lot.

... there are lots of examples of properties you can easily state but not easily check. How about asserting that two sets are disjoint?

If you know nothing about the two sets, it's linear to convert one to a hash set, then linear to look for each member in the other. If you know a lot about the two sets, because they are members of specific things you control, you can arrange membership is allowed in at most one set because of how links are handled. For example a green thread fiber is runnable or blocked, but never both at once, because it can only be in one collection at a time. Thus runnable and blocked sets are disjoint. So sometimes there is a constant time answer to what might otherwise be linear.

I'm actually sort of interested in whatever specific problem you had in mind. I assume you just mean it's possible to infer membership in at most one set was possible give the set of observed operations in code.

I'm actually sort of interested in whatever specific problem you had in mind.

I didn't really have a specific example in mind (this was my second choice for an example after all), but what I was imagining is that you write code to maintain the disjointness of two or more sets by construction, incrementally, and then you want to add an assertion that says that your incremental scheme works. Hopefully you could even prove that assertion.

In this situation, the goal is to write a simple specification of disjointedness that's obviously correct. Manually incrementalizing this specification or introducing complicated data structures into it for performance reasons is taking us further from the goal.

If your sets are tree sets then disjointness can be checked in O(log n) ;-) -- edit: oh, no it cannot :( Best you can get is linear in the number of elements in the smaller set.

I meant 'pay' to refer to programmer time, not run time. I guess I should have left it as prove-what-you-want-to. I'm thinking of an approach to programming where you first get it working and then shift to making it fast and proving it right. Dynamic checking is not necessarily part of the semantics in what I have in mind.

Right, that's how I interpreted it, but because you wrote:

"You can cast between types (have a Nat and need a non-zero Nat?) without changing your type signatures, with those casts leaving assertions to be checked in the underlying logic."

I assumed you'd have some form of dynamic checking. Or what will happen at run time if this cast turns out to be invalid?

Another limitation of dynamic checking as the basis of typing is that you can't express as much. There are useful propositions with quantifiers that you can't really check at run-time, but that you can prove correct. And there are lots of useful propositions with quantifiers that you cannot realistically check at run-time because it would be too slow. Things like "this reference isn't present in this collection at this time".

Actually, this method supports quantifiers, even quantifiers over an infinite domain, but checking happens on demand. With dependent types a proof of a quantifier forall x:T. p x is a function from T to proofs of p x. So you'd only observe a failure if you tried to use that proof somewhere on an actual x:T to obtain a proof of p x. This may still be slow of course if you actually use a lot of those proofs in a computation relevant way, but the hope is that simple decision procedures can eliminate most of the checks to be executed at compile time. In current dependently typed languages you have a decision procedure that has to verify ALL checks at compile time, otherwise it will simply signal an error -- i.e. it doesn't distinguish between "I can't prove this correct" and "this is incorrect". So the idea that most of these can be eliminated at compile time isn't totally unreasonable. Additionally, in most cases, and especially those cases that are difficult to check statically, proofs are not relevant to the computation itself. They are only used to build further proofs.

In addition to static checking and dynamic checking, you'd have something like quickcheck. For instance if you have a function that should return only primes, it would have a return type like {p:nat | forall q:nat. q=1 or q=p or q mod p != 0}. Values of this type would be represented by pairs (p,F) where p is the actual integer and F is the function that takes a q and returns a proof that q=1 or q=p or q mod p != 0. That the values are indeed primes can be quickchecked by generating random values q and passing them to F. At run time if you just printed such a prime, the proof function F would not even be called so nothing would be checked. In the IDE you would get some indicator to let you know that this is still in the category "not known to be false but not known to be true either".

Maybe the part I didn't explain well is that the mapping from type annotation to logic is programmable at the language level. I'm not just saying that there is a formalization of the type system into dependent type theory. I'm saying the type library creator gets to pick the map.

That sounds interesting. I hope you find time to finish it and write that blog post :)

I assumed you'd have some form of dynamic checking. Or what will happen at run time if this cast turns out to be invalid?

I distinguish between typing and representation selection, but they're related. The rep selection process has to be concerned with issues of memory safety, if that's a property you want your reps to have, but deciding to let zero sneak through probably wouldn't affect memory safety. It could require a run-time guard in front of a divide in order to obtain no-throw guarantees. Typing doesn't have a run-time component at all. (Design of the rep selection process is sketchy... first versions of the language won't have it)

So you'd only observe a failure if you tried to use that proof somewhere on an actual x:T to obtain a proof of p x.

Two points. One is that I think this approach will be very slow if you can't eliminate almost everything. Consider binary search. If the type says it produces a maximum over all elements, then all elements being in-order is computationally relevant, so your algorithm is now at least O(n). (Am I thinking about that right?)

The other is that being able to track exactly how an assumption is used later in order for it to be checked seems like a big burden. I want to be able to state and prove that a list is in order at a certain point without necessarily proving that this assumption implies the correctness of the rest of my program. This is related to my rant about Curry Howard not being a correspondence between proof and computation, but rather between proof and proven computation. IMO it's unrealistic to expect real programs to be proofs of anything interesting.

But this does sound interesting. Is this idea something you're building or just an idea you're tinkering with?

Two points. One is that I think this approach will be very slow if you can't eliminate almost everything. Consider binary search. If the type says it produces a maximum over all elements, then all elements being in-order is computationally relevant, so your algorithm is now at least O(n). (Am I thinking about that right?)

I don't understand exactly what you mean? If you have an ordered list of elements, then the maximum will always be at the end right? Usually that something is a maximum is also expressed with a quantifier: m is a maximum of a set S if forall x in S, m >= x. That would be represented as a function from x:S to a proof that m >= x. Also in general refinement types are not computationally relevant because their proof component does not affect the rest of the computation. Refinement types embedded in dependent types as a pair (x,t) where x is the value and t is a proof that x satisfies the refinement type. To compute the answer of a program you only ever use x, not t.

For an example where it is computationally relevant, consider the nodes in a trie. Each node in a trie implements a finite map from the alphabet to child nodes. Assume the alphabet is 'a'-'z'. We could represent such a node as an array of 26 elements, where each element is of type Option[Node], with None indicating that there is no child node, and Some(c) indicating that there is. However this representation is not efficient. Optimized implementations like Hash Array Mapped Tries use a bit field of 26 bits, where each bit indicates whether that corresponding letter has a child node. Then coupled with this bit field you have a variable length array of n elements where n is the number of 1 bits in the bitfield. We could represent this as the refinement type {(bitfield,array) : (Bits[26], Array[Node]) | length(array) == popcount(bitfield)}. However this representation is still slightly wasteful. If we have 5 bits that are 1 in the bitfield, then the length of the array will be 5, but that length will be stored again along with the variable length array. That is redundant because that 5 can already be determined as popcount(bitfield).

A better way to represent this is to use a fixed length vector Vec[n,Node], because fixed length vectors do not store their length as it is implied by their type. So we can represent a node as a dependent pair (bitfield : Bits[26], Vec[popcount(bitfield), Node]). Now the length of the vector is only stored implicitly as the bitfield. We see that whereas in the previous version with the refinement type the proof that length(array) == popcount(bitfield) was not computationally relevant, in this version it is computationally relevant because it dictates the representation of the node. Essentially the assertion length(array) == popcount(bitfield) is no longer checked, but it is maintained by construction. There is no way any more to construct a node where the length of the vector is not equal to the popcount of the bitfield, since the length of the vector IS the popcount of the bitfield.

So now the expression popcount(bitfield) that appears in the type becomes computationally relevant. For instance when we construct such a node with a given bitfield, memory for popcount(bitfield) Nodes has to be allocated along with it. And when the GC traverses such a node, when it encounters the Bits[26] bitfield it has to inspect its value and compute its popcount in order to determine how many Node values it needs to traverse. I find it interesting that you can use such representations that you'd usually only see in C/C++, in a memory safe garbage collected language.

I think you're probably right that I flubbed the example, but first I want to understand this:

To compute the answer of a program you only ever use x, not t.

Is this true? Imagine that you have encoded Tries the first way, and then you want to call some code that encodes them the second way. You look around and find that there's a function cast : xs:Array[Node] -> Vec[length(xs), Node] in the standard library. When you use the proof term t to prove that length(array) == popcount(bitfield) so that you can convert from cast to the type you want, doesn't t become computationally relevant?

If you convert from the first representation to the second, you do it like this: first you call that cast function to obtain ys = cast(xs) : Vec[length(xs), Node]. Suppose at run time length(xs) = 5, then that will at run time be represented with type/metadata Vec[5,Node] and actual data the fixed length vector of 5 Nodes. Then you use the dependent pair constructor to construct (bitfield, ys) : (b : Bits[26], Vec[popcount(b), Node]). At run time popcount(bitfield) is 5, so that means that in the second component something of type Vec[5,Node] is expected. Since the type of ys is Vec[5,Node] this is compatible.

The important point is that although the dynamic check happens to make sure that length(xs) == popcount(bitfield), this is not through calling the proof term t. This check only happens because we are passing ys of type Vec[length(xs), Node] into a position that expects something of type Vec[popcount(bitfield), Node]. In particular if we had written a nonsense type like this:

{(bitfield, array) : (Bits[26], Array[Node]) | length(array) < 234}

Then this conversion would still succeed at run time as long as at run time popcount(bitfield) == length(array). Since the above type does not guarantee this, it can happen that at run time popcount(bitfield) != length(array) and this would lead to a run time error. Also in the IDE it would be indicated passing ys of type Vec[length(xs),Node] into a position that expects Vec[popcount(bitfield),Node] could not be proven to never fail.

Now to prove statically that the conversion never fails at run time, the decision procedure needs to know that popcount(bitfield) == length(array) in all cases, and this will not be possible to prove with the nonsense type, but it will be possible to prove with the right type.

Have you formalized what's going on? It sounds like you're doing something like defining an erasure operation that removes non-computational content and then allowing implicit coercion between two types that have the same erased type such that the computational part of this implicit coercion is identity. Then, even if you never find the non-computational part, that doesn't change the run-time semantics. Or something like that?

Wow. This is exactly the sort of type system that I had in mind - types with arbitrary refinements, some of which can be proven statically, and some of which influence runtime computations.

I have no idea how to formalize or implement this kind of type system, but I have tried imagining what a zip function would look like:

type list['a] = cons['a, list['a]] | nil

function zip(list1 : list['a], list2 : list['b] if length(list1) == length(list2))
  match list1, list2 with
    | cons(head1, tail1), cons(head2, tail2) -> cons((head1, head2), zip(tail1, tail2))
    | nil, nil -> nil

However, this code is rather inefficient; if the compiler isn't able to statically prove that the two lists have the same length, it has to issue a dynamic type check, which in this case means that each list is traversed twice instead of just once. To prevent that, the programmer could overload the zip function with slightly different type:

function zip(list1 : list['a], list2 : list['b])
  match list1, list2 with
    | cons(head1, tail1), cons(head2, tail2) -> cons((head1, head2), zip(tail1, tail2))
    | nil, nil -> nil
    | _ -> raise Exception("lists have different lengths")

This way, the compiler could automatically choose the most efficient code, based on the statically available information. I'm not sure yet how I would extend this from "dependent functions" to "dependent values", e.g. how could a type like vector[int, 3] be turned into a dynamic value and back again. By wrapping it in a box that carries the static length along with it maybe?

Anyways, if you have interest in discussing and developing a type system like this, I'd be glad to talk to you about it.

Combining static checking and dynamic contract verification is not a rare idea -- it's so good it spread like wildfire. See Sage, hybrid contract checking for OCaml, or to some extent Liquid Haskell (it's only static checking, but I couldn't resist).

I wanted to cite the excellent Racket work as well, but the work I know about focuses on excellent static type checking or dynamic contract checking, but not so much hybrids with refinement-like static parts. Hopefully another LtU reader can chime in with more information.

Thanks, these are really interesting links. I don't really like Sage, as the types it infers are rather long, useless and unevaluated. Hybrid contract checking and Liquid Types are really interesting though. I've got a lot of papers to read.

I want to be able to state and prove that a list is in order at a certain point without necessarily proving that this assumption implies the correctness of the rest of my program.

Right, you can still do this. If you have some_list : {xs : List[Int] | ordered(xs)}, then you can still prove that independent of what the rest of the program does with that list. In order to do this you need to write the code that constructs some_list in such a way that the decision procedures of the type checker can see that ordered(xs) will always be True (just like in dependently typed languages).

But this does sound interesting. Is this idea something you're building or just an idea you're tinkering with?

Whether this can go beyond a toy depends on whether or not I can solve a number of issues. As you can imagine it is very unpleasant to program with dependent types without implicit parameters...

I tend to think of typecase, reflection, etc. as orthogonal to the concept of static vs. dynamic types. Some statically typed languages enable a high degree of reflection. And there are a rare few dynamically typed languages that offer no concept of typecase or 'message not understood', etc..

Conjecture: Dynamic without ambient authority for reflection or side-effects would be a sweet target for pluggable type systems.

And isn't a dynamic language without typecase even simpler than one with it?

Regarding 'null' - that's a form of accidental complexity. It certainly isn't essential to dynamically typed languages. I agree we should do without it. I prefer structural sum types (e.g. `() + a` instead of `Option a`) for a lot of reasons, but I agree we should address these more explicitly.

dynamically typed languages implicitly work with a sum type of all types

There's a big difference between "any variable can contain any type of value" and "any function can process any type of value". It is my understanding that 'dynamic typing' refers only to the former. :)

making a distinction between "can't prove that this code is type correct" and "this code is definitely type incorrect" would help a lot

I heartily agree.

no way to accurately describe a list of integers as metadata in a dynamically typed language

Well, it's certainly possible to infer that a list should contain only integers, even if it isn't explicitly described anywhere. It also seems feasible to express such a property in a manner amenable to inference - e.g. based on applying a fold function that simply asserts each argument is an integer.

one problem with this approach that I haven't figured out is how to do type classes/implicit parameters in such a language [..] doing it at run time also has complications that I won't go into here

I've been approaching this problem in terms of modeling a 'make' system in an Applicative, i.e. such that developers can require/provide named global interfaces (global only with respect to the Applicative) and this is addressed as a static constraint solving problem. OTOH, I've sacrificed conventional models of separate compilation to make such features feasible at compile time.

About nominal vs structural typing [..] structural by default, but there should be some construct to wrap an existing type into a nominally typed "box"

I understand the motivation, though I favor a structural model even for the "box". Value sealing seems a very simple, useful basis for modeling such boxes if you need information hiding. If representation independence isn't important, then simple pairing of a value with some unit metadata can perform admirably.

And isn't a dynamic language without typecase even simpler than one with it?

Yes but also significantly less expressive. You lose almost all of the benefits commonly associated with dynamically typed languages. If you don't have typecase then what you have is quite a different beast compared to what most people would understand as a dynamically typed language.

Regarding 'null' - that's a form of accidental complexity. It certainly isn't essential to dynamically typed languages.

I think it is quite essential to dynamically typed languages that programmers can write such programs. Sure, null itself doesn't need to be built-in, but you can always define your own MyNull. The more general problem is that dynamically typed languages allow you to implicity use union types (not sum types) in such an ad hoc way that is fragile under unforeseen circumstances, such as when T can also be null.

There's a big difference between "any variable can contain any type of value" and "any function can process any type of value". It is my understanding that 'dynamic typing' refers only to the former. :)

I don't understand what you mean by this distinction. Can you give examples of languages where "any variable can contain any type of value" and of languages where "any function can process any type of value"?

I understand the motivation, though I favor a structural model even for the "box".

I don't understand what you mean here either. Could you elaborate on what you mean by a structural model of the box?

People tend to conflate language properties based on the bundles they've seen before. Care to make a guess how many people think "object oriented" when you say "dynamically typed"? But that doesn't mean the properties are intrinsically related.

Erlang is a pretty decent example of a language with dynamic types that does not, idiomatically, make heavy use of typecase. A consequence is that Erlang is subject to a fair amount of safety analysis, e.g. via a tool called 'dialyzer'. But Erlang still has a very dynamic feel.

Eliminating pervasive access to typecase does reduce expressiveness. But I think this isn't a problem. Even without typecase, we're still more expressive than a static language with precise, dependent typing. Isn't that enough?

I don't understand what you mean by this distinction.

I simply mean that, for example, `a + b` doesn't always need to return a value. It doesn't even need to return 'message not understood'. For some pairs of values, it can simply halt the whole program. In this case, we have dynamic types (because `a` and `b` may carry any value) but we also have a clear notion of invalid programs.

This observation directly contradicts your position that "dynamically typed languages implicitly work with a [union] type of all types". Because we aren't working with all types. And this is important! When we work with a smaller subset of types or values, we can usefully infer type refinements.

Could you elaborate on what you mean by a structural model of the box?

I already elaborated two ways to structurally model such boxes: value sealing, and pairing with units. I believe you're familiar with these concepts.

Value sealing works in a simple way. A value is sealed with a given sealer, maybe uniquely identified by text 'dateTime'. The sealed value cannot be observed or manipulated without first unsealing it with the corresponding unsealer. Thus, the 'dateTime' sealer acts much like a newtype constructor without introducing a concept of nominative types.

Erlang is a pretty decent example of a language with dynamic types that does not, idiomatically, make heavy use of typecase. A consequence is that Erlang is subject to a fair amount of safety analysis, e.g. via a tool called 'dialyzer'. But Erlang still has a very dynamic feel.

It was my understanding that in Erlang you can pattern matching on values of different types in the same pattern match. Now whether or not that is actually common is a separate question, but Erlang makes it easier than most other dynamically typed languages to write a typecase. If one is not careful, this brings with it the issue of conflation of different values that I described above.

Even without typecase, we're still more expressive than a static language with precise, dependent typing. Isn't that enough?

Except you are not, because in a dependently typed language you can have type classes that give you more expressiveness than what you have in the dynamically typed language while not having the same problems that typecase has.

This observation directly contradicts your position that "dynamically typed languages implicitly work with a [union] type of all types". Because we aren't working with all types. And this is important! When we work with a smaller subset of types or values, we can usefully infer type refinements.

This all hinges on how you interpret all these imprecise words like "process". I don't think this is terribly relevant to this discussion, since terminating the program or otherwise signaling that an invalid type is being passed does not solve this problem. The problem is not that a type is being passed that is explicitly excluded, but that the same type is used with different meanings. For instance in a statically typed language you can have Option which contains both None and Some(None) which are distinct values. One has to be very careful to do the same wrapping of Some(None) in the dynamically typed program to distinguish None from Some(None), whereas in the statically typed program you can't even express the wrong but tempting dynamically typed solution.

Another example of such a potential conflation that is not about null can be found in the wild in MiniKanren. In MiniKanren you have logic variables, and you have lists and atoms. Lists are represented as Scheme lists, atoms are represented as Scheme atoms. Logic variables are represented as a vector containing a single element that is a unique identifier for that logic variable. All MiniKanren values are either lists of MiniKanren values, or atoms, or logic variables. This works fine because the logic programming language that MiniKanren implements does not itself support vectors as values. However if MiniKanren were to be extended to support vectors, a conflation between logic variables and vectors would happen. In a statically typed language like Haskell you would not even be able to express this. You would be forced to do the right thing from the start and define a sum type of all the values in your language that looks something like this:

data Value = List [Value] | Atom String | LogicVariable UniqueID

This could then be extended with support for vectors without problems.

Value sealing works in a simple way. A value is sealed with a given sealer, maybe uniquely identified by text 'dateTime'. The sealed value cannot be observed or manipulated without first unsealing it with the corresponding unsealer. Thus, the 'dateTime' sealer acts much like a newtype constructor without introducing a concept of nominative types.

Well, if I understand you correctly these are dynamically checked solutions. Since we were talking about nominal vs structural typing, we need a statically checked solution. If you mean that such a sealer does not actually do anything to the value, but only acts on the type of the value so that it has no run time effect, then we mean the same thing but then I don't see in which sense such a sealer is structural and how that is distinguished from other sealers that would be not structural in that sense of structural.

The problem is not that a type is being passed that is explicitly excluded, but that the same type is used with different meanings. [..] terminating the program [..] does not solve this problem

The problem you describe is fundamentally one of API design. The best a type system can do is align the path of least resistance with good API design and good performance.

Terminating the program plays an indirect role. As opposed to signaling or other observable failure, termination simplifies static analysis of dynamically typed code, i.e. by eliminating the possibility that an error exist in order to cause a signal. If we simplify static analysis, we can encourage idioms that leverage it.

One has to be very careful to do the same wrapping of Some(None) in the dynamically typed program to distinguish None from Some(None), whereas in the statically typed program you can't even express the wrong but tempting dynamically typed solution.

I think this claim doesn't generalize well. It seems you're comparing Scheme to Haskell, not 'dynamically typed languages' to 'statically typed languages'.

if I understand you correctly these are dynamically checked solutions. Since we were talking about nominal vs structural typing, we need a statically checked solution.

Valid use of sealed values is easy to check statically, even in a dynamically typed language. In context of pluggable typing, I would expect most seal/unseal actions to be validated statically.

Value sealing is structural because it formally operates on the structure of a value. Even text like 'dateTime' is part of the structure, not part of a separate namespace. In some contexts it is feasible to implement value sealing in terms of a few attributes in a type system, such that it has no static presence. But that's just an implementation option.

in a dependently typed language you can have type classes that give you more expressiveness

A pluggable type system cannot use type-driven dispatch, but there are other options for expressiveness.

The problem you describe is fundamentally one of API design. The best a type system can do is align the path of least resistance with good API design and good performance.

This was exactly my point: "I don't think that we'll manage the same level of simplicity as dynamically typed languages, but I don't think that would be a good thing either. Dynamic typing is simpler because it doesn't force you to think about types. But often thinking about types is a good thing. [...] So there is a line between simple and simplistic."

Valid use of sealed values is easy to check statically, even in a dynamically typed language.

Seeing is believing in this case...In my experience you quickly run into the halting problem as soon as you try to analyze anything about dynamically typed code. More generally, you tend to run into the halting problem if the code isn't specifically crafted to be amenable to the kind of analysis that you want to do. e.g. like you have to write code in a certain constrained way in a statically typed language so that it can be analyzed by the type checker.

Even text like 'dateTime' is part of the structure, not part of a separate namespace.

If it is merely the text 'dateTime' that gives you access to the internal value then it is not true sealing, since anyone can get the value out that way. But since you haven't specified how exactly you intend to do this sealing, it's really impossible to evaluate it. Maybe you mean that it's easy to do dynamically checked value sealing on top of an existing language, which is true, but that's not what this discussion was about. I think the best way to go here is to just have a proper module system that allows information hiding.

A pluggable type system cannot use type-driven dispatch, but there are other options for expressiveness.

No doubt about that :)

Dynamic typing is simpler because it doesn't force you to think about types. But often thinking about types is a good thing.

Ah, my point was that this is not a distinguishing characteristic. Static typing has the same property. Indeed, I have several twitter follows who regularly complain about "stringly typed programs" in strongly typed languages (i.e. where every value is shoved into a string). Use of a single integer for different kinds of return values isn't unusual (error codes, sentinels, results). Exceptions and nullable values and unboxed sums in statically typed languages can also accumulate multiple meanings.

There is no such thing as a type system that forces you to think about types. The best we can do is encourage it. The whole static/dynamic position seems almost entirely orthogonal to this.

you tend to run into the halting problem if the code isn't specifically crafted to be amenable to the kind of analysis that you want to do

If you want 'sound' types (never pass a program that might fail at runtime) then this might be a problem. But if your goal is simply to find as many errors as you can, distinguishing (as you mentioned earlier) "certainly incorrect" from "could not decide", then you can do a lot of good work without encountering the halting problem.

It isn't as though humans think in deep ways about program correctness, so - assuming we wish to reason about code at least as well as humans do - it's more useful to have many shallow proof strategies (e.g. via pluggable types) than a few deep ones.

In my experience, the big limitation on analyzing dynamic languages has been their tendency to admit all code. E.g. "message not understood" isn't an error, it's just an indicator that can support other dispatch logic. Or `+` between a number and a string isn't an error, it's just a way to implicitly stringify the number. (Automatic conversions are awful for analysis.)

If it is merely the text 'dateTime' that gives you access to the internal value then it is not true sealing, since anyone can get the value out that way.

It isn't secure sealing in this case. Secure sealers must be constructed in a secure manner; origin matters. But an insecure sealer is still useful in the same sense 'newtype' is useful.

In my particular implementation, the text 'dateTime' must be hard-coded as part of the sealer, because there are no ambient operators to translate plain text to capability text. So: `%{$dateTime}` for the sealer, and `%{/dateTime}` for the unsealer. This makes it relatively easy to search for all instances in a codebase.

The important bit is that developers need either to know statically which unsealer they need to use, or at least how to find out. If they use the wrong one, the program halts or a static analysis rejects the code.

Aside: I allow hard-coding only of non-operational capabilities. A sealer is non-operational because you can't ever observe its presence or failure. If your code is correct, then you can remove all seal/unseal actions and it would still have the same observable behavior. Performance annotations are another example of non-operational capability.

the best way to go here is to just have a proper module system that allows information hiding

A module system will work, but it also requires additional concepts and coupling of responsibilities (information hiding + bundling). It isn't at all clear to me that a module system is the best option. My intuition is that we can do better, e.g. by focusing on composition, and separation of responsibilities.

... which is a language that has only a fixed number of built-in dynamic types. That's not normal for dynamically typed languages nowadays. In addition, it would be perfectly possible to implement its logic variables not as vectors but as lists whose car is a unique and inaccessible sentinel object. There are several ways to create such objects in Scheme, including (cons 'whatever) and (copy-string "whatever"). So the MiniKanren representation is basically a matter of convenience, not something fundamental to dynamically typed languages.

In dynamically typed languages you often see functions that either return some type T or null. This works most of the time until T itself can be null.

It actually works all the time, provided you do not have to overload the meaning of null for hysterical raisins. In Lua, Smalltalk, JavaScript, and SQL, null/nil works fine, because it doesn't have to double as false or the empty list or a pointer to nothing. (There are other problems with null in SQL, but they have to do with trivalent logic.)

There is no way to accurately describe a list of integers as metadata in a dynamically typed language that tags values that way. This means that you have to invent some additional mechanism to describe that, so now you have two metadata systems.

Can you clarify this? In core Common Lisp, types are named using symbols and lists thereof: T is a type, and so is (LIST INTEGER), so metadata is data. The selfsame representation is used at run time as an argument to various functions of types, and in compile-time declarations. Where's the need for two metadata systems?

It actually works all the time, provided you do not have to overload the meaning of null for hysterical raisins. In Lua, Smalltalk, JavaScript, and SQL, null/nil works fine, because it doesn't have to double as false or the empty list or a pointer to nothing. (There are other problems with null in SQL, but they have to do with trivalent logic.)

Even if you distinguish the empty list and false from nil, the problem remains. Suppose you have a hash table that maps person names to date of death. Some people haven't yet died, so in that case we set their hash table entry to nil to indicate that they have no date of death. In some dynamically typed languages you also get nil if you try to look up a value in a hash table that is not in it. So now if you look up a name in the hash table and we get nil, is the meaning of that that that person hasn't yet died, or is the meaning of that that the person isn't in our data structure?

In a proper statically typed language such a conflation isn't even possible. The lookup function of a hash table would have type HashTable[Key,Value] -> Option[Value]. The type of our hash table in this example would be HashTable[String, Option[Date]]. So if we look up a person's name in it, we get a value of type Option[Option[Date]]. Here we get two kinds of null: None and Some(None). None means that the person isn't in our hash table, and Some(None) means that it is known that the person hasn't died yet.

(apologies for all this death, it was the first example that came to mind)

This is just one way in which the implicit union type of dynamically typed languages can cause conflation. In a response to dmbarbour I gave another example that is unrelated to nil.

Where's the need for two metadata systems?

This (LIST INTEGER) metadata is seperate from the type tags that are attached to each (pointer to) cons cell and integer. So there are still two kinds of metadata: metadata that is known at compile time and the metadata that is known at run time. The fact that '(LIST INTEGER) is itself a list is a totally different issue.

None means that the person isn't in our hash table, and Some(None) means that it is known that the person hasn't died yet.

The surrounding code can easily maintain an invariant such that it won't try to look up the date of death of an unknown user. If I had to do a few dozen operations on a particular username, each of which had two notions of null, when I only really need one, then I have to write a bunch of unwrapping code and make heavy use of maybe-monad-style mechanisms. The problem gets worse when you have N-levels of Option instead of just two.

So now if you look up a name in the hash table and we get nil, is the meaning of that that that person hasn't yet died, or is the meaning of that that the person isn't in our data structure?

It means precisely that: "This person doesn't exist OR they are dead". That's probably enough, but in the context of the invariant "This username is definitely in the hash table", then it means "they are dead". If you don't have such an invariant and need to distinguish, you can use a lookup function that returns a union type of (KeyValuePair | Null) to answer the presence question and destructure the key value pair to answer the alive/dead question.

Clojure, for example, has both get and find.

No, this is terrible, because it isn't compositional. The particular point Jules was making is that when you have an abstraction that is generic in some type T, then you want to be sure that type T cannot be confused with Option(T), no matter what T is instantiated with later. In general, clients of an abstraction have no way of even knowing about the potential risk for this confusion, because it might not even be apparent from the interface of the abstraction, which could just be using an Option(T) internally.

Sure, in principle you can always work around the problem by wrapping all values of type T manually in your abstraction, but (1) that is even more expensive, and (2) in practice nobody remembers doing it, and (3) if they don't, they also won't remember to document their generic APIs telling clients that they have to do it.

Prediction: in 25 there will still be optimists.

In 25 years there will still be ill-specified problems for which making progress requires flexibility at the expense of ahead-of-time safety. Lisp will never die.

Hah! Maybe I picked 25 years because it's far enough out that I there's very little chance that I'd ever have to answer for being wrong. :)

To be honest, I've been predicting this for over twenty years now, I was just being snarky... So who knows?!

Undecidable doesn't mean unsafe. I believe we could develop systems that operate within a weaker constraint than you are assuming: IF typechecking terminates with acceptance THEN the runtime program is safe - i.e. semidecision. A kind system is optional.

Also, even if we try to pose this as a regression, it seems to me that "just as subject to error as the Turing-complete run-times" is trivially false because run-time errors often arise from side-effects that may be unavailable at compile-time. There is much value in staging of computations and effects to support safety analyses.

Maybe we'd be better off turning languages upside down: Turing-complete compile-times that guarantee termination or progress at run-time. Compile-time is, after all, easier to debug: the programmer is right there.

Even for a continuous build server, the programmer is still there - and further will have a pretty good idea of how much time it should take to build.

If you can execute arbitrary code at compile time (as in a Common Lisp, C++, or R6RS Scheme compiler) then it's unsafe to continuously build, as there is no guarantee that any of the compilations actually terminate. I don't know what you mean by "still there" in any case; my code may be fine, but if someone else checks in uncompilable code that is built alongside mine, all bets are off.

Would you also argue a web browser is unsafe because web pages can execute arbitrary code? Or that a web server unsafe because you cannot guarantee, in general, that a query will terminate because of server-side scripting? If so, then you're clearly using browsers and servers and what you call unsafety must be less objectionable to you than you're implying. If not, then perhaps you have a double standard - your definition of 'safe' would not be consistent between run-time and compile-time.

Really, the worst that could happen is you must do some process control, e.g. to limit the number of versions of code being compiled at a given instant. But process control would be desirable ANYWAY, even for guaranteed termination, if it can take more than a few seconds.

The important feature, as always, is that developers of the code can comprehend and control performance. The structurally-enforced or typeful guarantee of termination is much less valuable at compile-time when the developers can most readily get feedback and fix problems. There isn't much utility in provable termination at compile-time unless you already have that guarantee for run-time. There is no good argument that compile-time should terminate when it simply means developers shift necessary but potentially divergent computations to the run-time. It's always worse to diverge at run-time than to diverge at compile-time.

Would you also argue a web browser is unsafe because web pages can execute arbitrary code?

Many people do, notably those who run with JavaScript turned off. But I'm not one of them, and yes, I don't consider safety the most important point in all circumstances. I made this very argument to a critic of R7RS-small who complained that it doesn't require safety: my counter was that in some cases people prefer fast compilation or fast execution to safety, and a conformant implementation should be able to provide that either as an option or as its raison d'etre.

It's always worse to diverge at run-time than to diverge at compile-time.

If by that you mean that it's less likely to damage users, who are around at run time but not at compile time, then I certainly agree.

I had an analogous conversation with Felix Winkelmann about the behavior of the Chicken Scheme compiler in the presence of "inline" declarations (which are not part of the Scheme standard). In Common Lisp, "notinline" declarations must not be ignored, whereas "inline" declarations may be ignored. Chicken was always inlining whenever a declaration was present, on the grounds that the programmer's intention must be obeyed even if that sent the compiler into an infinite inlining loop. My counterargument, which was apparently convincing, was that the programmer could never intend an infinite loop at compile time (whereas for some programs, an infinite but effectful loop at run time is the Right Thing). (By the same token, "notinline" is a signal from the programmer that the compiler's decision to inline is based on insufficient information, such as that the program will be run using a runtime-only debugger.)

Termination is interesting as a theoretical property, but as a practical matter or from a security standpoint, a proof of termination is useless. As a practical matter, hard bounds on time and other resource usage would be useful, but there's usually no difference in practice between a program that terminates in a year and one that doesn't terminate.

Termination is interesting as a theoretical property, but as a practical matter or from a security standpoint, a proof of termination is useless.

Not always. In particularly flexible type systems, like the recently discussed pure subtype systems and systems with Type : Type, a proof termination is a proof of soundness and completeness, respectively.

I acknowledged that it's useful as a theoretical property, but maybe I should have said it has no intrinsic usefulness.

"Top-down design is a great way to redesign a program you already know how to write." — P.J. Plauger, "Which tool is best?", Computer Language 3 no. 7 (July 1986).

i wouldn't like a dynamic language that never let me put in the types. for me personally i find that often worse than a language that requires type annotations. of course i think the best is in the middle, where you can progressively add the types as you want. (random e.g. qi lisp which had optional static type checking. or ocaml, or haskell, et. al. -- although generally speaking you do want to write down the types up front 'cause it will make compiler errors a lot more sane, i guess.)