> if an expression evaluates without error, then its type is… What’s curious is that this is true in every language with general recursion/looping: int f(

> if an expression evaluates without error, then its type is… What’s curious is that this is true in every language with general recursion/looping: int f(int n) { while (true) {} return n + 1; } (In other words, the type of “f” isn’t the logical formula “a → a”, but rather “a → ¬¬a”.) The type of “eval” can also be fully static; it can just return a type that you have to do case analysis or runtime type inspection on to use. In Haskell, with a data type: data Value = Integer Int | Text String | ... eval :: String -> Value foo = do value <- read_from_the_network let result = eval value case result of Integer n -> return (1 + n) _ -> error "that was not an integer!" Or with RTTI: eval :: String -> Dynamic foo = do value <- read_from_the_network let result = eval value case fromDynamic result of Just n -> return (1 + n) Nothing -> error "that was not an integer!" “fromDynamic” has the type: Typeable a => Dynamic -> Maybe a Which is to say “given a dynamic value, and its runtime type information, I can either give you the value back with a static type, or nothing if I can’t perform the downcast”—much like “dynamic_cast” on pointer types in C++.