3 ms·

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 wa

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 sound type system. Assume a "fromVariant" function that unpacks the variant, it has a type: forall a. Variant -> Maybe a. Maybe is either Nothing or Just a, depending on whether the variant does indeed contain what you expect it to contain. > if you have a reference to an array of integers in the typed part of the code you need to protect against untyped parts of the code inserting non-integers inside the array. This "protection" is exactly what static type systems do. "Untyped code" in the context of using a static type system, is code that works with variants. So we need to pack the array of integers into a variant, where they will be suitably tagged by the runtime. The "untyped code" is free to write whatever it wants into a variant, so we must unpack it with runtime checks. The static type system forces us to unpack and assert its contents, before we can assign a specific type to it. > The only solution is to insert typechecks in the reads and/or writes to the array I am not sure what you mean here. When the array is packed into a variant then it can indeed be modified into anything by "untyped" code. But it should always be tagged correctly, which is the responsibility of the runtime. It will need to be re-asserted when unpacked into a specific type. > A similar problem happens with functions Functions should be values like any other, so my points apply to them too. The point I have been trying to make, is that a conventional static type system will already allow for "gradual typing". I cannot see a need to use an unsound type system in order to achieve this goal.

ufo 9y ago
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, etc). And perhaps also for objects, if your language has something analogoud to an instanceof operator. But for the higher order stuff like functions and mutable references you cannot write such a fromVariant function so easily! 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). There is no way that fromVariant can also check the function signature, to guarantee that the dynamically typed implementation will always return an integer when given an integer. 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. But these wrappers can slow down the program a lot and they also mess up with pointer equality... > the arrays The basic problem with the arrays is similar to the one with function. The statically typed code can't blindly trust that the array will always contain the type it expect because at any moment the untyped portion of the code could try to insert junk values into the array. 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). Things also get extra tricky if the array contains non primitive values (functions, other arrays, etc) --- 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 :)
- willtim 9y ago
  > 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. 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.
  - ufo 9y ago
    > I do concede that there is probably a definition of the term "gradual typing" out there that I am not strictly adhering to. The basic goal of gradual typing is that you can have your program be fully untyped or fully typed or somewhere in between and it will behave in a sensibly in all cases. Adding types to a program does not change the result of the program, except that sometimes adding types may cause new type errors to show up. > the best we can do is tag it as a function, with type Variant -> Variant This is very limiting. 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. Similarly, you cannot use statically typed objects inside the dynamically typed code because all objects that can be touched by the dynamically typed part of the code must have all their fields typed with the Variant type. > Although the danger of this is that you have a bomb waiting to go off inside some unsuspecting piece of typed code Technically the bomb is inside the dynamically typed part of the code :) One of the nice things you can get with a well though out gradual typing system is a guarantee that the line number in any of the type error messages will point to the dynamically typed part of the code. We call this blame tracking. > It sounds like you are concerned with performance and efficiency, that may indeed be an issue, but it's orthogonal to the type system Yeah, but one of the big challenges with gradual typing today is that i we try to be flexible (letting programmers add types wherever they want) and sound (with a soud type system, blame tracking, etc) all the implementations so far have had very bad performance, often running much much slower than the untyped version of the code would (with factors like 5x or 10x slower being common). When the performance gets this bad it effectively means that your only options are to have fully typed code or fully untyped code, because almost anything in between will run up super slow. Which kind of ruins the whole point of being able to gradually add types to your program. > Thanks for the offer, I am definitely interested. You can get very far by searching google scholar for "gradual typing. One good place to start out would be Siek and Taha's original paper on gradual typing for functional languages[1] and Sam Tobin-Hochstadt's PHD thesis on Typed Racket[2] (which used to be called Typed Scheme back then). For an example of the challenges of gradual typing in practice, this recent paper [3] might be interesting. [1] https://cs.colorado.edu/~siek/pubs/pubs/2006/siek06:_gradual.pdf https://cs.colorado.edu/~siek/pubs/pubs/2006/siek06:_gradual... [2] http://www.ccis.northeastern.edu/racket/pubs/dissertation-tobin-hochstadt.pdf http://www.ccis.northeastern.edu/racket/pubs/dissertation-to... [3] http://www.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf http://www.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf

ufo 9y ago

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, etc). And perhaps also for objects, if your language has something analogoud to an instanceof operator. But for the higher order stuff like functions and mutable references you cannot write such a fromVariant function so easily! 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). There is no way that fromVariant can also check the function signature, to guarantee that the dynamically typed implementation will always return an integer when given an integer. 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. But these wrappers can slow down the program a lot and they also mess up with pointer equality... > the arrays The basic problem with the arrays is similar to the one with function. The statically typed code can't blindly trust that the array will always contain the type it expect because at any moment the untyped portion of the code could try to insert junk values into the array. 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). Things also get extra tricky if the array contains non primitive values (functions, other arrays, etc) --- 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 :)

willtim 9y ago
> 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. 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.
- ufo 9y ago
  > I do concede that there is probably a definition of the term "gradual typing" out there that I am not strictly adhering to. The basic goal of gradual typing is that you can have your program be fully untyped or fully typed or somewhere in between and it will behave in a sensibly in all cases. Adding types to a program does not change the result of the program, except that sometimes adding types may cause new type errors to show up. > the best we can do is tag it as a function, with type Variant -> Variant This is very limiting. 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. Similarly, you cannot use statically typed objects inside the dynamically typed code because all objects that can be touched by the dynamically typed part of the code must have all their fields typed with the Variant type. > Although the danger of this is that you have a bomb waiting to go off inside some unsuspecting piece of typed code Technically the bomb is inside the dynamically typed part of the code :) One of the nice things you can get with a well though out gradual typing system is a guarantee that the line number in any of the type error messages will point to the dynamically typed part of the code. We call this blame tracking. > It sounds like you are concerned with performance and efficiency, that may indeed be an issue, but it's orthogonal to the type system Yeah, but one of the big challenges with gradual typing today is that i we try to be flexible (letting programmers add types wherever they want) and sound (with a soud type system, blame tracking, etc) all the implementations so far have had very bad performance, often running much much slower than the untyped version of the code would (with factors like 5x or 10x slower being common). When the performance gets this bad it effectively means that your only options are to have fully typed code or fully untyped code, because almost anything in between will run up super slow. Which kind of ruins the whole point of being able to gradually add types to your program. > Thanks for the offer, I am definitely interested. You can get very far by searching google scholar for "gradual typing. One good place to start out would be Siek and Taha's original paper on gradual typing for functional languages[1] and Sam Tobin-Hochstadt's PHD thesis on Typed Racket[2] (which used to be called Typed Scheme back then). For an example of the challenges of gradual typing in practice, this recent paper [3] might be interesting. [1] https://cs.colorado.edu/~siek/pubs/pubs/2006/siek06:_gradual.pdf https://cs.colorado.edu/~siek/pubs/pubs/2006/siek06:_gradual... [2] http://www.ccis.northeastern.edu/racket/pubs/dissertation-tobin-hochstadt.pdf http://www.ccis.northeastern.edu/racket/pubs/dissertation-to... [3] http://www.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf http://www.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf