sdthompson1 / babylon

An experimental new programming language with verification features.
https://www.solarflare.org.uk/babylon
Other
0 stars 0 forks source link

Abstract types in interfaces #4

Open sdthompson1 opened 1 month ago

sdthompson1 commented 1 month ago

It should be possible to write type Foo; in the interface, but have type Foo = something or datatype Foo = something in the implementation.

For now the codegen for this will work by "looking inside" the imported module to see what the implementation of the type is, and then just using that as normal. This means we won't be able to do separate compilation, unfortunately, but compilation times are fairly fast, so this is not a big issue (and we can always add separate compilation back in later).

The renamer might have to be modified to ensure that e.g. constructor names are hidden outside of the module. The typechecker will have to hide the actual implementation of the type from other modules (merely exporting it as an "abstract type" as if type Foo; had been used all along). The verifier is similar - we just have to make sure that in external modules, the type is considered to be type Foo; rather than its real definition.

This shouldn't therefore be all that hard to do.

If the type contains allocated-predicates (#3) then the allocated-predicate given in the interface must be implied by the one given in the implementation. I.e. the interface might lie and say the type is allocated, when it isn't really; but it can't lie the other way around and say that the type isn't allocated when it is.

sdthompson1 commented 2 days ago

At the same time I'm going to change the syntax for "external" types (corresponding to void* in C) from type Foo; to extern type Foo;. This will avoid confusion between two different uses of type Foo;.

So to summarise, the type keyword will now be usable as follows: