u/LPTK

You may be interested in a paper we published last year on a somewhat related topic: A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation With Constraint-Based Subtype Inference.

In many programming paradigms, some program entities are only valid within delimited regions of the program, such as resources that might be automatically deallocated at the end of specific scopes. Outside their live scopes, the corresponding entities are no longer valid – they are permanently invalidated. Sometimes, even within the live scope of a resource, the use of that resource must become temporarily invalid, such as when iterating over a mutable collection, as mutating the collection during iteration might lead to undefined behavior. However, high-level general-purpose programming languages rarely allow this information to be reflected on the type level. Most previously proposed solutions to this problem have relied on restricting either the aliasing or the capture of variables, which can reduce the expressiveness of the language. In this paper, we propose a higher-rank polymorphic type-and-effect system to statically track the permanent and temporary invalidation of sensitive values and resources, without any aliasing or capture restrictions. We use Boolean-algebraic types (unions, intersections, and negations) to precisely model the side effects of program terms and guarantee they are invalidation-safe. Moreover, we present a complete and practical type inference algorithm, whereby programmers only need to annotate the types of higher-rank and polymorphically-recursive functions. Our system, nicknamed InvalML, has a wide range of applications where tracking invalidation is needed, including stack-based and region-based memory management, iterator invalidation, data-race-free concurrency, mutable state encapsulation, type-safe exception and effect handlers, and even scope-safe metaprogramming.

It was mentioned in a Mojo design discussion (I just noticed I forgot to respond to it).

Do the students get anything out of it (i.e. financial help attending the event itself), or is it just volunteering for the sake of it?

Yo udo not get any tangible benefit from it, but you do get the bragging right of putting it on your CV, which an help if you're interested in an academic career ;^)

Not saying there would be much wrong with the latter, but I think clearly stating which one it is would be a good idea.

Thanks for the feedback!

It does work, thank you!

Thanks a lot for your investigation; it helped reassure me that the behavior was not intended, which made it easier to endure while it lasted :^)

Following a recent update, the problem has now disappeared!

OCaml already is like this with its polymorphic variants and objects. You absolutely can write entire applications without a single type definition or annotation.

Turns out it's not particularly glorious, and people usually recommend against using these features when possible. They notably make type errors harder to parse, and can even lead to subtle mistakes slipping through and causing runtime bugs (such as mistyping a constructor name when it's only later consumed by pattern matches with default cases, so it does not lead to a type error because it's still technically well-typed).

Cc /u/hshahid98

Thanks for responding.

Yes, I am sure. This is a new behavior, which started happening on all my machines.

Does it behave differently for you?

For anyone stumbling on this: /u/church-rosser is full of it and has no idea what they're talking about. (This is coming from an actual expert in the field.)

Sure, I think it will do. We just want to know who you are.

I'm sorry, what?

Ah thanks for pointing it out, I read it too fast on my phone.

(Regular languages are non-recursive, and context-free grammars are recursive, but it does not follow that all lexers are regular, and all parsers are CFGs! )

This sounds quite confused to me. Lexers and parsers are implementations (algorithms, not languages). Whether the languages they recognize are regular or context-free has nothing to do with whether they use recursion.

As soon as you have matching parentheses, your language isn't regular...

Oh no, I'm not talking about escape hatches. I'm talking about Cell types, which are mutable on the inside even when viewed as immutable by Rust from the outside. These are the most common way to implement many types of data structures where the borrow-checker is too limiting, including mutable data structure with any amount of sharing. They're a standard feature.

Yes, but like in C++ this does absolutely nothing to prevent the value's insides from being mutated. So it's irrelevant to the discussion at hand.

Sorry, but you seem to be quite confused.

Rust is imperative and has no support for immutability whatsoever. The closest it has is static tracking of outer mutability, but things are still free to be internally mutable. 

And building efficient immutable abstractions and libraries is much easier in any language with a GC, including in Java and Go.

Note that TypeScript's conditional types don't have well-defined semantics and are very easily unsound. Also, your signature wouldn't work if Array was invariant (as it should be).

What you really want is proper negation types. I wrote a paper on a research language where the flatten definition can be typed essentially as:

flatten:
  (#Cons & {h: 'a, t: 'a} | Nil | 'h & ~#Cons & ~#Nil) as 'a
  ->
  (#Cons & {h: 'h, t: 'b} | Nil) as 'b

This is a principal type (the language has principal type inference). The function implementation is:

rec def flatten x = case x of
    Nil -> Nil{},
    Cons -> concat (flatten x.h) (flatten x.t),
    _ -> Cons { h = x; t = Nil{} }

See: https://github.com/hkust-taco/mlstruct/issues/2

while there are still some remaining cases where static type systems struggle to represent dynamic idioms, it’s mostly an ergonomics/engineering/mild research effort at this point

Well I guess that's why my recent grant proposals kept being shot down :^P

Yeah, the problem is that TS decided that {field:0} could be assigned type A, which makes zero sense, as that object is not and instance of class A at runtime. It's a really stupid design flaw that, in my opinion, doesn't buy you anything, but creates lots of problems (including performance ones – JITs much prefer when you properly instantiate classes rather than pass records that quack the same).

Just consider what your signature says when you instantiate it at T = Array<string>, for example. The signature tells us you'll get an Array<Array<string>> as a result.

How do you make the implementation do that while still giving a proper Array<string> when taking T = string?

Here's Typescript, it allows for defining a type for those lists, so it's even typesafe (to the extend Typescript can be typesafe, but that's another matter)

Which is to say – not type safe at all. Notably, see https://counterexamples.org/polymorphic-union-refinement.html

Thanks for the shout out, u/DependentlyHyped!