summer (empty) → 0.1.0.0

raw patch · 8 files changed

+597/−0 lines, 8 filesdep +basedep +summerdep +vectorsetup-changed

Dependencies added: base, summer, vector

Files

• CHANGELOG.md +5/−0
• LICENSE +9/−0
• README.md +23/−0
• Setup.hs +2/−0
• src/Data/Prodder.hs +184/−0
• src/Data/Summer.hs +207/−0
• summer.cabal +32/−0
• test/Test.hs +135/−0

@@ -0,0 +1,5 @@+# Revision history for extensible-sums++## 0.1.0.0 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.

@@ -0,0 +1,9 @@+Copyright 2020 Samuel Schlesinger++Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.++

@@ -0,0 +1,23 @@+# summer++Extensible sums and products for Haskell.++```haskell+x :: Sum '[Int, Bool, Float]+x = Inj True++y :: Sum '[Int, Float, Bool, Char]+y = weaken x++a :: Bool+a = match y (== 10) (== 0.2) id (== 'x')++x' :: Prod '[Int, Float, Bool, Char]+x' = produce $ \f -> f 10 0.2 True 'x'++y' :: Prod '[Bool, Float]+y' = strengthen x'++a' :: Bool+a' = consume y' (\b f -> b && f == 0.2)+```

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,184 @@+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE TypeFamilies #-}+{- |+Module: Data.Prodder+Copyright: (c) Samuel Schlesinger 2020+License: MIT+Maintainer: sgschlesinger@gmail.com+Stability: experimental+Portability: non-portable+Description: Extensible products+-}+module Data.Prodder+  ( -- * The extensible product type+    Prod+    -- * Type families+  , IndexIn+  , HasIndexIn+  , Consumer+  , (<>)+    -- * Construction and deconstruction+  , extract+  , index+  , tailN+  , initN+  , dropFirst+  , Consume(consume, produce, extend1, cmap)+    -- * Rearranging and removing elements+  , Strengthen(strengthen)+    -- * Transforming extensible products+  , remap+  ) where++import Control.Monad (unless)+import Control.Exception (catch, SomeException)+import GHC.Exts (Any)+import Unsafe.Coerce (unsafeCoerce)+import Data.Vector (Vector)+import qualified Data.Vector as V+import GHC.TypeLits (KnownNat, type (+), type (-), natVal, type (<=))+import Data.Proxy (Proxy(Proxy))++-- | An extensible product type+data Prod (xs :: [*]) = UnsafeProd { unProd :: Vector Any }++type role Prod representational++-- | A type family for computing the index of a type in a list of types.+type family IndexIn (x :: k) (xs :: [k]) where+  IndexIn x (x ': xs) = 0+  IndexIn x (y ': xs) = 1 + IndexIn x xs++-- | A type family for computing the length of a type level list+type family Length (xs :: [k]) where+  Length '[] = 0+  Length (x ': xs) = 1 + Length xs++type family Tail n xs where+  Tail 0 xs = xs+  Tail n (x ': xs) = Tail (n - 1) xs++type family Init n xs where+  Init 0 xs = '[]+  Init n (x ': xs) = x ': Init (n - 1) xs++-- | A class that is used for convenience in order to make certain type+-- signatures read more clearly.+class KnownNat (x `IndexIn` xs) => x `HasIndexIn` xs+instance KnownNat (x `IndexIn` xs) => x `HasIndexIn` xs++-- | Computes the index of the given type in the given type level list.+index :: forall x xs. x `HasIndexIn` xs => Word+index = fromInteger $ natVal (Proxy @(IndexIn x xs))+{-# INLINE CONLIKE index #-}++-- | Extract a value at a particular index+extract :: forall x xs. x `HasIndexIn` xs => Prod xs -> x+extract (UnsafeProd v) = unsafeCoerce $ v V.! fromIntegral (index @x @xs)+{-# INLINE CONLIKE extract #-}++-- | Takes the tail of a product after the nth element.+tailN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Tail n xs)+tailN (UnsafeProd v) = UnsafeProd $ V.slice n (V.length v - n) v+  where+    n = fromInteger $ natVal (Proxy @n)+{-# INLINE CONLIKE tailN #-}++-- | Takes the initial length n segment of a product.+initN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Init n xs)+initN (UnsafeProd v) = UnsafeProd $ V.slice 0 n v+  where+    n = fromInteger $ natVal (Proxy @n)+{-# INLINE CONLIKE initN #-}++-- | Drop the first element of a product. Sometimes needed for better type+-- inference and less piping around of constraints.+dropFirst :: forall x xs. Prod (x ': xs) -> Prod xs+dropFirst (UnsafeProd v) = UnsafeProd $ V.slice 1 (V.length v - 1) v+++type family (<>) (xs :: [k]) (ys :: [k]) :: [k] where+  '[] <> ys = ys+  (x ': xs) <> ys = x ': (xs <> ys)+combine :: forall xs ys. Prod xs -> Prod ys -> Prod (xs <> ys)+combine (UnsafeProd p) (UnsafeProd q) = UnsafeProd (p V.++ q)+{-# INLINE CONLIKE combine #-}++-- | Type family for replacing one type in a type level list with another+type family Replace x y xs where+  Replace x y (x ': xs) = y ': xs+  Replace x y (z ': xs) = z ': Replace x y xs++-- | Replaces one type with another via a function+remap :: forall x y xs. x `HasIndexIn` xs => (x -> y) -> Prod xs -> Prod (Replace x y xs)+remap f (UnsafeProd v) = UnsafeProd (update `V.imap` v) where+  update :: Int -> Any -> Any+  update (fromIntegral -> n) a+    | n == index @x @xs = unsafeCoerce $ f $ unsafeCoerce a+    | otherwise = a+  {-# INLINE CONLIKE update #-}+{-# INLINE CONLIKE remap #-}++-- | This is a reified pattern match on an extensible product+type family Consumer xs r where+  Consumer '[] r = r+  Consumer (x ': xs) r = x -> Consumer xs r++-- | A typeclass that is useful to define the scott encoding/decoding for+-- extensible products.+class Consume xs where+  consume :: forall r. Prod xs -> Consumer xs r -> r+  produce :: (forall r. Consumer xs r -> r) -> Prod xs+  extend1 :: x -> Consumer xs (Prod (x ': xs))+  cmap :: (r -> r') -> Consumer xs r -> Consumer xs r' ++instance Consume '[] where+  consume = flip const+  {-# INLINE CONLIKE consume #-}+  produce x = UnsafeProd V.empty+  {-# INLINE CONLIKE produce #-}+  extend1 x = UnsafeProd (V.singleton (unsafeCoerce x))+  {-# INLINE CONLIKE extend1 #-}+  cmap f x = f x+  {-# INLINE CONLIKE cmap #-}++instance Consume xs => Consume (x ': xs) where+  consume (UnsafeProd v) g = consume @xs (UnsafeProd (V.tail v)) $ g (unsafeCoerce $ v V.! 0)+  {-# INLINE CONLIKE consume #-}+  produce g = g (extend1 @xs)+  {-# INLINE CONLIKE produce #-}+  cmap f = fmap (cmap @xs f)+  {-# INLINE CONLIKE cmap #-}+  extend1 (x1 :: x1) x = cmap @xs @(Prod (x ': xs)) @(Prod (x1 ': x ': xs)) (UnsafeProd . (V.singleton (unsafeCoerce x1) V.++) . unProd) (extend1 @xs x)+  {-# INLINE CONLIKE extend1 #-}++instance Eq (Prod '[]) where+  _ == _ = True+  {-# INLINE CONLIKE (==) #-}++instance (Eq x, Eq (Prod xs)) => Eq (Prod (x ': xs)) where+  px@(UnsafeProd x) == py@(UnsafeProd y) = unsafeCoerce @_ @x (x V.! 0) == unsafeCoerce @_ @x (y V.! 0) && dropFirst px == dropFirst py+  {-# INLINE CONLIKE (==) #-}++-- | A typeclass to rearrange and possibly remove things from a product.+class Strengthen xs ys where+  strengthen :: Prod xs -> Prod ys+instance (Strengthen xs ys, y `HasIndexIn` xs) => Strengthen xs (y ': ys) where+  strengthen p = UnsafeProd $ V.singleton (unsafeCoerce $ unProd p V.! fromIntegral (index @y @xs)) <> unProd (strengthen @xs @ys p)+  {-# INLINE CONLIKE strengthen #-}+instance Strengthen xs '[] where+  strengthen = const (UnsafeProd V.empty)+  {-# INLINE CONLIKE strengthen #-}

