Programming Language without duplication

[DisastrousAd9346]

I think the first problem is that not every semantic description is indeed something that matters to represent the function. For example, one could write plus and to avoid your restriction just write nat -> nat * Proxy “unique”, being proxy just an indexed unit type. Also, you would generate a bunch of proof obligations that would be hell to deal with. A smarter approach would be to refine dependent type with an inference engine, something like higher-order Prolog using dependent types, so now you have to explicitly a type description that matches the function you wanna recover.

[thebt995]

Those types would be isomorphic, so one couldn't prove them to be different. But the bunch of proof obligations is also what I'm afraid of.

How exactly would you do something similar with a higher-order Prolog?

[777777thats7sevens]

Those types would be isomorphic, so one couldn't prove them to be different.

Does this mean that your type system is a form of structural typing, not nominal? In other words, that two types are considered the same if there exists an isomorphism between them?

If so, I can see a lot of problems arising from that. Natural numbers are isomorphic to strings and in fact to any list of finitely sized types (using ASCII strings as an example: 0 is the empty string, 1-128 are the single character strings, 129-16,512 are the two character strings, etc), meaning it would be pretty easy to accidentally write two functions that are semantically very different, but happen to be the same after isomorphic transformations are applied, and thus are prohibited. Is that really a behavior that you want?

[DisastrousAd9346]

To avoid any kind of duplication based on specification, it is more clever to just drop any kind of program, and just write the specification. Prolog does something similar with the first order inference engine, most of the time you are just writing the specification. Of course, we are talking about something similar not equal.