[Haskell-cafe] No Enum for (,), no Enum or Bounded for Either
zemyla at gmail.com
Mon Jun 4 16:49:17 UTC 2018
Not from Rational, Float, or Double.
On Sun, Jun 3, 2018, 13:32 Olaf Klinke <olf at aatal-apotheke.de> wrote:
> >Also note that what you're talking about is a special type of objects,
> > 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
> 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
> >to agree with Ord.
> Consider this: From every type's Enum instance you can derive an Ord
> compare = compare `Data.Function.on` fromEnum
> -- Olaf
> [*] In the text  by Andrej Bauer I found this funny theorem: Excluded
> middle is equivalent to the statement that subsets of finite sets are
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe