<p>In short, it is because <code>(+.)</code> and <code>(+)</code> as well as <code>1</code> and <code>1.</code> denote different values despite the fact that they look alike. Those values have different types, different representations, and different semantics. The feature of a language that makes <code>(+)</code> and <code>1</code> work the same in different contexts is called ad-hoc polymorphism and it is not present in OCaml. OCaml is not trying to infer which value you're going to use from the textual representation of your program and its type, instead, it infers what is the type of your program based on the values that you're using and how you're using them. It is an important distinction of ML wrt some other languages that move the other way around, i.e., they have the user-specified type and then infer the correct values that match that type and check that the values are used correctly. In ML the input is the program and the output is the type of that program, which is (a) used to prove that the program is well-typed and will not have any type errors in runtime and, (b), is used to generate native and performant code with all inferred types erased. It is also important to understand that type inference in OCaml is not a convenience utility that lets you omit the types when they could be inferred (like in C++'s <code>auto</code> or local type inference in Scala). Instead, it is a principal step in the compilation process and in the semantics of the language, as OCaml must be able to infer the type for any program. The types that we occasionally write in OCaml programs are used only as constraints and are never taken as inputs. Moreover, type annotations never change the behavior of the program. Well, unless GADTs come into play, but this is a completely different story.</p>
<p>For the deeper insight, we should recall that the type inference algorithm underneath OCaml is <em>syntax-driven</em> and <em>declarative</em>. The syntax-driven means that the program syntax fully defines the type of that program. Moreover, the algorithm ensures that if the type exists (i.e., the program is well-typed), then this inferred type is unique and principal. I.e., either there are no other types that represent this program or all other types are instances of the inferred type. The declarative means that the rules of how types are assigned to the programs are described with <a href="https://en.wikipedia.org/wiki/Type_rule" rel="noreferrer">declarative type rules</a>. This algorithm gives the formal translation of programs to types, which enables/ensures <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="noreferrer">Curry-Howard</a> correspondence, a deep connection between computer programs and mathematical proofs. That enables us to speak about program correctness and the other way around, about truth correctness, i.e., to prove with programs that our theorems are correct. This brings us back to the history of OCaml/ML, which was originally a Meta Language (ML) for <a href="https://en.wikipedia.org/wiki/Logic_for_Computable_Functions" rel="noreferrer">LCF</a> (Logic for Computable Functions) theorem prover.</p>
<p>Given that we agree that we don't want to lose that important property of the language, the question still remains open, why couldn't we implement ad-hoc polymorphism that is syntax-driven and declarable. Well, in fact, we can, for example, Haskell has one. And there is some work on adding <a href="https://arxiv.org/pdf/1512.01895.pdf" rel="noreferrer">modular implicits</a> to OCaml. But it all comes with the tradeoffs and it would be, at the end, a completely different language. So far, in OCaml, each value has a type or a type scheme and there is no type in the OCaml runtime system that will represent a <code>+</code> operator that works for ints and floats.</p>
<p>With that said, it would be dishonest to OCaml not to say that you can define your own <code>(+)</code> operator that will have type <code>number -&gt; number -&gt; number</code>, where the <code>number</code> is an existential <code>type number = Num : 'a typeid * 'a -&gt; number</code> with a separate table of operations for each <code>typeid</code> stored in some hidden hashtable. But this would be dynamic typing (see how the <code>typeid</code> is packed in each value) and it is completely different from the static typing, which gives you guarantees about your program before it runs (in our example this <code>(+)</code> function could fail in runtime and our typing rules are not declarative but are intrinsic to the implementation of the <code>(+)</code> operator).</p>
Why does OCaml have mandatory distinct float and int literal syntax?
<p>OCaml has distinct syntax for BOTH:</p>
<ul>
<li>float operations vs. int operations. Float operations end in dot: <code>+.</code>.</li>
<li>float literals vs. int literals. Floats literals end in dot: <code>3.</code>.</li>
</ul>
<pre class="lang-ml prettyprint-override"><code># 3 + 3;;
- : int = 6
# 3. +. 3.;;
- : float = 6.
# 3. + 3;;
Error: This expression has type float but an expression was expected of type
         int
</code></pre>
<p>I can see using one of these mechanisms to disambiguate, but why are two needed <em>always</em>?
For example, I could see a case where <code>.</code> is <em>sometimes</em> needed at the end of a literal, but not why it is needed for <code>3 +. 3</code> where OCaml could figure out that we want float arithmetic because we're saying we want float arithmetic.</p>
<p>I'm looking for specific technical justification based on interaction with other language features–not opinion or arguments from ergonomics.</p>