refinement types
zpdDG4gta8XKpMCd opened this issue · 12 comments
This is a further development of the idea of tag types.
There are situations where being able to encode a certain predicate about a given value using its type is tremendously helpful.
Let's imagine that we have a number. In order to proceed with it we need to assert that it is greater than 0. This assertion doesn't come for free, because it takes some processor time to get evaluated. Since numbers are immutable this assertion only needs to be evaluated once and will hold true from then on without having to be reevaluated. But due to having no way to attach this knowledge to the number value we:
- either need to play safe and reevaluate it every time immediately before using
- or take our chances trying to trace it through the code from the place where it was asserted keeping the result of the assertion in mind and hoping not to break things during the next refactoring
Being able to attach additional knowledge to the type of a value in form of predicate that is guaranteed to hold true as long as the value doesn't change is what is called refinement types.
@ahejlsberg, what are the chances of seeing the refinement types in TypeScript one day?
References:
- Refinement types: https://en.wikipedia.org/wiki/Refinement_(computing)
- Pre/post conditions, Hoare logic: https://en.wikipedia.org/wiki/Hoare_logic
- Design by contract: https://en.wikipedia.org/wiki/Design_by_contract
In Rust this (or a similar?) idea was called typestate. This blog post discusses how you can sometimes model this using phantom types: http://pcwalton.github.io/blog/2012/12/26/typestate-is-dead/
looks like it, my respects to the design team of rust
There seems to be a paper that describes an implementation of refinement types: https://scirate.com/arxiv/1604.02480
This seems to be the implementation: https://github.com/UCSD-PL/refscript
Not sure if this helps but I think this might be related to Phantom Types as described here: https://medium.com/@gcanti/phantom-types-with-flow-828aff73232b
Flow does have native support for phantom types in the form of Opaque Type Aliases:
Could this be a viable approach for TypeScript as well?
Guaranteeing non-0 input was one thing I found Idris language was doing to implement type-safe division, see here.
So rather than requiring the user to tag other types w.r.t. whether they might be zero, it infers it from the type. (As in TypeScript, type literals are a thing there.)
Within TypeScript, I've been experimenting to achieve something similar. I've been trying to implement this safe division as a PoC by using overloads to conditionally produce an error in type calls (#17961).
I've managed to get it to error on bad input (0), though I'm still working out a few quirks as discussed there.
Now obviously, this is approaching it from the other end -- putting the checks where the info is requested, rather than manually tagging a type from where it is supplied. For things like numbers the former approach feels sensible to me as the types could already bear the info available, though I'll admit marking the types instead does feel more sensible for cases like Rust's open file check.
Will Phantom Types be implemented?
I use refined types in Scala and it is a godsend. I'm hoping this gets more attention.
BTW, a refinement condition where x % 1 === 0 is necessary for all web APIs that accept unsigned long long and all JS APIs that perform ToInteger (including implicitly via ToLength). And for web APIs that use unsigned long/unsigned int/unsigned short/unsigned byte as well as JS APIs that do ToUint32/ToInt32/ToUint16/etc., those all require the additional constraint of 0 <= x && x < 2**32 and similar.
So for the web at least, refining numbers is absolutely critical to typing several APIs correctly.
@AnyhowStep Refinement types are a strict superset of the subset I was referring to. 😉