My full and proper response to this was sent to the mailing list. Since we appear to have at least one Rust person here and the mailing list may have blocked the email or something, I'm CC'ing here.
Hey, I saw this linked on Hacker News, so I thought I would give it a read. And boy, this is a strange one. It's like watching a painful portion of my life flash before my eyes, and realizing someone else lived it before I did. I can't say how much I and my work owe to you and BitC. Seriously, thank you for all your effort and for having the courage to do a public autopsy of your own language.
I've seen everything you said about the compilation model happen in my own attempts. My only way of slinking around that issue has been to output to a bitcode able to do link-time resolution of opaque/abstracted type representations. This means that I have to allow for some whole-program tracking of abstracted representations. It leaves a bad taste in one's mouth, but it can be... workable. Its downside is that representation sizes have to be specified for abstracted types exported as binary blobs from libraries, because the library client's dynamic linker (to my knowledge) cannot see inside the existential. I need the same whole-program tracking to perform polyinstantiation (although theoretically the typed IR language would admit code to copy it and then resolve an Opaque Type to an instantiation).
Ideally, I think we'd compile a New Systems Language down to a Typed Assembly Language, and the portion of the compiler dealing with polyinstantiation and type abstraction would retain access to generated TAL code. Work on TALs is ongoing.
On the fortunate side, C++ already had an ABI problem with exporting classes from shared libraries. C++ requires both programmers use C++, and both to use the same C++ ABI. Yick.
I have ended up having to "add back" regions into my own language just this year. Pointers have ended up being just another type constructor, and they do have to be associated with both a region and a mutability. The good news is that once you do associate them, the region can be a universal variable; a function can be polymorphic in the region it touches by taking a pointer as a parameter.
The good news is: inference, polymorphism and subtyping do get along. They get along just fine, if you're willing to toss Top, Bottom and principal typing out the window in the special case where HM unification would end with a polymorphic generalization. Consistently viewing this problem as impossible (either a full semi-unification problem or a failure of the existence of principal types) has, I've noticed, been holding back certain strands of PL thought for a long time.
Once you have subtyping, you can introduce existential types (possibly with a restriction such as "existentials can only be used in the this-pointer place") and recover a fair approximation to objects, interfaces, BitC capsules, etc. Since we're dealing with existentials, there's also a strong resemblance and possibly even a full morphism to first-class modules, thence to type-classes and instances... And then we all get lost in how deep our thoughts are.
The lexical resolution issues of type-classes (especially with respect to their "looking like" object instances) can be dealt with as by Odersky et al in "Type-Classes as Objects and Implicits". That leaves us with the same instance-coherence issues you've already mentioned (was my ordered set built with this partial ordering or that partial ordering?), but no problem of ambient naming or authority. There might be a good hybrid approach in allowing only one truly global type-class instance per type, accessible via a special way of capturing the instance as an implicit parameter/value, but lexically resolve instances when we don't want the One True Instance. Then we could use object identity for testing instance equality to check, when given data built based on multiple instances, that they agree.
Moving on, I've got a question: why did you tackle the problem of inference and mutability together by trying to treat mutability as part of the data type?
Look at it from the C/C++ point of view rather than the ML point of view, and it sort of stops making sense. An integer value can be passed to a parameter expecting an integer, whether or not the procedure will modify the parameter slot in which it received the integer. In an imperative language, if we want to actually modify the parameter, we pass it by reference ("var i: integer" in Pascal) or by passing a pointer ("int i" in C). In ML or Haskell, I'd say it makes sense to classify mutable slots/references to mutable memory cells as their own data-type because everything* other than referenced memory cells is immutable. Those mutable cells are not real values: the reference to one is a real value, and the contents of one is a real value, but the memory cell itself is not a first-class citizen of the language.
I sidestepped the issue for my own work by treating mutability as the property of the "slot" (the memory cell itself), which is a second-class citizen of the language, and then building pointer types that track the mutability of the slot to which they point. This is (once again) much easier to do once you already know you can handle subtyping ("submuting", haha, a vastly incomplete start of a short paper). For a systems language, I admit to having gone "the C way" with a little more formalism rather than "the ML/Miranda/Haskell way".
But why go the ML/Haskell way in the first place? Just because doing things that way makes you more publishable in PL? You seem to be implying that, but I'm fairly sure the OO-PL community has their own literature on constancy and mutability ("Ownership and Immutability in Generic Java" being a paper I've seen referenced fairly often) that you could have dragged in to "shield yourself" against the ML/Haskell-style FP-PL community (and its horrifying armies of conference reviewers!).
Anyway, my condolences for the death of your language by starvation of funding. It really sucks to see BitC go when you've learned so much about how to do BitC right, but you definitely did manage to make a ton of important contributions. Though, since I should ask, did you ever talk to or collaborate with the Cyclone folks? Habit folks? ATS folk(s)?
The line between self-promotion and useful contextual information can be a fine one. But in this case, I think mentioning the source of your own experience is OK, since it's directly relevant to the discussion and it establishes the context for your comment.
I dunno about that. This clarifies to me that what I just read was not about "some guy's language", but "that language I saw on LtU, that's on the top of my stack of languages to look at." :-)
Hey, I saw this linked on Hacker News, so I thought I would give it a read. And boy, this is a strange one. It's like watching a painful portion of my life flash before my eyes, and realizing someone else lived it before I did. I can't say how much I and my work owe to you and BitC. Seriously, thank you for all your effort and for having the courage to do a public autopsy of your own language.
I've seen everything you said about the compilation model happen in my own attempts. My only way of slinking around that issue has been to output to a bitcode able to do link-time resolution of opaque/abstracted type representations. This means that I have to allow for some whole-program tracking of abstracted representations. It leaves a bad taste in one's mouth, but it can be... workable. Its downside is that representation sizes have to be specified for abstracted types exported as binary blobs from libraries, because the library client's dynamic linker (to my knowledge) cannot see inside the existential. I need the same whole-program tracking to perform polyinstantiation (although theoretically the typed IR language would admit code to copy it and then resolve an Opaque Type to an instantiation).
Ideally, I think we'd compile a New Systems Language down to a Typed Assembly Language, and the portion of the compiler dealing with polyinstantiation and type abstraction would retain access to generated TAL code. Work on TALs is ongoing.
On the fortunate side, C++ already had an ABI problem with exporting classes from shared libraries. C++ requires both programmers use C++, and both to use the same C++ ABI. Yick.
I have ended up having to "add back" regions into my own language just this year. Pointers have ended up being just another type constructor, and they do have to be associated with both a region and a mutability. The good news is that once you do associate them, the region can be a universal variable; a function can be polymorphic in the region it touches by taking a pointer as a parameter.
The good news is: inference, polymorphism and subtyping do get along. They get along just fine, if you're willing to toss Top, Bottom and principal typing out the window in the special case where HM unification would end with a polymorphic generalization. Consistently viewing this problem as impossible (either a full semi-unification problem or a failure of the existence of principal types) has, I've noticed, been holding back certain strands of PL thought for a long time.
Once you have subtyping, you can introduce existential types (possibly with a restriction such as "existentials can only be used in the this-pointer place") and recover a fair approximation to objects, interfaces, BitC capsules, etc. Since we're dealing with existentials, there's also a strong resemblance and possibly even a full morphism to first-class modules, thence to type-classes and instances... And then we all get lost in how deep our thoughts are.
The lexical resolution issues of type-classes (especially with respect to their "looking like" object instances) can be dealt with as by Odersky et al in "Type-Classes as Objects and Implicits". That leaves us with the same instance-coherence issues you've already mentioned (was my ordered set built with this partial ordering or that partial ordering?), but no problem of ambient naming or authority. There might be a good hybrid approach in allowing only one truly global type-class instance per type, accessible via a special way of capturing the instance as an implicit parameter/value, but lexically resolve instances when we don't want the One True Instance. Then we could use object identity for testing instance equality to check, when given data built based on multiple instances, that they agree.
Moving on, I've got a question: why did you tackle the problem of inference and mutability together by trying to treat mutability as part of the data type?
Look at it from the C/C++ point of view rather than the ML point of view, and it sort of stops making sense. An integer value can be passed to a parameter expecting an integer, whether or not the procedure will modify the parameter slot in which it received the integer. In an imperative language, if we want to actually modify the parameter, we pass it by reference ("var i: integer" in Pascal) or by passing a pointer ("int i" in C). In ML or Haskell, I'd say it makes sense to classify mutable slots/references to mutable memory cells as their own data-type because everything* other than referenced memory cells is immutable. Those mutable cells are not real values: the reference to one is a real value, and the contents of one is a real value, but the memory cell itself is not a first-class citizen of the language.
I sidestepped the issue for my own work by treating mutability as the property of the "slot" (the memory cell itself), which is a second-class citizen of the language, and then building pointer types that track the mutability of the slot to which they point. This is (once again) much easier to do once you already know you can handle subtyping ("submuting", haha, a vastly incomplete start of a short paper). For a systems language, I admit to having gone "the C way" with a little more formalism rather than "the ML/Miranda/Haskell way".
But why go the ML/Haskell way in the first place? Just because doing things that way makes you more publishable in PL? You seem to be implying that, but I'm fairly sure the OO-PL community has their own literature on constancy and mutability ("Ownership and Immutability in Generic Java" being a paper I've seen referenced fairly often) that you could have dragged in to "shield yourself" against the ML/Haskell-style FP-PL community (and its horrifying armies of conference reviewers!).
Anyway, my condolences for the death of your language by starvation of funding. It really sucks to see BitC go when you've learned so much about how to do BitC right, but you definitely did manage to make a ton of important contributions. Though, since I should ask, did you ever talk to or collaborate with the Cyclone folks? Habit folks? ATS folk(s)?
--Eli