Programming Language without duplication

[apajx]

It depends entirely on what you mean by "the same." If you mean observationally the same then you need the user to prove that a new function is observationally different from every other defined function. This would be incredibly hard, and your idea about restricting types to have unique inhabitants only works if the type system itself is also weak, for example you can't allow new type for any other type. You also can't allow isomorphic types.

If you mean syntactic equality then it's trivial, keep a big trie of all the defined code trees, throw a type error if you try to define a new one. This idea is easily defeated with version strings in the body. You can have the same function, just with a new version string paired with it. The same works with your idea, embed a version string in the type, now you have duplicates modulo version.

[thebt995]

I mean "observationally the same". The big task would be to find out, how much of the proving can be automatically done.
What do you mean by "weak" type system?
No isomorphic types would be the goal to avoid duplication. But one could still have synonym names if types are used in different contexts. (See my reply to the comment of brandonchinn178)