Re: [Haskell-cafe] No Enum for (,), no Enum or Bounded for Either
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-09...
Not from Rational, Float, or Double.
On Sun, Jun 3, 2018, 13:32 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-09... _______________________________________________ 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.
participants (2)
-
Olaf Klinke -
Zemyla