Type syntax not stable under bracketing?

[martinberger]

Not sure this is a bug or feature, but (in Sail 0.17 (sail @ opam-v2.3.0) ) we can do

val f : unit -> unit

But not

val f : (unit -> unit) // ERROR 

I imagine that this comes from function types for functions being enforced during parsing, not type-checking. But it surprised me: in most programming languages one can always bracket expressions, whether types or program expressions.

Could you clarify?

[Alasdair]

Yes, because Sail is first-order function types are only allowed in specific places in the grammar - therefore a function type is not currently an expression you can use anywhere a type is expected, for example

vector('n, int -> int)

val f : int -> int -> int

are both parse errors.

It is sometimes a good idea to refactor the parser to be more permissive, and then reject the bad cases later with a more bespoke and descriptive error message.

If we did want to refactor like that I think the real motivation would be function type synonyms which aren't currently possible due to the syntactic restrictions on function types.

[martinberger]

Yes, I also noticed that function type synonyms are not possible, and was about to raise an issue here.

[Alasdair]

There are some more fundamental issues we'd have to solve to make it work. The first-orderness assumption is pretty baked-in to the design of the type system and grammar all the way back to the first few commits in this repository.

[martinberger]

Can the first order assumption not simply be enforced by the type checker? It's a natural division of labour and clean modularisation: parser checks syntactic correctness, the subsequent type checker, assuming grammatical correctness, checks type-and kind correctness? (I am probably overlooking some subtlety!)

[Alasdair]

It's a trade off. Right now the fact that function types are not nested within other types is guaranteed by the structure of the AST. That means it's impossible to even represent a non first order program. Sail backends downstream of the type checker don't even have to consider the possibility that they'll see an unexpected function type anwhere, they can just follow the structure of the AST and rely on OCaml's pattern completeness checker to cover all cases.

For properties of the AST that are just enforced by type-checking rules (or AST->AST rewrites), that's something you have to hold in your head while writing Sail backends, so there's more cognitive load on the developer to remember all the invariants.

So the trade off is a more flexible AST usually gets you better error messages and reduces syntactic ambiguity, but a more restrictive AST means you can leverage the type-system of the implementation language to enforce invariants. This is why in Sail we have two ASTs, the Parse_ast type that represents the AST just after parsing, then the Ast type that is a bit simpler and has a lot of syntactic sugar removed.