Re: [Haskell-cafe] Should there be a haskell template for inclusion polymorphism in Haskell?

So my central questions for discussions are:
- Is inclusion polymorphism something we should use at all in Haskell? - These boiler plate code maybe better be generated using Haskell template instead, is there one already, or should there be one?
Maybe one of the authors of a sub-typing library can share a more informed opinion on this. My view as a mathematician: A type being a subtype of another is a relation between types. Relations between types is what multi-parameter type classes is about. Hence it seems that this is how subtypes in Haskell ought to be done. For example, in the attenuation and records-sop package, the latter of which is based on genercis-sop, which depends on Template Haskell. So without having used any of the mentioned packages, I believe your second question can be answered with "yes". Regarding the first question, we should probably ask ourselves how much type-safety we're sacrificing for the convenience we gain. The Num example you gave shows one possible danger: While a subtype relation may hold mathematically, the implementiation details may cause this relation to fail in reality. Example: All floating point numbers are rationals, aren't they? So there should be a subtype relation. But how to convert NaN, -infinity or -0 of type Double to a pair of Integers? Olaf

Very interesting that you are mentioning looking into multi-parameter type
classes! I will think a bit about it.
And thanks for the libraries you suggested, will also need to take some
times to look into them
FWIW: I made an actual OOP-style code in C++ to demonstrate the difference
between compile-time and run-time polymorphism
https://github.com/hellwolf/haskell-examples/blob/master/2022-05-25-inclusio...
On Fri, May 27, 2022 at 12:32 AM Olaf Klinke
So my central questions for discussions are:
- Is inclusion polymorphism something we should use at all in Haskell? - These boiler plate code maybe better be generated using Haskell template instead, is there one already, or should there be one?
Maybe one of the authors of a sub-typing library can share a more informed opinion on this. My view as a mathematician: A type being a subtype of another is a relation between types. Relations between types is what multi-parameter type classes is about. Hence it seems that this is how subtypes in Haskell ought to be done. For example, in the attenuation and records-sop package, the latter of which is based on genercis-sop, which depends on Template Haskell. So without having used any of the mentioned packages, I believe your second question can be answered with "yes". Regarding the first question, we should probably ask ourselves how much type-safety we're sacrificing for the convenience we gain. The Num example you gave shows one possible danger: While a subtype relation may hold mathematically, the implementiation details may cause this relation to fail in reality. Example: All floating point numbers are rationals, aren't they? So there should be a subtype relation. But how to convert NaN, -infinity or -0 of type Double to a pair of Integers?
Olaf

On Fri, 2022-05-27 at 13:50 +0300, Miao ZhiCheng wrote:
Very interesting that you are mentioning looking into multi-parameter type classes! I will think a bit about it.
And thanks for the libraries you suggested, will also need to take some times to look into them
FWIW: I made an actual OOP-style code in C++ to demonstrate the difference between compile-time and run-time polymorphism https://github.com/hellwolf/haskell-examples/blob/master/2022-05-25-inclusio...
On Fri, May 27, 2022 at 12:32 AM Olaf Klinke
wrote: So my central questions for discussions are:
- Is inclusion polymorphism something we should use at all in Haskell? - These boiler plate code maybe better be generated using Haskell template instead, is there one already, or should there be one?
Maybe one of the authors of a sub-typing library can share a more informed opinion on this. My view as a mathematician: A type being a subtype of another is a relation between types. Relations between types is what multi-parameter type classes is about. Hence it seems that this is how subtypes in Haskell ought to be done. For example, in the attenuation and records-sop package, the latter of which is based on genercis-sop, which depends on Template Haskell. So without having used any of the mentioned packages, I believe your second question can be answered with "yes". Regarding the first question, we should probably ask ourselves how much type-safety we're sacrificing for the convenience we gain. The Num example you gave shows one possible danger: While a subtype relation may hold mathematically, the implementiation details may cause this relation to fail in reality. Example: All floating point numbers are rationals, aren't they? So there should be a subtype relation. But how to convert NaN, -infinity or -0 of type Double to a pair of Integers?
Olaf
Miao, Your existential type AnyNum is the union of all number types, but even set-theoretically there is no way of extending individual operations on many sets to a single operation on the union of all sets, even when the operations commute with subset inclusion. That ony works if the union is directed (see attached), that is, if for every two sets A and B there is a third set C in the union of which both other sets are a subset. So in order to implement AnyNum (5 :: Rational) + AnyNum (NaN :: Double) you first have to find a single other Num type that Rational and Double can be cast into, then perform the (+) there. What the libraries like generics-sop, attenuation and to some extent the Prelude do is to construct a hierarchy either via multi-parameter type classes A `IsSubtypeOf` B or constrained classes like Num a => Fractional a That may culminate in a most inclusive type or type class, providing all the operations of its ancestors. Notice the reversal of inclusions: Integer `IsSubtypeOf` Rational fromInteger :: Integer -> Rational instance Num Integer instance Fractional Rational Rational `IsSubclassOf` Num Instead of the union of all types under consideration, maybe the intersection is useful to you. Attached is a module that implements the initial object of a class (which I think in the case of Num is isomorphic to Integer), that is a type that can do everything every other Num type can do, but nothing more. AnyNum is the terminal object of Num. -- The initial object in the Num class newtype FreeNum = FreeNum { runNum :: forall r. (Integer -> r) -> -- fromInteger (r -> r -> r) -> -- (+) (r -> r -> r) -> -- (*) (r -> r) -> -- negate (r -> r) -> -- abs (r -> r) -> -- signum r } On this, we can implement numeric operations without casting. Olaf

