SSA + Type Inference = "Compile time" dynamic typing, "runtime" static typing?

If we SSA transform our program and _then_ perform type inference (glossing over issues like if we get always infer somethings type), do we get strong static dynamic typing?

e.g.:

a = 1
b = a + 1
a = "hello"
printLine a
.
.
.
a0 = 1
b0 = a0 + 1
a1 = "hello"
printLine a1

Of course there are scenarios like:

if condition then a = 1 else a = "Hello"
end if

But I believe that these scenarios can be overcome. My question is then, is this impossible for any reason?

Thoughts

But I believe that these scenarios can be overcome.

What do you have in mind? Converting to SSA form would only rename away inessential local dynamicity, which is trivial anyway. Obviously you can have the phi-functions in your SSA code map to type-level joins (least upper bounds in the type lattice), i.e. you let x = phi(y, ..., z) generate the constraints type(x) <: type(y), ..., type(x) <: type(z) and then you probably have a separate stage that solves all the constraints by dataflow iteration. In general the bounds generated this way will be too loose, effectively diverging to the top case. This then motivates making the type bounds in the constraints conditional. For instance, in your case you would have constraints saying "type(a) <: int if condition" and "type(a) <: string if not condition", which puts you on the path to dependent typing. And the most general form of dependent typing as seen in e.g. Ontic does not have decidable checking, let alone decidable inferencing. So either you let your type bounds become so inclusive as to be useless or you introduce non-decidability. The non-decidability need not become an insurmountable issue in practice if you program in a principled way (i.e. you have the specific type system in mind) but it _will_ be an issue if you throw a program at it which is highly dynamic at the type level.

(I'm not an expert so I'm waiting for the gurus to point out my horrible mistakes in the above!)

By Per Vognsen at Sat, 2006-09-23 17:09 | login or register to post comments

SSI might be appropriate -

SSI might be appropriate - AIUI it makes parts as well as joins explicit. GRIN does something similar for optimising lazy functional code, though by that point it's typeless - it's the possible range of tags on a value that it's looking at.

By Philippa Cowderoy at Sun, 2006-09-24 12:11 | login or register to post comments

Squaring the circle

But I believe that these scenarios can be overcome.

The desire to solve unsolvable problems seems to be a constant of human history. Our anchestors spent their lives trying to prove the parallel axiom of euclidean geometry or squaring the circle. More recent efforts were spent in a final theory of the universe. The latest generation appears to seek for whole program inference and static analysis of languages like Ruby. Of course I'm joking when I give you some kind of Zen advice: only when you leave everything as it is you will make progress and achieve your goal. This is by no means intended to convince you giving up everything.

By Kay Schluehr at Sat, 2006-09-23 18:40 | login or register to post comments

Unsolvable?

if condition then a = 1
else a = "Hello"
end if

I'm confused, what is unsolvable? Isn't the type of a simply the union of integers and strings?

By cdiggins at Sat, 2006-09-23 18:48 | login or register to post comments

Context

Right. Now consider this in the context of a whole program. If you write code that is "dynamically typed in essence" then you are likely going to see a combinatorial explosion in the size of the type unions.

Perhaps a more essential objection: you generally need this kind of analysis to be whole-program unless you can confine the dynamicity very carefully. But once your type inference is whole-program you by definition don't have any static checking of types, do you? The type reconstructor will just widen the union types to accomodate any and all terms you throw at it.

By Per Vognsen at Sat, 2006-09-23 19:26 | login or register to post comments

objections...

Right. Now consider this in the context of a whole program. If you write code that is "dynamically typed in essence" then you are likely going to see a combinatorial explosion in the size of the type unions.

while, in theory, this might be an issue, concrete applications should not suffer from this problem.

dynamic typing basically imposes the tracking of variable types onto the programmer, as it is still necessary to be able to reason about the content of a variable at a point in the program in some way. therefor manual type coercion is applied anyways in practise (usually via the help of runtime reflection mechanisms).

any application of discriminated union types in existing languages with type inference is basically the same, with the difference that unions are explicit there.

on the other hand, certain techniques like open classes may be more problematic.

But once your type inference is whole-program you by definition don't have any static checking of types, do you? The type reconstructor will just widen the union types to accomodate any and all terms you throw at it.

no. as with any type system, as soon as no typing rule can be satisfied a type error has to be produced.

take the following hypothetical example:

if condition then a = 1 else a = "Hello" end if a == true -- type error, neither Int nor String allow a comparison to Bool

By peter steiner at Mon, 2006-09-25 16:45 | login or register to post comments

How far can you get without naming types?

A simple example: An Erlang function that returns a two element tuple in some cases and a three element tuple in others. In Haskell, this would be a no-no. You'd have to name the return type, then name each variant.

By James Hague at Sat, 2006-09-23 19:02 | login or register to post comments

Two/three tuple in Haskell?

See section 4 of Functional Pearl: Implicit Configurations.


{-# OPTIONS -fglasgow-exts #-} 

main = print $ two_three_tuple 3 sum_up

two_three_tuple :: Integer -> (forall s. Sum s => s -> c) -> c
two_three_tuple x k = if even x then k (x,x) else k (x,x,x)

class Sum a where 
    sum_up :: a -> Integer
instance Sum (Integer,Integer) where 
    sum_up (x,y) = x+y
instance Sum (Integer,Integer,Integer) where 
    sum_up (x,y,z) = x+y+z

By Greg Buchholz at Sun, 2006-09-24 00:10 | login or register to post comments

strong static dynamic typing?

What is "strong static dynamic typing" supposed to mean? Among other things, strong typing has absolutely nothing to do with the other two, which possibly makes what you're trying to get across even more confusing.

If you're proposing a solution for type inferring dynamic languages, it seems like what you've shown has little to do with it at all. Type inference with most dynamically typed languages isn't conceptually that hard, but it does require certain trade-offs which most people don't realize, e.g. you're going to get very generic results for certain situations. Whether or not this is a bad thing is debatable, but even still it's is far from impossible, as a previous poster implied.

By Curtis W at Sat, 2006-09-23 21:08 | login or register to post comments

ocaml

can some one write this in ocaml and or objective-c using protocol?

By maxime caron at Mon, 2006-09-25 02:14 | login or register to post comments

Lambda the Ultimate

User login

Navigation