March Type System Changes

[alexgrejuc]

This post contains information about some forthcoming changes to bogl. After a few people have tried them out, I would feel comfortable merging it into master, at which point it will go live for all of the student programmers.

I initially intended to release them as part of a rewrite of the type system, but as Jennifer noted, many of the fixes would be useful to have now.

Ben has set up a development server. You can access it here to try out all of these changes.

I am hoping that some people can do a quick test run to make sure that nothing has gone horribly wrong, since these fixes required some significant changes to the bogl implementation.

My hope is that people poke around and try to break/stress test these changes. Note that I am not asking you to type in the examples below verbatim; the point is that we get a variety of programs running on these new changes.

Also note that Ben and I do keep a test suite; I've written tests for these fixes and they of course pass.

If you encounter an issue, make sure to try it both on the main bogl site as well as on the development one so that we can know whether one of the current changes introduced it or whether it existed before that.

You can email Ben and me and we will take it from there.

Proper support for type names

Type errors will now be reported nominally rather than structurally. That is, they will use type names instead of type expressions.

Before

After

Report first type error first

In the past, the last type error was reported. This led to very unhelpful you did not define x errors.

Before

After

Assign symbols to a type

In the past, the type checker assigned symbols to a singleton type, regardless of the type definitions. For example, X to {X} and O to {O}.

Before

After

Disallow symbols that have not been declared

In the past, arbitrary symbolic values could be used, even if they were never declared.

Before

After

Enforce parameter cardinality

In the past, function equations and signatures with mismatched parameter cardinality were not rejected.

Before

After

Reject spurious subsumption

In the past, symbols were incorrectly considered subtypes in certain edge cases of if expressions and binary operations.

Before

After

Not fixed: well-formedness criteria for symbols in type definitions

Certain type definitions are not rejected as they should be. For example, symbol literals can still be declared in multiple types. This is not correct, but is a known issue that will be fixed in the future.

Fortunately, the type system does still prevent unsafe expressions formed from these types from being executed.

[montymxb]

@alexgrejuc I found an interesting type error in an existing program "Space Invaders" that we wrote some time ago. (See the example in the comment below). This works on the normal server. In addition, the message is a bit dense as well, but we can consider that at some other time if we want.

[montymxb]

I have condensed the type issue from above into a clean unit. This works on the live version as expected.

type T0 = (Int,Int)
type T1 = (Int,T0)

f : T1 -> T1
f(a,b) = if True then (a,b) else (a,b)

Type error in "Program" (line 7, column 37) Could not match types T0 and T0 in expression: if True then (a, b) else (a, b)

This doesn't occur if you don't nest the tuple inside of an if-then-else expression. I checked while loops, let exprs, and played around a bit with other things, but it seems it's just this case.

[alexgrejuc]

Thank you for finding the issue and finding a minimal example of it! Also,

doesn't occur if you don't nest the tuple inside of an if-then-else expression

is a quite helpful. I just patched an issue up related to if expressions right before making this post, and evidently I didn't quite do it right.

I won't be able to work on it until the 25th, but the details you've provided are very helpful.

The issue is very likely in this function

[alexgrejuc]

Closed since the issue @montymxb spotted has been fixed and these changes have been merged.