3 ms·

Actually, you can call both ways - from statically typed to dynamically typed and back. This is the premise of the work done in Racket on contracts, and more ge

by rntz 12y ago

Actually, you can call both ways - from statically typed to dynamically typed and back. This is the premise of the work done in Racket on contracts, and more generally of the "gradual typing" movement. Harper's "unityped" term suggests exactly how this can work. An untyped function takes arguments that are all of one type, and returns one of the same type (that type being the "dynamic" type that includes every possible value, and thus is useless for static checking). To call an untyped function from typed code, simply cast all your arguments to this type (trivial, since it contains anything), and check its return value has the type you expect (throwing an error if it's of the wrong type). To call a statically typed function from untyped code, simply check the types of all the arguments you wish to pass to it (throwing an error if they don't match its signature), and cast the returned value to the dynamic type (again, trivial). I'm glossing over a very important difficulty, which is that you can't dynamically check something of a function type -- if I'm handed a function, how do I know at runtime whether it's of type `int -> int`? I can't! So the solution is to "wrap" this function with a contract that delays checking until the function is actually called, at which point you can check the argument is an `int` and the result is an `int`.

tel 12y ago
Total agreement generally, but I wanted to mention that the Any -> X downcasting is trouble sometimes. It is difficult to do this in a type-safe way (e.g. without accidentally introducing holes) and if you have typecasing universally then you lose parametricity, one of the most powerful tools in any polymorphic type theory.
JadeNB 12y ago
> To call an untyped function from typed code, simply cast all your arguments to this type (trivial, since it contains anything), and check its return value has the type you expect (throwing an error if it's of the wrong type). To me, as soon as a function includes dynamic checks, it ceases to be statically typed; so I would say that a function that operates this way becomes only dynamically typed.
- rntz 12y ago
  Do you consider any function which may raise an error to be "dynamically typed", then? (For example, any function which performs an array index; or any function which performs I/O; or, to be absurd, any function which allocates memory (since memory is a finite resource that may run out).) If so, I understand the distinction you're making, but it's a very strong position; most people do not mean that when they say "statically typed". If not, I don't understand the distinction you're making. Admittedly, gradual typing does not mean that calling into untyped code from typed code is "safe" from runtime type errors (although it is safe in the technical preservation-and-progress sense). But it gives you a partial guarantee: if a type error occurs, you know that the fault does not lie in the typed code. This aids debugging, and helps you port over existing codebases gradually. So it's still quite useful.
  - JadeNB 12y ago
    > Do you consider any function which may raise an error to be "dynamically typed", then? (For example, any function which performs an array index; or any function which performs I/O; or, to be absurd, any function which allocates memory (since memory is a finite resource that may run out).) That's a good question! Yes, in an idealised sense, I do; but, in practice, I think that I would make an exception for functions where the error comes from the host system, not from the program. (For example, if I were too strict about it, then I would have to disallow even the safest of Haskell functions because it might be executed on a computer whose hard drive is failing.) Thus, I would call Haskell's `head` function dynamically typed. > Admittedly, gradual typing does not mean that calling into untyped code from typed code is "safe" from runtime type errors (although it is safe in the technical preservation-and-progress sense). I think that I don't understand the definition. Isn't encountering a runtime error precisely getting 'stuck' (in the "opposite-of-progress" sense)?
    - rntz 12y ago
      > I think that I don't understand the definition. Isn't encountering a runtime error precisely getting 'stuck' (in the "opposite-of-progress" sense)? Sorry, perhaps I should have said "exception" rather than "error". Raising an exception is absolutely "safe"/progress-obeying, as long as your language specifies the behavior of exceptions. That the exception happens to be called a "TypeError" doesn't change anything. Getting "stuck" means being in a state such that there's no defined next state - a state which the language spec doesn't cover. So most "dynamically-typed" languages are in fact safe in progress-and-preservation terms, because they have well-defined behavior in all cases. C, otoh, is "statically-typed" but unsafe, because you can write C code with undefined behavior. (That dynamically typed languages can be (statically) typesafe should be unsurprising, since they're just statically-unityped languages. Nothing says a unityped language can't be typesafe, it's just a very uninteresting property!)
rpglover64 12y ago
(Late to the party; sorry) > you can't dynamically check something of a function type Another approach, besides contracts, (one that my lab is working on) relies on whole program type-checking and path-sensitive program analysis.

by rntz 12y ago

tel 12y ago

Total agreement generally, but I wanted to mention that the Any -> X downcasting is trouble sometimes. It is difficult to do this in a type-safe way (e.g. without accidentally introducing holes) and if you have typecasing universally then you lose parametricity, one of the most powerful tools in any polymorphic type theory.

JadeNB 12y ago

> To call an untyped function from typed code, simply cast all your arguments to this type (trivial, since it contains anything), and check its return value has the type you expect (throwing an error if it's of the wrong type). To me, as soon as a function includes dynamic checks, it ceases to be statically typed; so I would say that a function that operates this way becomes only dynamically typed.

rntz 12y ago
Do you consider any function which may raise an error to be "dynamically typed", then? (For example, any function which performs an array index; or any function which performs I/O; or, to be absurd, any function which allocates memory (since memory is a finite resource that may run out).) If so, I understand the distinction you're making, but it's a very strong position; most people do not mean that when they say "statically typed". If not, I don't understand the distinction you're making. Admittedly, gradual typing does not mean that calling into untyped code from typed code is "safe" from runtime type errors (although it is safe in the technical preservation-and-progress sense). But it gives you a partial guarantee: if a type error occurs, you know that the fault does not lie in the typed code. This aids debugging, and helps you port over existing codebases gradually. So it's still quite useful.
- JadeNB 12y ago
  > Do you consider any function which may raise an error to be "dynamically typed", then? (For example, any function which performs an array index; or any function which performs I/O; or, to be absurd, any function which allocates memory (since memory is a finite resource that may run out).) That's a good question! Yes, in an idealised sense, I do; but, in practice, I think that I would make an exception for functions where the error comes from the host system, not from the program. (For example, if I were too strict about it, then I would have to disallow even the safest of Haskell functions because it might be executed on a computer whose hard drive is failing.) Thus, I would call Haskell's `head` function dynamically typed. > Admittedly, gradual typing does not mean that calling into untyped code from typed code is "safe" from runtime type errors (although it is safe in the technical preservation-and-progress sense). I think that I don't understand the definition. Isn't encountering a runtime error precisely getting 'stuck' (in the "opposite-of-progress" sense)?
  - rntz 12y ago
    > I think that I don't understand the definition. Isn't encountering a runtime error precisely getting 'stuck' (in the "opposite-of-progress" sense)? Sorry, perhaps I should have said "exception" rather than "error". Raising an exception is absolutely "safe"/progress-obeying, as long as your language specifies the behavior of exceptions. That the exception happens to be called a "TypeError" doesn't change anything. Getting "stuck" means being in a state such that there's no defined next state - a state which the language spec doesn't cover. So most "dynamically-typed" languages are in fact safe in progress-and-preservation terms, because they have well-defined behavior in all cases. C, otoh, is "statically-typed" but unsafe, because you can write C code with undefined behavior. (That dynamically typed languages can be (statically) typesafe should be unsurprising, since they're just statically-unityped languages. Nothing says a unityped language can't be typesafe, it's just a very uninteresting property!)

rpglover64 12y ago

(Late to the party; sorry) > you can't dynamically check something of a function type Another approach, besides contracts, (one that my lab is working on) relies on whole program type-checking and path-sensitive program analysis.