Hi Olaf! Sorry for a bit of delay, I finally managed to digest your inputs. Your existential type AnyNum is the union of all number types, but even
set-theoretically there is no way of extending individual operations on many sets to a single operation on the union of all sets, even when the operations commute with subset inclusion. That ony works if the union is directed (see attached), that is, if for every two sets A and B there is a third set C in the union of which both other sets are a subset.
So in order to implement
AnyNum (5 :: Rational) + AnyNum (NaN :: Double) you first have to find a single other Num type that Rational and Double can be cast into, then perform the (+) there.
Thank you for the example! I managed to play around with it, and added a bit more general examples: ``` instance Castable Integer Double where cast1 = fromInteger instance Castable Rational Double where cast1 = fromRational instance Castable Double Double where cast1 = id instance (Castable a Double, Castable b Double) => Directed Num a b Double where castUnion _ (a, b) = (cast1 a, cast1 b) genericPlus :: forall a b c. (Num a, Num b, Num c, Directed Num a b c) => a -> b -> c genericPlus = castOp (Proxy :: Proxy Num) (+) main = do print $ show $ genericPlus (2 :: Integer) (5 :: Integer) print $ show $ genericPlus (1/3 :: Rational) (5 :: Integer) print $ show $ genericPlus (1/3 :: Rational) (2/3 :: Rational) print $ show $ genericPlus (4 :: Integer) (2/3 :: Rational) ``` That's interesting, it also makes me think how the C language style of "implicit casting" is working under the hood.
What the libraries like generics-sop, attenuation and to some extent the Prelude do is to construct a hierarchy either via multi-parameter type classes A `IsSubtypeOf` B or constrained classes like Num a => Fractional a That may culminate in a most inclusive type or type class, providing all the operations of its ancestors. Notice the reversal of inclusions:
Integer `IsSubtypeOf` Rational fromInteger :: Integer -> Rational instance Num Integer instance Fractional Rational Rational `IsSubclassOf` Num
Instead of the union of all types under consideration, maybe the intersection is useful to you. Attached is a module that implements the initial object of a class (which I think in the case of Num is isomorphic to Integer), that is a type that can do everything every other Num type can do, but nothing more. AnyNum is the terminal object of Num.
-- The initial object in the Num class newtype FreeNum = FreeNum { runNum :: forall r. (Integer -> r) -> -- fromInteger (r -> r -> r) -> -- (+) (r -> r -> r) -> -- (*) (r -> r) -> -- negate (r -> r) -> -- abs (r -> r) -> -- signum r }
On this, we can implement numeric operations without casting.
That's the next level... I don't think I can manage to figure out how to define "operations in NumSig num" or even a `freeDouble` today... Although it already deviates from my original inquiry, which was about run-time polymorhpism and have some sort of OO-style INum class in Haskell. As later I figured out, a "+=" operator would make more sense for "objects", and type checkings could be run-time using Typeable. But I learned something already, fun exercise so far though! Best regards, Miao
Olaf

On Wed, 2022-06-01 at 02:54 +0300, Miao ZhiCheng wrote:
it also makes me think how the C language style of "implicit casting" is working under the hood.
Ooh, good question! I am not a C expert. Can anyone more experienced share some details, please? In Kernighan & Ritchie I found this wonderful sentence at the beginning of Section 2.7: "In general, the only conversions that happen automatically are those that make sense, ..." And further: "Implicit arithmetic conversions work much as expected. In general, if an operator like + or * which takes two operands (a 'binary operator') has operands of different types, the 'lower' type is promoted to the 'higher' type before the operation proceeds." This suggests that C, too, maintains a directed hierarchy [1] of (numeric) types in which implicit conversions are performed. Attempt to perform an explicit conversion not of this hierarchy (e.g. a struct) is a compile-time error. Except, the hierarchy is not really directed, because implicitly casting "down" or "across" the hierarchy is also allowed. The following is accepted by gcc 8.3.0. unsigned long l = 3000; double d = -3.4; long x = l + d; // which is higher: long or double? double y = l + d; K & R mention that implicit casting can lose information, e.g. by rounding. I suppose a sane implementation in Haskell would want to avoid that. Olaf [1] https://www.guru99.com/images/1/020819_0641_TypeCasting2.png

The first gcc example upcasts l to `double` before the addition, then
casts the result of the addition down to `long` which loses
information by truncation and possibly range (which can be triggered
by either the `unsigned long` or the `double`; but neither one
triggers that in this particular example). `long` and `unsigned long`
are below both `float` and `double` in the hierarchy because the
exponent can easily push a value out of their range.
I'll also note that currently `fromIntegral` in Haskell doesn't verify
range, so one can argue that a casting implementation has prior art to
refer to.
On Wed, Jun 1, 2022 at 2:52 PM Olaf Klinke
On Wed, 2022-06-01 at 02:54 +0300, Miao ZhiCheng wrote:
it also makes me think how the C language style of "implicit casting" is working under the hood.
Ooh, good question! I am not a C expert. Can anyone more experienced share some details, please? In Kernighan & Ritchie I found this wonderful sentence at the beginning of Section 2.7: "In general, the only conversions that happen automatically are those that make sense, ..." And further:
"Implicit arithmetic conversions work much as expected. In general, if an operator like + or * which takes two operands (a 'binary operator') has operands of different types, the 'lower' type is promoted to the 'higher' type before the operation proceeds."
This suggests that C, too, maintains a directed hierarchy [1] of (numeric) types in which implicit conversions are performed. Attempt to perform an explicit conversion not of this hierarchy (e.g. a struct) is a compile-time error. Except, the hierarchy is not really directed, because implicitly casting "down" or "across" the hierarchy is also allowed. The following is accepted by gcc 8.3.0. unsigned long l = 3000; double d = -3.4; long x = l + d; // which is higher: long or double? double y = l + d; K & R mention that implicit casting can lose information, e.g. by rounding. I suppose a sane implementation in Haskell would want to avoid that.
Olaf
[1] https://www.guru99.com/images/1/020819_0641_TypeCasting2.png
_______________________________________________ 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.
-- brandon s allbery kf8nh allbery.b@gmail.com

Not to mention the horror and hilarity of endless JS surprises: ```js
"4"+2 '42' "4"-2 2 +"4"+2 6 "5"*true 5 "5"+true '5true' "5"/false Infinity // and so on and so on...
To end this thread, actually I finally found out that most of the
discussion we had so far could be summarized perfectly well in
* Cardelli, Luca, and Peter Wegner. "On understanding types, data
abstraction, and polymorphism." *
The question if Haskell should have inclusion polymorphism still does not
have a satisfying answer to me, but I found that
https://discourse.haskell.org/search?q=oop seem to have some good threads
to read more on.
Cheers everyone.
On Wed, Jun 1, 2022 at 10:01 PM Brandon Allbery <allbery.b@gmail.com> wrote:
> The first gcc example upcasts l to `double` before the addition, then
> casts the result of the addition down to `long` which loses
> information by truncation and possibly range (which can be triggered
> by either the `unsigned long` or the `double`; but neither one
> triggers that in this particular example). `long` and `unsigned long`
> are below both `float` and `double` in the hierarchy because the
> exponent can easily push a value out of their range.
>
> I'll also note that currently `fromIntegral` in Haskell doesn't verify
> range, so one can argue that a casting implementation has prior art to
> refer to.
>
> On Wed, Jun 1, 2022 at 2:52 PM Olaf Klinke <olf@aatal-apotheke.de> wrote:
> >
> > On Wed, 2022-06-01 at 02:54 +0300, Miao ZhiCheng wrote:
> > > it also makes me think how the C language style of
> > > "implicit casting" is working under the hood.
> >
> > Ooh, good question! I am not a C expert. Can anyone more experienced
> > share some details, please? In Kernighan & Ritchie I found this
> > wonderful sentence at the beginning of Section 2.7:
> > "In general, the only conversions that happen automatically are those
> > that make sense, ..."
> > And further:
> >
> > "Implicit arithmetic conversions work much as expected. In general, if
> > an operator like + or * which takes two operands (a 'binary operator')
> > has operands of different types, the 'lower' type is promoted to the
> > 'higher' type before the operation proceeds."
> >
> > This suggests that C, too, maintains a directed hierarchy [1] of
> > (numeric) types in which implicit conversions are performed. Attempt to
> > perform an explicit conversion not of this hierarchy (e.g. a struct) is
> > a compile-time error.
> > Except, the hierarchy is not really directed, because implicitly
> > casting "down" or "across" the hierarchy is also allowed. The following
> > is accepted by gcc 8.3.0.
> > unsigned long l = 3000;
> > double d = -3.4;
> > long x = l + d; // which is higher: long or double?
> > double y = l + d;
> > K & R mention that implicit casting can lose information, e.g. by
> > rounding. I suppose a sane implementation in Haskell would want to
> > avoid that.
> >
> > Olaf
> >
> > [1] https://www.guru99.com/images/1/020819_0641_TypeCasting2.png
> >
> > _______________________________________________
> > 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.
>
>
>
> --
> brandon s allbery kf8nh
> allbery.b@gmail.com
>
participants (3)
-
Brandon Allbery
-
Miao ZhiCheng
-
Olaf Klinke