@@ -0,0 +1,207 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE DataKinds #-}+{- |+Module: Data.Summer+Copyright: (c) Samuel Schlesinger 2020+License: MIT+Maintainer: sgschlesinger@gmail.com+Stability: experimental+Portability: non-portable+Description: Extensible sums+-}+module Data.Summer+  ( -- * The extensible sum type and its associated pattern for convenience+    Sum+  , pattern Inj+  , tag+  -- * Construction and Deconstruction+  , inject+  , inspect+  , consider+  , Match(match, override, unmatch)+  -- * Type families+  , TagIn+  , HasTagIn+  , Delete+  , HaveSameTagsIn+  , Matcher+  -- * Weakening extensible sums+  , Weaken(weaken)+  , noOpWeaken+  -- * Transforming extensible sums+  , inmap+  , smap+  ) where++import Control.Exception (catch, SomeException)+import Unsafe.Coerce (unsafeCoerce)+import GHC.Exts (Any, Constraint)+import GHC.TypeLits (Nat, KnownNat, natVal, type (+))+import Data.Proxy (Proxy(Proxy))+import Data.Kind (Type)+import Control.Monad (unless)++-- | The extensible sum type, allowing inhabitants to be of any of the+-- types in the given type list.+data Sum (xs :: [*]) = UnsafeInj {-# UNPACK #-} !Word Any++type role Sum representational++-- | A pattern to match on for convenience. Without this, the user facing+-- interface is rather baroque.+pattern Inj :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs+pattern Inj x <- (inspect -> Just x)+  where+    Inj x = inject x++-- | A type family for computing the tag of a given type in an extensible+-- sum. In practice, this means computing the first index of the given type in+-- the list.+type family TagIn (x :: k) (xs :: [k]) where+  TagIn x (x ': xs) = 0+  TagIn x (y ': xs) = 1 + TagIn x xs++-- | A class that is used for convenience in order to make certain+-- type signatures read more clearly.+class KnownNat (x `TagIn` xs) => x `HasTagIn` xs+instance KnownNat (x `TagIn` xs) => x `HasTagIn` xs++-- | Computes the tag of the given type in the given type level list.+tag :: forall x xs. x `HasTagIn` xs => Word+tag = fromInteger $ natVal (Proxy @(TagIn x xs))+{-# INLINE CONLIKE tag #-}++-- | Injects a type into the extensible sum.+inject :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs+inject x = UnsafeInj (tag @x @xs) (unsafeCoerce x)+{-# INLINE CONLIKE inject #-}++-- | Inspects an extensible sum for a particular type.+inspect :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Maybe x+inspect (UnsafeInj tag' x) = if tag @x @xs == tag' then Just (unsafeCoerce x) else Nothing+{-# INLINE CONLIKE inspect #-}++-- | A type family for deleting the given type from a list+type family Delete (x :: k) (xs :: [k]) :: [k] where+  Delete x (x ': xs) = xs+  Delete x (y ': xs) = y ': Delete x xs+  Delete x '[] = '[]++-- | Consider a certain type, discarding it as an option if it is not the+-- correct one.+consider :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Either (Sum (Delete x xs)) x+consider (UnsafeInj tag' x) =+  if tag' == tag @x @xs+    then Right (unsafeCoerce x)+    else Left (UnsafeInj (if tag' >= tag @x @xs then tag' - 1 else tag') x)+{-# INLINE CONLIKE consider #-}++-- | Consider the first type in the list of possibilities, a useful+-- specialization for type inference.+considerFirst :: forall x xs. Sum (x ': xs) -> Either (Sum xs) x+considerFirst = consider+{-# INLINE CONLIKE considerFirst #-}++-- | Transforms one type in the sum into another.+inmap :: forall x y xs. (x `HasTagIn` xs, y `HasTagIn` xs) => (x -> y) -> Sum xs -> Sum xs+inmap f uv@(UnsafeInj tag' x) = if tag' == tag @x @xs then UnsafeInj (tag @y @xs) (unsafeCoerce (f (unsafeCoerce x))) else uv+{-# INLINE CONLIKE inmap #-}++-- | Transform one type in one sum into another type in another sum.+smap :: forall x y xs ys. (Weaken xs ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys+smap f uv@(UnsafeInj tag' x) = if tag' == tag @x @xs then UnsafeInj (tag @y @ys) (unsafeCoerce (f (unsafeCoerce x))) else weaken uv+{-# INLINE CONLIKE smap #-}++-- | A class which checks that every type has the same tag in the first+-- list as the second. In other words, checks if the first list is a prefix+-- of the other.+class HaveSameTagsIn xs ys+instance {-# OVERLAPPABLE #-} HaveSameTagsIn '[] ys+instance {-# OVERLAPPABLE #-} HaveSameTagsIn xs ys => HaveSameTagsIn (x ': xs) (x ': ys)++-- | A free version of weakening, where all you're doing is adding+-- more possibilities at exclusively higher tags.+noOpWeaken :: forall xs ys. (xs `HaveSameTagsIn` ys) => Sum xs -> Sum ys+noOpWeaken = unsafeCoerce+{-# INLINE CONLIKE noOpWeaken #-}++unsafeForget :: Sum (x ': xs) -> Sum xs+unsafeForget (UnsafeInj tag' x) = UnsafeInj (tag' - 1) x+{-# INLINE CONLIKE unsafeForget #-}++-- | Testing extensible sums for equality.+instance (Eq (Sum xs), Eq x) => Eq (Sum (x ': xs)) where+  uv@(UnsafeInj tag' x) == uv'@(UnsafeInj tag'' x')+    | tag' == tag'' =+        if tag' == 0+          then unsafeCoerce @_ @x x == unsafeCoerce @_ @x x'+          else unsafeForget uv == unsafeForget uv'+    | otherwise = False+  {-# INLINE CONLIKE (==) #-}+instance Eq (Sum '[]) where+  (==) = error "(==) base case: impossible by construction"++-- | Transforming one sum into a sum which contains all of the same types+class Weaken xs ys where+  weaken :: Sum xs -> Sum ys+instance (Weaken xs ys, x `HasTagIn` ys) => Weaken (x ': xs) ys where+  weaken uv@(UnsafeInj tag' x) =+    if tag' == 0+      then UnsafeInj (tag @x @ys) x+      else let UnsafeInj tag'' _ = weaken @xs @ys (unsafeForget uv) in UnsafeInj tag'' x+  {-# INLINE CONLIKE weaken #-}+instance Weaken '[] ys where+  weaken = error "weaken base case: impossible by construction"+  {-# INLINE CONLIKE weaken #-}++-- | The scott encoding of an extensible sum+type family Matcher xs r :: Type where+  Matcher '[] r = r+  Matcher (x ': xs) r = (x -> r) -> Matcher xs r++-- | A typeclass for scott encoding extensible sums+class Match xs where+  match :: forall r. Sum xs -> Matcher xs r+  unmatch :: (forall r. Matcher xs r) -> Sum xs+  override :: forall r. r -> Matcher xs r -> Matcher xs r+instance Match '[] where+  match = error "match base case: impossible by construction"+  {-# INLINE CONLIKE match #-}+  unmatch = id+  {-# INLINE CONLIKE unmatch #-}+  override = const+  {-# INLINE CONLIKE override #-}+instance (Unmatch xs (x ': xs), Match xs) => Match (x ': xs) where+  match :: forall r. Sum (x ': xs) -> (x -> r) -> Matcher xs r+  match uv@(UnsafeInj tag' x) f =+    if tag' == 0+      then override @xs @r (f (unsafeCoerce x)) $ match @xs @r (unsafeForget uv)+      else match @xs @r (unsafeForget uv)+  {-# INLINE CONLIKE match #-}+  unmatch :: (forall r. (x -> r) -> Matcher xs r) -> Sum (x ': xs)+  unmatch g = unmatchGo @xs $ g @(Sum (x ': xs)) (UnsafeInj 0 . unsafeCoerce @x)+  {-# INLINE CONLIKE unmatch #-}+  override r m = fmap (override @xs r) m+  {-# INLINE CONLIKE override #-}++class Unmatch xs ys where+  unmatchGo :: Matcher xs (Sum ys) -> Sum ys+instance Unmatch '[] ys where+  unmatchGo = id+instance (Unmatch xs ys, x `HasTagIn` ys) => Unmatch (x ': xs) ys where+  unmatchGo f = unmatchGo @xs (f (UnsafeInj (tag @x @ys) . unsafeCoerce @x))

