search

vehicle-lang / vehicle

A toolkit for enforcing logical specifications on neural networks
https://vehicle-lang.readthedocs.io/
Other
80 stars 7 forks source link

Get rid of automatic generalisation and use variable declarations instead #456

Open MatthewDaggitt opened 1 year ago

MatthewDaggitt commented 1 year ago

I'm writing so so many bugs with it when I misspell something in the type-signature.

wenkokke commented 1 year ago

Could you share some examples of these bugs, so that we could use those to see if we can put better guard rails on automatic generalisation?

MatthewDaggitt commented 1 year ago

There's the classic ones with a simple misspelling, e.g.:

fun : InputVectro -> Rat
fun x = x ! 0

but also cases where you rename some type but you forget to change all the occurrences of it.

The problem is that they lead to absolutely baffling error messages.

wenkokke commented 1 year ago

Haskell and—I think—Idris2 only generalise over lowercase names. Would that help a lot already?