search

raphlinus / ghilbert

Automatically exported from code.google.com/p/ghilbert
Apache License 2.0
48 stars 4 forks source link

Allow duplicate interface params. #6

Open abliss opened 7 years ago

abliss commented 7 years ago

This change seems to be required in order to define an interface generally as accepting two different types, but then allow it to be used in a specific instance where the types are the same.

(Also: improve the error message on param mismatch, which is very useful in debugging a typo in a complex nest of param layers.)

--

@raphlinus, please let me know whether you think this is sound or not. I don't know the reason why duplicate params were forbidden in the first place. This change was needed in order to verify my attemp at codifying typed SK combinators: https://github.com/abliss/ghilbert-app/commit/ccc205d9307f8989a4b3fd80e04f16a9c1490b3e I tried to do so as you suggested on the mailing list, and was unable to do it without this modification to the verifier. (But maybe I misunderstood what you meant, in which case, please let me know.)

abliss commented 7 years ago

Hm, it just occurred to me that perhaps I was supposed to solve this with a "kindbind" statement somewhere, but I've never understood exactly how to use them.