@@ -0,0 +1,32 @@+cabal-version:       2.4+name:                summer+version:             0.1.0.0+synopsis:            An implementation of extensible products and sums+description:         An implementation of extensible products and sums.+license:             MIT+license-file:        LICENSE+author:              Samuel Schlesinger+maintainer:          sgschlesinger@gmail.com+copyright:           2020 Samuel Schlesinger+category:            Data+extra-source-files:  CHANGELOG.md, README.md+build-type:          Simple+extra-source-files:  CHANGELOG.md+tested-with:         GHC ==8.6.3 || ==8.8.3 || ==8.10.1++source-repository head+  type: git+  location: https://github.com/samuelschlesinger/summer++library+  exposed-modules:     Data.Summer, Data.Prodder+  build-depends:       base >=4.12 && <4.15, vector >=0.12+  hs-source-dirs:      src+  default-language:    Haskell2010++test-suite test-summer+  type: exitcode-stdio-1.0+  main-is: Test.hs+  hs-source-dirs: test+  build-depends: base >= 4.12 && <5, summer+  default-language: Haskell2010

@@ -0,0 +1,135 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+module Main (main) where++import Control.Exception+import Control.Monad+import Data.Summer+import Data.Prodder++main :: IO ()+main = sumTest >> prodTest++prodTest :: IO ()+prodTest = catchAndDisplay+  [ indexTest+  , remapTest+  , consumeAndProduceTest+  , extractTest+  , strengthenTest+  , tailNTest+  , initNTest+  ]+  where+    catchAndDisplay (x : xs) = catch @SomeException x print >> catchAndDisplay xs+    catchAndDisplay [] = pure ()+    indexTest = do+      let index' = index @Int @'[Bool, Int]+          index'' = index @Bool @'[Bool, Int]+      unless (index' == 1) $ fail ("Index " <> show index' <> " does not equal 1")+      unless (index'' == 0) $ fail ("Index " <> show index'' <> " does not equal 0")+    remapTest = do+      let x :: Prod '[Int, Bool] = produce (\f -> f 10 True)+      let y = remap ((+ 10000000000000000000000000000) . toInteger @Int) x+      let z = remap not x+      unless (y == produce (\f -> f 10000000000000000000000000010 True)) $ fail "Remapping does not work 1"+      unless (z == produce (\f -> f 10 False)) $ fail "Remapping does not work 2"+    consumeAndProduceTest = do+      let x :: Prod '[Int, Bool] = produce (\f -> f 10 True)+          y :: Bool = consume x (\n b -> n == 10 && b)+      unless y $ fail "Consuming and producing does not work"+    extractTest = do+      let x :: Prod '[Int, Bool] = produce (\f -> f 10 True)+          y :: Bool = extract x+          z :: Int = extract x+      unless (z == 10 && y) $ fail "Extracting does not work"+    strengthenTest = do+      let x :: Prod '[Int, Bool, Float] = produce (\f -> f 10 True 0.1)+          y :: Prod '[Bool, Int, Float] = strengthen x+          z :: Prod '[Bool, Int] = strengthen x+      unless (y == produce (\f -> f True 10 0.1)) $ fail "strengthen doesn't work 1"+      unless (z == produce (\f -> f True 10)) $ fail "strengthen doesn't work 2"+    initNTest = do+      let x :: Prod '[Int, Bool, Char, Float] = produce (\f -> f 10 True 'a' 0.2)+      unless (initN @0 x == produce id) $ fail "tailN does not work 0"+      unless (initN @1 x == produce (\f -> f 10)) $ fail "tailN does not work 1"+      unless (initN @2 x == produce (\f -> f 10 True)) $ fail "tailN does not work 2"+      unless (initN @3 x == produce (\f -> f 10 True 'a')) $ fail "tailN does not work 3"+      unless (initN @4 x == produce (\f -> f 10 True 'a' 0.2)) $ fail "tailN does not work 4"+    tailNTest = do+      let x :: Prod '[Int, Bool, Char, Float] = produce (\f -> f 10 True 'a' 0.2)+      unless (tailN @0 x == x) $ fail "tailN does not work 0"+      unless (tailN @1 x == produce (\f -> f True 'a' 0.2)) $ fail "tailN does not work 1"+      unless (tailN @2 x == produce (\f -> f 'a' 0.2)) $ fail "tailN does not work 2"+      unless (tailN @3 x == produce (\f -> f 0.2)) $ fail "tailN does not work 3"+      unless (tailN @4 x == produce id) $ fail "tailN does not work 3"++sumTest :: IO ()+sumTest = catchAndDisplay+  [ tagTest+  , eqTest+  , noOpWeakenTest+  , weakenTest+  , matchTest+  , considerTest+  , inmapTest+  , smapTest+  , unmatchTest+  ]+  where+    catchAndDisplay (x : xs) = catch @SomeException x print >> catchAndDisplay xs+    catchAndDisplay [] = pure ()+    tagTest = do+      let tag' = tag @Int @'[Bool, Int]+          tag'' = tag @Bool @'[Bool, Int]+      unless (tag' == 1) $ fail ("Tag " <> show tag' <> " does not equal 1")+    eqTest = do+      let x :: Sum '[Int, Bool] = Inj (10 :: Int)+          y :: Sum '[Int, Bool] = Inj True+          z :: Sum '[Int, Bool] = Inj (11 :: Int)+          -- wrap around the alphabet like fromIntegral+          a :: Sum '[Int, Bool] = Inj (10 :: Int)+          b :: Sum '[Int, Bool] = Inj False+          c :: Sum '[Int, Bool] = Inj True+      unless (x /= y) $ fail "10 equals True"+      unless (x /= z) $ fail "10 equals 11"+      unless (x == a) $ fail "10 does not equal 10"+      unless (y /= b) $ fail "True equals False"+      unless (y == c) $ fail "True does not equal True"+    noOpWeakenTest = do+      let x :: Sum '[Int, Bool]  = Inj (10 :: Int)+          y :: Sum '[Int, Bool, Integer] = noOpWeaken x+      unless (y == Inj (10 :: Int)) $ fail "y does not equal Inj 10"+      pure ()+    weakenTest = do+      let x :: Sum '[Int, Bool] = Inj (10 :: Int)+          y :: Sum '[Bool, Int] = weaken x+          z :: Sum '[Integer, Bool, Float, Int] = weaken y+      unless (y == Inj (10 :: Int)) $ fail "y does not equal Inj 10"+      unless (z == Inj (10 :: Int)) $ fail "y does not equal Inj 10"+    matchTest = do+      let x :: Sum '[Int, Bool] = Inj (10 :: Int)+      unless (match x (== 10) id) $ fail "x does not match 10"+    considerTest = do+      let x :: Sum '[Int, Bool] = Inj (10 :: Int)+          y :: Sum '[Int, Bool] = Inj True+      unless (consider @Int x == Right 10) $ fail "x at Int is not considered to be 10"+      unless (consider @Int y == Left (Inj True)) $ fail $ "x is not considered to be Left (Inj True)"+      unless (consider @Bool y == Right True) $ fail "x at Bool is not considered to be Right True"+    inmapTest = do+      let x :: Sum '[Int, Bool] = Inj (10 :: Int)+          y :: Sum '[Int, Bool] = inmap (== (10 :: Int)) x+          z :: Sum '[Int, Bool] = inmap (== True) x+      unless (y == Inj True) $ fail "x did not get mapped to True"+      unless (z == Inj (10 :: Int)) $ fail "x did not get left alone"+    smapTest = do+      let x :: Sum '[Int, Bool] = Inj (10 :: Int)+          y :: Sum '[Bool, Int] = smap (== (10 :: Int)) x+          z :: Sum '[Bool, Int] = smap (== True) x+      unless (y == Inj True) $ fail "x did not get mapped to True"+      unless (z == Inj (10 :: Int)) $ fail "x did not get left alone"+    unmatchTest = do+      let x :: Sum '[Int, Bool] = Inj True+          y = \f g -> f 100+      unless (x == unmatch (match x)) $ fail "match and unmatch are not an inverse pair"