Earlier quoted context omitted.
I assume that my downvoters do not believe this can be done in a conventional static type system. So I will try to explain further. > The problem munificent was talking about is that for more complex types you cannot write that type checking predicate you want, which would check if a value belongs to the given type and return a variant-free version of the object. The complexity of the type should not matter to a soun…
Dart's choice of an unsound type system doesn't actually matter for those gradual typing problems we were talking about. I think you are getting too caught up in that point. Anyway, going back to the topic, I'll try to explain why your idea doesn't work. > assume a fromVariant function What I was trying to say on my other post is that you can only create such a function for primitive types (numbers, booleans, strings…
I was trying to show that "gradual typing" should be possible in any reasonable static type system, without resorting to unsoundness. I do concede that there is probably a definition of the term "gradual typing" out there that I am not strictly adhering to.
> Suppose I write down a dynamically typed implementation of the identity function and pass it to some typed code that expects an int->int function. When we pass the function to the typed side we will call fromVariant on it but the best we can do at first is check if the value we have is a function (and not an integer, etc).
If the best we can do is tag it as a function, then fromVariant would unpack it to a function with type Variant -> Variant, which represents all dynamically-typed functions. When we call this function, we indeed would need need to assert the outputs.
> One way to solve this problem is for fromVariant to return a wrapped version of the dynamic function that checks if the returned value is of the expected type
Agreed. Although the danger of this is that you have a bomb waiting to go off inside some unsuspecting piece of typed code. The alternative to to acknowledge that it is a partial function in the type, e.g. the Variant -> Variant function becomes Int -> Maybe Int, or similar. The point is that we are solving these problems using conventional static typing. You haven't yet convinced me that this doesn't work.
> You will either need to do a runtime check when the dynamic code writes to the array (which slows down the dynamic code) or you need to add runtime checks when the static code reads from the array (which makes it slower than it would be in a fully static language).
It sounds like you are concerned with performance and efficiency, that may indeed be an issue, but it's orthogonal to the type system. My own position is that if one wants performance, then don't write untyped code!
> If you are interested I can send you links to a couple of gradual typing papers. As munificent said, there is currently lots of ongoing research about this and we all wish it were as simple as you were suggesting it would be
Thanks for the offer, I am definitely interested. I suspect that the outstanding issues are around usability and efficiency. I stand by my original point that "gradual typing" should be possible in any sufficiently expressive static type system.