История изменений

Это объединение, а не сумма

Которое всё равно fiber сумма в самом топосе и обычная сумма в категории частичного порядка подъобъктов.

Racket выезжает за счёт того что lispobject-ы и так тегированы — нетегированное объединение тегированных значений ~ тегированное объединение нетегированных значений, ну и monic-и ещё «расставляет» (то есть — нет, так как теги уже есть), в ML-ях их руками пишут (вводя теги), например:

data a :+ b = L a | R b deriving Show
class b :> a where sup :: a -> b
instance a :+ b :> a where sup = L
instance a :+ b :> b where sup = R

sin_ :: Integer -> Double
sin_ = sin . fromInteger

f :: Integer -> Double :+ String
f x = if odd x then sup $ sin_ x else sup "abc"

(правда такой sup в полиморфизм совершенно не умеет). И дальше главное, чтобы a + b -> a и a + b -> b не производились — они epic-и, но не monic-и, так что об автоматических преобразованиях не может быть речи — статика предполагает что их нет, есть только a + b -> c если есть a -> c _и_ b -> c, какая-то статика может их допускать в виде non-exhaustiveness с compile-time предупреждениями и расставлением исключений. Но динамика отличается тем, что допускает вообще любые top -> some и, как следствие, anything -> anything', так как anything -> top -> anything', так что звучит это либо в мире где только top (а нам в любом случае нужны примитивные типы и операции, так что ULC это не вариант), либо если семантика выполнения предполагает наличие _|_.

Это объединение, а не сумма

Которое всё равно fiber сумма в самом топосе и обычная сумма в категории частичного порядка подъобъктов.

Racket выезжает за счёт того что lispobject-ы и так тегированы — нетегированное объединение тегированных значений ~ тегированное объединение нетегированное значений, ну и monic-и ещё «расставляет» (то есть — нет, так как теги уже есть), в ML-ях их руками пишут (вводя теги), например:

data a :+ b = L a | R b deriving Show
class b :> a where sup :: a -> b
instance a :+ b :> a where sup = L
instance a :+ b :> b where sup = R

sin_ :: Integer -> Double
sin_ = sin . fromInteger

f :: Integer -> Double :+ String
f x = if odd x then sup $ sin_ x else sup "abc"

(правда такой sup в полиморфизм совершенно не умеет). И дальше главное, чтобы a + b -> a и a + b -> b не производились — они epic-и, но не monic-и, так что об автоматических преобразованиях не может быть речи — статика предполагает что их нет, есть только a + b -> c если есть a -> c _и_ b -> c, какая-то статика может их допускать в виде non-exhaustiveness с compile-time предупреждениями и расставлением исключений. Но динамика отличается тем, что допускает вообще любые top -> some и, как следствие, anything -> anything', так как anything -> top -> anything', так что звучит это либо в мире где только top (а нам в любом случае нужны примитивные типы и операции, так что ULC это не вариант), либо если семантика выполнения предполагает наличие _|_.