3

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.

  • 1
    would be nice if you share your reasoning, namely what looks paradoxical to you – gnat Aug 1 '14 at 15:15
  • 2
    It's simple. Write a JavaScript interpreter in your Turing-complete language, and you can do anything that JavaScript can do. – Kilian Foth Aug 1 '14 at 15:16
  • 1
    What does that return in JavaScript? You can get the exact same effect in, say, C# by returning something of the root type object. You have no type safety, but it is equivalently powerful to your JS snippet, which has no type safety either. – Phoshi Aug 1 '14 at 15:23
  • @Phoshi: It can return anything. Any arbitrary JavaScript expression. – davidk01 Aug 1 '14 at 22:51
  • @davidk01: Right. Whereas unityped Javascript has /only/ the root return type, strongly typed languages can often still use a root type. object in C#, as per my example, could return the value of any arbitrary C# expression. – Phoshi Aug 3 '14 at 20:02
9

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.

  • Note that the restriction to prove that the caller will provide a string that will evaluate to a function of type string -> string does not exist in the JavaScript version. The return type can be any arbitrary object. – davidk01 Aug 1 '14 at 22:53
  • Really good answer by the way. – davidk01 Aug 1 '14 at 22:55
  • @davidk01 That's true, you could also do something like exists T. typeOf s = String -> T – jozefg Aug 2 '14 at 17:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.