Repository navigation
refinement types #7599
Description
Activity
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/
Reacted by Ricardo Fernández Serratalooks like it, my respects to the design team of rust
Reacted by Salathiel GeneseReacted by ErikThere 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
Reacted by Wiktor Czajkowski, Ali and tintin10qNot 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
Reacted by Zzzen and Tsotne NazarashviliFlow does have native support for phantom types in the form of Opaque Type Aliases:
Could this be a viable approach for TypeScript as well?
Reacted by Joram van den BoezemGuaranteeing 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.
Reacted by Jason DreyzehnerWill Phantom Types be implemented?
I use refined types in Scala and it is a godsend. I'm hoping this gets more attention.
Reacted by Karol Majewski, Christopher Dignam, Daniel Nixon, LifeIsStrange, Ihor Mielientiev, Sean Matheson, Nathan Broadbent, Benjamin Rood, Arnau Sanchez Sala and AliBTW, 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 Refinement types are a strict superset of the subset I was referring to. 😉
There are also IntervalTypes which address a similar issue: #43505
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:
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: