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

[Olaf Klinke]

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-inclusion-polymorphism/AnyNum.cpp
> 
> 
> On Fri, May 27, 2022 at 12:32 AM Olaf Klinke <olf at aatal-apotheke.de> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: FreeNum.hs
Type: text/x-haskell
Size: 2924 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220527/cf2a2b99/attachment.hs>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Directed.hs
Type: text/x-haskell
Size: 926 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220527/cf2a2b99/attachment-0001.hs>