ML function of type 'a -> 'b - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-08-22T07:50:35Z https://cs.stackexchange.com/feeds/question/302 http://www.creativecommons.org/licenses/by-sa/3.0/rdf https://cs.stackexchange.com/q/302 18 ML function of type 'a -> 'b Gilles https://cs.stackexchange.com/users/39 2012-03-13T11:21:21Z 2017-08-01T01:57:33Z <p>Our professor asked us to think of a function in OCaml that has the type</p> <pre><code>'a -&gt; 'b </code></pre> <p>i.e. a function of one argument that could be anything, and that can return a different anything.</p> <p>I thought of using <code>raise</code> in a function that ignores its argument:</p> <pre><code>let f x = raise Exit </code></pre> <p>But the professor said there was a solution that doesn't require any function in the standard library. I'm confused: how can you make a <code>'b</code> if you don't have one in the first place?</p> <p><sub> I'm asking here rather than on Stack Overflow because I want to understand what's going on, I don't want to just see a program with no explanation. </sub></p> https://cs.stackexchange.com/questions/302/-/303#303 18 Answer by rgrig for ML function of type 'a -> 'b rgrig https://cs.stackexchange.com/users/15 2012-03-13T11:46:51Z 2012-03-13T17:17:44Z <p>The skeleton is <code>let f x = BODY</code>. In BODY you must use x only in generic ways (for example, don't send it to a function that expects integers), and you must return a value of <em>any</em> other type. But how can the latter part be true? The only way to satisfy the statement "for all types <code>'b</code>, the returned value is a value of type <code>'b</code>" is to make sure the function does <em>not</em> return. There are exactly two possibilities: either BODY faults or it doesn't terminate. The function <code>raise</code> faults, the following doesn't terminate:</p> <pre><code>let rec f x = f x </code></pre> https://cs.stackexchange.com/questions/302/-/304#304 19 Answer by Stéphane Gimenez for ML function of type 'a -> 'b Stéphane Gimenez https://cs.stackexchange.com/users/68 2012-03-13T11:48:13Z 2012-03-13T13:05:18Z <p>First, some remarks. Using only the core typed lambda calculus it's not possible to obtain <code>'a -&gt; 'b</code> because the typing system is in correspondence (via the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry Howard isomorphism</a>) to intuitionistic logics, and the corresponding formula <code>A → B</code> is not a tautology.</p> <p>Other extensions such as tuples and matchings/conditionals still preserve some logic consistency adding product types <code>*</code> which correspond to the logical connective <em>and</em>, and sum types <code>|</code> which correspond to the <em>or</em>. Again, don't expect them to produce that <code>'a -&gt; 'b</code> type, as it would allow one to prove some formula which is not a tautology. </p> <p>So your only chances are using other constructions which escape from the logics like <code>raise</code> (but you're not allowed to in this case)… or <code>let rec</code>! Recursion allows to build programs which never terminate, and their results can be given an arbitrary return type as they will never be produced. Now if you think about the most trivial non terminating function (the one which directly calls itself to return a result):</p> <pre><code>let rec f x = f x </code></pre> <p>You'll notice that its type is exactly <code>'a -&gt; 'b</code>: whatever is the provided argument, the result (which will never be computed) can be assumed to have any type.</p> <p>Of course this <code>f</code> is not an interesting function, but that's the point. In OCaml, any function whose type does not look like a valid formula is a suspicious function.</p> https://cs.stackexchange.com/questions/302/-/59951#59951 1 Answer by Demi for ML function of type 'a -> 'b Demi https://cs.stackexchange.com/users/15470 2016-06-23T19:22:55Z 2017-08-01T01:57:33Z <p>Using a compiler primitive you can write this:</p> <pre><code>external magic: 'a -&gt; 'b = "%identity" </code></pre> <p>(and indeed the compiler distribution provides this, though isn't part of the language). This is an unsafe identity cast.</p> <p>Your professor almost certainly doesn't want this. However, this is also the only <em>useful</em> function with type <code>'a -&gt; 'b</code> that I am aware of, and indeed it is used in the OCaml distribution itself.</p>