[Haskell-cafe] No Enum for (,), no Enum or Bounded for Either

[Zemyla]

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,
> >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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180604/6a36372e/attachment.html>