Curious how this relates to what lean4 is doing, I guess in lean's case some of the data structures are special cased (Array) and there is no easy way to implement such data structures yourself
Interesting stuff. I didn't read the whole paper in detail. I'm unclear on how FIP differs from adding uniqueness types to a language. A number of languages are exploring this (Rust being the most well known) so what's the novelty that FIP brings?
Whereas uniqueness qualifiers on values or references are a semantic component of a languages terms, FIP is more akin to a polymorphic System F based language having restrictions on term formation to enable decidable type inference.
Uniqueness types (which Rust can only be said to have as an implementation detail of the borrow checker’s running, as opposed to having programmer assignable uniqueness qualifier syntax for construction of types) are semantic constructs that a user places on types which then restrict the operations available for that object. In this paper and in Koka, the language that semi-inspired the exploration here, the functional-in-place mutation scheme is an optimization performed by the compiler in those cases where the resulting code is probably equivalent to the surface level syntax. Said surface level syntax presenting a logical view of the program as only have persistent, immutable objects.
The implicit novelty, although this paper is more an exploration of existing concepts in a specific environment (i.e. no GC at run time), is that there is no annotation burden or conceptual distinction to be made by users of the language to receive the performance benefits of mutation where available.
Seems like this is a step in that direction.
It’s neat what falls out of type theory. Counting Immutable Beans was another eye-opening paper worth reading if you’re curious like me.
reply