>Also note that what you're talking about is a special type of objects,
>namely > > type BoundedEnum a = (Bounded a, Enum a) -- using ConstraintKinds > >(I'm sure the mathematicians have a better name for this) Indeed the Prelude states no laws for Bounded. But maybe we all agree on this: forall a. fromEnum minBound <= fromEnum a <= fromEnum maxBound 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. [*] 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. >This is all true, but I was implicitly assuming that Bounded and Enum ought >to agree with Ord. Consider this: From every type's Enum instance you can derive an Ord instance: compare = compare `Data.Function.on` fromEnum -- Olaf [*] 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. [1] http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Not from Rational, Float, or Double. On Sun, Jun 3, 2018, 13:32 Olaf Klinke <[hidden email]> wrote: >Also note that what you're talking about is a special type of objects, _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Free forum by Nabble | Edit this page |