Repository navigation
refinement types #7599
Description
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.
Anders Hejlsberg (@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
Activity
evmar commentedon Mar 21, 2016
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/
zpdDG4gta8XKpMCd commentedon Mar 21, 2016
looks like it, my respects to the design team of rust
bennoleslie commentedon Apr 12, 2016
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
ccorcos commentedon Aug 10, 2017
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
denisw commentedon Aug 25, 2017
Flow does have native support for phantom types in the form of Opaque Type Aliases:
https://medium.com/flow-type/hiding-implementation-details-with-flows-new-opaque-type-aliases-feature-40e188c2a3f9
Could this be a viable approach for TypeScript as well?
KiaraGrouwstra commentedon Sep 16, 2017
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.
Zzzen commentedon Nov 23, 2017
Will Phantom Types be implemented?
zalbia commentedon Aug 22, 2018
I use refined types in Scala and it is a godsend. I'm hoping this gets more attention.
dead-claudia commentedon Dec 29, 2019
BTW, a refinement condition where
x % 1 === 0is necessary for all web APIs that acceptunsigned long longand all JS APIs that performToInteger(including implicitly viaToLength). And for web APIs that useunsigned long/unsigned int/unsigned short/unsigned byteas well as JS APIs that doToUint32/ToInt32/ToUint16/etc., those all require the additional constraint of0 <= x && x < 2**32and similar.So for the web at least, refining numbers is absolutely critical to typing several APIs correctly.
AnyhowStep commentedon Dec 30, 2019
Couldn't the range as number type proposal also solve that problem?
#15480
There has been a proposal to have a min, max, and step for the range.
There's also a proposal for a type to just describe an integer type backed by a double type.
#28682
#30543
dead-claudia commentedon Jan 3, 2020
AnyhowStep Refinement types are a strict superset of the subset I was referring to. 😉
nikeee commentedon Jul 29, 2021
There are also IntervalTypes which address a similar issue: #43505