GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 123 forks source link

Allow instances of Field and other typeclasses #912

Open ramsdell opened 3 years ago

ramsdell commented 3 years ago

The addition of the Field type class is a significant improvement. Thank you for that.

I implemented the operations of the field GF(16) and then defined vectors and matrices over this field. It all works, however, what I really want to be able to do is define vectors and matrices over members of typeclass Field, assert that GF(16) is a member of this typeclass, and then get definitions of vectors and matrices of this field implicitly. That is, I asking for the equivalent of instance in Haskell.

brianhuffman commented 3 years ago

We've talked about this idea at various times (e.g. #367). It would be pretty nice to use. One thing holding us back is that this would require Cryptol to have user-defined types, whereas currently Cryptol has a closed universe of types; that would be a pretty fundamental change and would interact with other design decisions in lots of ways. Also, using features like user-definable infix operators and explicit dictionary passing, you can get by reasonably well without user-defined instances.

weaversa commented 3 years ago

Maybe a possible solution would be to extend the Field type class by creating a Field module (similar to the new Float module) that provides common methods for fields.

brianhuffman commented 3 years ago

Another thing to keep in mind is that we are currently working on a new-and-improved design for parameterized modules for Cryptol (#815). The new system will be rather similar to functors in Standard ML. One of the things you'll be able to do with it is to write modules that define the operations of a field, and then have other parameterized modules that you can instantiate with whatever field you want.