As a newcomer to Fantom I'm trying to understand the details of the type system from the documentation. Specifically what happens when a type is substituted for another.

Doing some examples in fansh, a local variable static Num can be dynamic (typeof) Int or Float but not typeof Num even if statically declared as Num. However if statically declared as Num it can be dynamically reassigned either Int or Float both of which fit Num of course.

static Num [] can be assigned Int or Float each element as expected, and stays Num[]

static Num [] can be assigned a static Int[] value and then becomes dynamic typeof Int []. When static Num [] is typeof Int[] it can still be assigned static Float[] or static Num[]. In which case it switches back to dynamic typeof Float[] or typeof Num[] However individual element assignment to the list is allowed or not according to the List's dynamic type, not its static type.

So what is surprising here is that static Num [] variables do not stay Num [] when assigned Int [], and this is then seen as a possible runtime errors in setters.

You note in the documentation this issue with setters, that it is a hole in the static type system that this contravariancy of List setters is not captured. I'd want to be sure (which the documentation does not seem certain about) that Fantom runtime code is dynamically typesafe. It appears to be so under fansh?

The complete type semantics of Fantom seems to me to be understood only by tracking separately the static type and the dynamic type of every (object) value. And noting that static Num [] lists are objects that can have dynamic type that is either Int [], Float [] or Num []. Static typing can then be seen as an approximation to dynamic typing that will catch most but not all runtime type errors.

The documentation says that runtime type coercion is implicitly inserted where it would be needed in C, which is when the static type narrows the actual type (and therefore fits it). I suppose whenever the actual type fits the static type no runtime type coercion is ever done? That seems to be the case in the above examples.

I'd like to explain this properly in Hertz's textbook - but I'm not sure I fully understand it myself yet!

I think the simplest way to understand it might to be just compare the Fantom type system to Java (since in the end that is how it gets implemented).

1. Fantom subclassing maps directly to Java subclassing (mixins are interfaces)
2. Fantom List workt just like Java array of Objects

So understanding how a Fantom Num[] works is that basically that creates a Java backing store array of java.lang.Number. But the compile time type doesn't ever change with casting:

fansh> ints := [2, 3]
[2, 3]
fansh> nums := (Num[])ints
[2, 3]
fansh> nums.typeof
sys::Int[]
fansh> nums.add(4f)
sys::CastErr: Adding 'sys::Float' into 'sys::Int[]'
  fan.sys.List.insert (List.java:419)
  fan.sys.List.add (List.java:386)

Casting a list works just as it does in Java with arrays. In Java you would get something like ArrayStoreException.

I suppose whenever the actual type fits the static type no runtime type coercion is ever done? That seems to be the case in the above examples.

Yes you are right. If a Str is expected and we know we have a Str variable at compile time, then no cast is inserted.

Hopefully that helps explain it, if not let me know and I'm happy to explain it more detail or answer more specific questions.

Thanks for this, that does answer how the type system works.

Just one question.

Is there ever a case where a dynamic type error allowed by the static type checking (setting an Int [] with a float, say) is NOT caught as an error by the JVM?

Your current documentation sound as though you are not sure. But I'm hoping you are sure.

My take on this is that a static type system which has a few known but unusual leaks where it does not detect possible errors is OK - but only if I can be certain those type errors will be detected at runtime.

If such an error is not caught it is ugly because the effect will be very unexpected (1.0 turning into some large integer etc). In that case a compile-time warning whenever an Int [] is fitted to a non-const Num [] might be worthwhile.

Tom

If you are running Fantom on the JVM then anything not caught by the compiler at compile time will be caught at runtime by the JVM. In the end, everything is an actual Java type which gets handled in the bytecode signatures.

The only exceptions to this are the collection generic types List and Map which work sort of like Java using type erasure. In the JVM the bytecode for any list type will just be fan.sys.List and any map will be fan.sys.Map.

Since the List uses a backing store array of the proper type it catches type.

However, Map works just like a Java generics map - you can "cast away" the compile time checks and then won't get them at them runtime.

fansh> map := Str:Int["foo": 3]
[foo:3]
fansh> map2 := (Str:Str)((Obj)map)
[foo:3]
fansh> map2["bar"] = "baz"

In a perfect world you shouldn't be allowed to perform that last statement at runtime. But since the JVM doesn't really support reified generics, it would be expensive to implement that. We are just lucky because we get it for free with List by using an array of correct type.

In the above case accessing the "foo" value via map2 leads to a dynamic cast error: map2["foo"]+1

As you would hope. So I am still expecting that the JVM will always throw errors on dynamic type violations. That is not in general guaranteed because a value type might be stored in such a way that only a type contract determined its interpretation.

But it seems to me that your value types are all correctly typed in the JVM because your compiler generates JVM bytecode and therefore can't break JVM dynamic typing?

The case I'm wondering about is whether it is ever possible for a value type to be misinterpreted without a run-time error - but I don't think it is.

But it seems to me that your value types are all correctly typed in the JVM because your compiler generates JVM bytecode and therefore can't break JVM dynamic typing?

Collection types aside - anytime you use a method/field/class the JVM will do the proper checking. The JVM bytecode analyzer is very trust worthy since it was designed for sand boxed security.