<div dir="auto">Not from Rational, Float, or Double.</div><br><div class="gmail_quote"><div dir="ltr">On Sun, Jun 3, 2018, 13:32 Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de">olf@aatal-apotheke.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">>Also note that what you're talking about is a special type of objects, <br>
>namely<br>
><br>
>    type BoundedEnum a = (Bounded a, Enum a) -- using ConstraintKinds<br>
><br>
>(I'm sure the mathematicians have a better name for this)<br>
<br>
Indeed the Prelude states no laws for Bounded. But maybe we all agree on this:<br>
<br>
forall a. fromEnum minBound <= fromEnum a <= fromEnum maxBound<br>
<br>
With this law and the rule fromEnum.toEnum=id (for those integers that this type's toEnum accepts) we can say that (Bounded a,Enum a) is the class of all types which have a distinguished finite subset. If one assumes further the law toEnum.fromEnum=id (which is violated e.g. by Double) then (Bounded a,Enum a) are precisely the constructively finite types, that is, the types for which one can exhibit an isomorphism with a finite cardinal. Note that in constructive mathematics, a set may be known to be finite in the sense that the assumption it is infinite is absurd, yet one can not name an isomorphism with a finite cardinal. [*]<br>
<br>
As Jon Fairbairn pointed out, (Int,Int) can be given an Enum instance. The same is true for every type that is build from types that already have an Enum instance using only sum and product. <br>
<br>
>This is all true, but I was implicitly assuming that Bounded and Enum ought<br>
>to agree with Ord.<br>
<br>
Consider this: From every type's Enum instance you can derive an Ord instance: <br>
compare = compare `Data.Function.on` fromEnum<br>
<br>
-- Olaf<br>
<br>
[*] In the text [1] by Andrej Bauer I found this funny theorem: Excluded middle is equivalent to the statement that subsets of finite sets are finite. <br>
[1] <a href="http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf" rel="noreferrer noreferrer" target="_blank">http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf</a><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>