Re: No Enum for (,), no Enum or Bounded for Either

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Re: No Enum for (,), no Enum or Bounded for Either

Olaf Klinke
>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.
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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.

_______________________________________________
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.