Skip to content

Levity-polymorphic data types

I don't know if this belongs as a part of levity-polymorphic type classes (#12708) but many data types can be made levity-polymorphic, some have just been added to base:

-- Product Array# Array# :: Type -> Type
data Product :: forall rep. (k -> TYPE rep) -> (k -> TYPE rep) -> (k -> Type) where
  Pair :: f a -> g a -> (Product f g) a

-- Sum Array# Array# :: Type -> Type
data Sum :: forall rep. (k -> TYPE rep) -> (k -> TYPE rep) -> (k -> Type) where
  InL :: f a -> (Sum f g) a
  InR :: g a -> (Sum f g) a

-- Compose Array# [] :: Type -> Type
data Compose :: forall rep. (b -> TYPE rep) -> (a -> b) -> (a -> Type) where
  Compose :: f (g a) -> (Compose f g) a

Can you think of other examples?

Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information