Uny, build small datatypes with algebraic expressions

Uny.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Uny where

import Data.Kind (Type, Constraint)
import Data.Bifunctor
import Data.Bifoldable
import Data.Bitraversable
import Data.Traversable

data Y
data N
data y ? n

data Uny p as where
  U ::                     Uny  Y            as
  N ::      !(Uny n as) -> Uny (y ? n) (a ': as)
  Y :: a -> !(Uny y as) -> Uny (y ? n) (a ': as)

type family AllC (c :: Type -> Constraint) (as :: [Type]) :: Constraint where
  AllC c '[] = ()
  AllC c (a ': as) = (c a, AllC c as)

deriving instance AllC Eq as => Eq (Uny p as)
deriving instance (AllC Eq as, AllC Ord as) => Ord (Uny p as)
deriving instance AllC Show as => Show (Uny p as)

type Zero = N
type One = Y
type A = Y ? N
type B = N ? A
type C = N ? B
type D = N ? C

type family a + b :: Type where
  N + a = a
  a + N = a
  Y + Y = Y
  Y + (a ? b) = a ? Y + b
  (a ? b) + Y = a ? b + Y
  (a ? b) + (c ? d) = a + c ? b + d

type family a * b :: Type where
  N * a = N
  a * N = N
  Y * a = a
  a * Y = a
  (a ? b) * (c ? d) = a * b + a * d + b * c ? b * d

infixl 7 *
infixl 6 +
infixl 5 ?

{-
type Void = Uny0 Zero
type Unit = Uny0 One
type V1 a = Uny1 Zero a
type U1 a = Uny1 One a
type Identity a = Uny1 A a
type Maybe a = Uny1 (A + One) a
type Tuple a b = Uny2 (A * B) a b
type Either a b = Uny2 (A + B) a b
type These a b = Uny2 (A*B + A + B) a b
type Can a b = Uny2 (A*B + A + B + One) a b
type Wedge a b = Uny2 (A + B + One) a b
type Smash a b = Uny2 (A*B + One) a b
type Tuple3 a b c = Uny3 (A * B * C) a b c
-}

type family AllP (as :: [Type]) :: Type where
  AllP '[] = Y
  AllP (a ': as) = AllP as ? N

type family Kleislis m (as :: [Type]) (bs :: [Type]) :: [Type] where
  Kleislis m '[] '[] = '[]
  Kleislis m (a ': as) (b ': bs) = (a -> m b) ': Kleislis m as bs

class TraverseUny as bs where
  traverseUny :: Applicative m => Uny (AllP as) (Kleislis m as bs) -> Uny p as -> m (Uny p bs)

instance TraverseUny '[] '[] where
  traverseUny U U = pure U

instance TraverseUny as bs => TraverseUny (a ': as) (b ': bs) where
  traverseUny  _        U       = pure U
  traverseUny (Y _ fs) (N   as) = N <$>         traverseUny fs as
  traverseUny (Y f fs) (Y a as) = Y <$> f a <*> traverseUny fs as

-- not a real traversal due to the `forall q.` but useful
_tail :: Applicative f => (forall q. Uny q as1 -> f (Uny q as2)) -> Uny p (a ': as1) -> f (Uny p (a ': as2))
_tail _ U = pure U
_tail f (N as) = N <$> f as
_tail f (Y a as) = Y a <$> f as

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

_a :: Traversal (Uny p (a1 ': as)) (Uny p (a2 ': as)) a1 a2
_a _ U = pure U
_a _ (N as) = pure (N as)
_a f (Y a as) = (`Y` as) <$> f a

_b :: Traversal (Uny p (a ': b1 ': as)) (Uny p (a ': b2 ': as)) b1 b2
_b f = _tail (_a f)

_c :: Traversal (Uny p (a ': b ': c1 ': as)) (Uny p (a ': b ': c2 ': as)) c1 c2
_c f = _tail (_b f)

_d :: Traversal (Uny p (a ': b ': c ': d1 ': as)) (Uny p (a ': b ': c ': d2 ': as)) d1 d2
_d f = _tail (_c f)

newtype Uny0 p = Uny0 { unUny0 :: Uny p '[] } deriving (Eq, Ord, Show)
newtype Uny1 p a = Uny1 { unUny1 :: Uny p '[a] } deriving (Eq, Ord, Show)
newtype Uny2 p a b = Uny2 { unUny2 :: Uny p '[a, b] } deriving (Eq, Ord, Show)
newtype Uny3 p a b c = Uny3 { unUny3 :: Uny p '[a, b, c] } deriving (Eq, Ord, Show)

instance Functor (Uny1 p) where
  fmap = fmapDefault
instance Foldable (Uny1 p) where
  foldMap = foldMapDefault
instance Traversable (Uny1 p) where
  traverse f = fmap Uny1 . traverseUny (Y f U) . unUny1

instance Functor (Uny2 p a) where
  fmap = fmapDefault
instance Foldable (Uny2 p a) where
  foldMap = foldMapDefault
instance Traversable (Uny2 p a) where
  traverse f = bitraverse pure f
instance Bifunctor (Uny2 p) where
  bimap = bimapDefault
instance Bifoldable (Uny2 p) where
  bifoldMap = bifoldMapDefault
instance Bitraversable (Uny2 p) where
  bitraverse f g = fmap Uny2 . traverseUny (Y f (Y g U)) . unUny2

instance Functor (Uny3 p a b) where
  fmap = fmapDefault
instance Foldable (Uny3 p a b) where
  foldMap = foldMapDefault
instance Traversable (Uny3 p a b) where
  traverse f = bitraverse pure f
instance Bifunctor (Uny3 p a) where
  bimap = bimapDefault
instance Bifoldable (Uny3 p a) where
  bifoldMap = bifoldMapDefault
instance Bitraversable (Uny3 p a) where
  bitraverse f g = fmap Uny3 . traverseUny (Y pure (Y f (Y g U))) . unUny3

type Test a b c = Uny ((A + One) * (B + C + One)) '[a, b, c]
test :: (Show a, Show b, Show c) => Test a b c -> String
test (Y a (Y b U)) = show (a, b)
test (Y a (N (Y c U))) = show (a, c)
test (Y a (N (N U))) = show a
test (N (Y b U)) = show b
test (N (N (Y c U))) = show c
test (N (N (N U))) = ""

newtype These a b = T (Uny2 (A*B + A + B) a b) deriving (Eq, Ord, Functor, Foldable, Bifunctor, Bifoldable)
pattern This :: a -> These a b
pattern This a = T (Uny2 (Y a (N U)))
pattern That :: b -> These a b
pattern That b = T (Uny2 (N (Y b U)))
pattern These :: a -> b -> These a b
pattern These a b = T (Uny2 (Y a (Y b U)))
{-# COMPLETE This, That, These #-}
instance (Show a, Show b) => Show (These a b) where
  showsPrec p (These a b) = showParen (p > 10) $ showString "These " . showsPrec 11 a . showString " " . showsPrec 11 b
  showsPrec p (This a) = showParen (p > 10) $ showString "This " . showsPrec 11 a
  showsPrec p (That b) = showParen (p > 10) $ showString "That " . showsPrec 11 b
instance Traversable (These a) where traverse f (T u) = fmap T $ traverse f u
instance Bitraversable These where bitraverse f g (T u) = fmap T $ bitraverse f g u