<br><br><div class="gmail_quote">On Thu, Jun 23, 2011 at 1:15 PM, wren ng thornton <span dir="ltr">&lt;<a href="mailto:wren@freegeek.org">wren@freegeek.org</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im"><br></div>
<br>
To put a different spin on it, in the dual case we can show that Haskell&#39;s<br>
(,) is not a categorical product. There&#39;s a good deal of historical debate<br>
about why it works the way it does, but if we&#39;re looking to make a better<br>
system then the fact that tuples are not well-behaved suggests a place for<br>
improvement. The current (,) is a compromise between two different notions<br>
of product in domain theory. On the one hand we have domain products<br>
(which do not produce domains) and on the other hand we have smash<br>
products (which can &quot;lose&quot; information). I&#39;ve had in mind for a while to<br>
make a Haskell-like language with a total functional core. In a total<br>
language (even a lazy one), we don&#39;t have bottom so we don&#39;t need domain<br>
theory to reason about the language. So in a language which is only<br>
partially total, it&#39;s reasonable to have two different kinds of<br>
products--- which means we can get away from Haskell&#39;s compromise, but do<br>
so in a way that&#39;s harmonious with the rest of the language. Would this<br>
new system be &quot;better&quot;? I dunno. It would behave in a more lawful manner,<br>
so it should be easier to reason about; but then we&#39;re making programmers<br>
keep that reasoning in mind, and maybe that&#39;s too much work. A decent<br>
system has to be both correct but also usable, and human factors are messy<br>
and hard to predict.<br></blockquote><div><br></div><div><br></div><div>Please read &quot;Fast and Loose Reasoning is Morally Correct&quot;. <a href="http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf">http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf</a></div>
<div> </div><div>As I have told you before, it is perfectly appropriate to ignore bottom-the-type and bottoms-the-inexpressible proto-values to recover the categorical product semantics of (,).  It&#39;s not even hard.  It will make your life easier.  All you have to do is apply an equivalence relation that considers all bottom-proto-values as equivalent.  Domain theory is an unnecessary complication.  All bottoms have the same semantics anyway -- they all diverge.</div>
</div>