|
|
|
|
|
by willtim
3265 days ago
|
|
Thanks for the references. It looks like "gradual typing" is about trying to retrofit types to dynamic languages. That is certainly harder than
starting with a statically-typed system and adding dynamic types (my preference). The latter clearly works, as evidenced by e.g. C# and Dart 2. > With this restriction, you cannot assign an accurate static type to a function with a dynamically typed implementation, which means that you can't use dynamically typed libraries from inside statically typed code. It depends what you mean by an accurate type. A accurate type for adapting your example would be to expose Variant -> Variant as Int -> Maybe Int, thus capturing the partiality. I concede that Int -> Maybe Int cannot be used in a function that expects Int -> Int, but that is how it should be! An untyped language cannot provide me with a function of Int -> Int. |
|
> It depends what you mean by an accurate type.
The gradual typing literature tends to prefer having partial functions (that might raise well-behaved type errors at runtime) because it eases the transition between typed and untyped programs. You can add or remove type annotations without having to simultaneously add and remove tons of explicit pattern matches against Maybe. But this isn't the part I was talking about.
The key issue is that when you cast a function from (Variant->Variant) to (Int->Maybe Int) you need to add a small wrapper around the dynamic function that converts the input from Int to Variant and converts the output from Variant to Maybe Int. In theory it is simple but in practice all those wrappers can add up really quickly...
Functions are the simplest case where these higher-order type-conversion issues pop up but in my experience things are actually the most thorny when it comes to mutable objects and arrays. The extra type checks and conversions around every property read and write can add a ton of overhead. And from a semantics point of view you need to be careful because if your implementation is based around wrappers it could end up messing with object identity (like Javascript's === operator or Python's "is")