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

27 May 2022

      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