How would you statically type the following JavaScript program
function c(str) {
c = eval(str);
return c(str);
}
I’m not trying to start a flame war but I’m genuinely curious. I’ve always assumed that dynamic languages allow more programs to be written because of examples like the above. But if a statically typed language is Turing complete then it should be able to express the equivalent of the above program. So where exactly does my reasoning break down because this seems paradoxical to me? My reasoning is that this is obviously a function that can not be typed in a statically typed language and still allow the generality that the above code allows for.
7
There are a few ways you could go about typing this.
Forget All The Types!
You can mimic dynamic types in statically typed languages by simply forgetting that you had types in the first place and switching to using runtime type information.
In haskell this would look something like
evalThingy s = let result = eval s
resultTy = typeOf result
if resultTy == typeOf (id :: String -> String)
then unsafeCoerce result s
else fail in some manner
So we have a runtime switch which just checks whether it’s safe to continue and if it is, beat the typechecker into submission and proceed.
Personally I dislike this way since if I’m going to have to write something in a static type system, I want to get the safety benefits. That means coercions like the above are a no-no.
Explicit Failure
The simplest is to force eval to either return a specific type or fail in a controlled manner
eval : String -> Either Error a
And then we could say something like
c = eval(str) : Either Error (str -> Int)
case c of
Right f -> f str
Left err -> blowup str
In order to support this well are language needs something called return type [parametric] polymorphism. ATM I’m only aware of this being supported through type classes. That means that we need to different things depending on what the type called is.
Dependent Types
The more convoluted approach would be to actually reflect the typing judgement of the language into some function, let’s say typeOf.
typeOf : String -> TypeOfTypes
Where TypeOfTypes is the universe of all types that programs normally use. This can’t include itself if we want some sanity in our type system.
Next we can assign eval a fairly convoluted dependent type to eval
eval : (s : str) -> typeOf str
applySelf : (s : String) -> typeOf s = (String -> String) -> String
applySelf = function(s, p){
case p of
reflexivity -> eval(s)(s)
}
So we force the caller of applySelf to prove that the string they’re asking us to evaluate will have the type string -> string at which point we can ignore the safety checks since we have a static proof of correctness.
3