Adjust syntax to cater to our target ML audience

vehicle-lang / vehicle

A toolkit for enforcing logical specifications on neural networks

https://vehicle-lang.readthedocs.io/

BSD 3-Clause "New" or "Revised" License

78 stars 6 forks source link

Adjust syntax to cater to our target ML audience #84

Open MatthewDaggitt opened 2 years ago

MatthewDaggitt commented 2 years ago

@yiergot makes the point that some of our syntax could be better targeted to machine learning users. Major points of friction are:

[x] Finite type - at the moment we follow Agda's convention of using Fin n for the type family of naturals strictly less than n. This short-hand isn't very meaningful to non ITP users. Perhaps we should rename it to Index n which would be more intuitive?
[ ] Indexing into tensors. The lookup operator is currently x ! i which conflicts pretty heavily with imperative languages' syntax for logical negation. Ideally we would have it look something more like lookup in imperative languages x[i] but I'm unsure if we can get the parser to accept that syntax for both list literals and lookup... If that doesn't work then @yiergot suggestions x @ i which at least is more readable.

MatthewDaggitt commented 2 years ago

Fin was changed to Index in 8c25ce6cd0e4faea5c0ed9009ed35869e4ba984a

MatthewDaggitt commented 2 years ago

@bobatkey suggested that we consider copying Dex and reusing the . as lookup, e.g. x . 0 or x . strongLeft. The only niggle is that if the user writes f x.0 gets parsed as (f x).0. Unfortunately if the user intends the former, it won't always be guaranteed to give a type-error, e.g. f : Tensor Rat [2] -> Tensor Rat [2], x : Tensor Rat [2].

wenkokke commented 2 years ago

I think any tensor access operator should bind tighter than any other operator, including juxtaposition. For something in the style of a property access operator ., I think we should syntactically enforce no spaces around it.

MatthewDaggitt commented 2 years ago

I think any tensor access operator should bind tighter than any other operator, including juxtaposition. For something in the style of a property access operator ., I think we should syntactically enforce no spaces around it.

The combination of those together makes a lot of sense!

wenkokke commented 2 years ago

I think in that case, f x.0 where the user intends (f x).0 would always be a type error, otherwise the type of f would violate the occurrence check.

(Absolutely check me on this, though.)