{-# LANGUAGE CPP
, PolyKinds
, DataKinds
, TypeOperators
, GADTs
, TypeFamilies
, Rank2Types
, ScopedTypeVariables
, ConstraintKinds
, MultiParamTypeClasses
, FlexibleInstances
, UndecidableInstances
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.IClasses
(
Show1(..), shows1, showList1
, Show2(..), shows2, showList2
, showListWith
, showTuple
, showParen_0
, showParen_1
, showParen_2
, showParen_01
, showParen_02
, showParen_11
, showParen_12
, showParen_22
, showParen_010
, showParen_011
, showParen_111
, Eq1(..)
, Eq2(..)
, TypeEq(..), symmetry, transitivity, congruence
, JmEq1(..)
, JmEq2(..)
, Functor11(..), Fix11(..), cata11, ana11, hylo11
, Functor12(..)
, Functor21(..)
, Functor22(..)
, Foldable11(..), Lift1(..)
, Foldable12(..)
, Foldable21(..), Lift2(..)
, Foldable22(..)
, Traversable11(..)
, Traversable12(..)
, Traversable21(..)
, Traversable22(..)
, Some1(..)
, Some2(..)
, Pair1(..), fst1, snd1
, Pair2(..), fst2, snd2
, Pointwise(..), PointwiseP(..)
, type (++), eqAppendIdentity, eqAppendAssoc
, List1(..), append1
, List2(..)
, DList1(..), toList1, fromList1, dnil1, dcons1, dsnoc1, dsingleton1, dappend1
, All(..), Holds(..)
) where
import Prelude hiding (id, (.))
import Control.Category (Category(..))
import Unsafe.Coerce (unsafeCoerce)
import GHC.Exts (Constraint)
#if __GLASGOW_HASKELL__ < 710
import Data.Monoid (Monoid(..))
import Control.Applicative
#endif
class Show1 (a :: k -> *) where
{-# MINIMAL showsPrec1 | show1 #-}
showsPrec1 :: Int -> a i -> ShowS
showsPrec1 Int
_ a i
x String
s = a i -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1 a i
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
show1 :: a i -> String
show1 a i
x = a i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => a i -> ShowS
shows1 a i
x String
""
shows1 :: (Show1 a) => a i -> ShowS
shows1 :: a i -> ShowS
shows1 = Int -> a i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
0
showList1 :: (Show1 a) => [a i] -> ShowS
showList1 :: [a i] -> ShowS
showList1 = (a i -> ShowS) -> [a i] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showListWith a i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => a i -> ShowS
shows1
class Show2 (a :: k1 -> k2 -> *) where
{-# MINIMAL showsPrec2 | show2 #-}
showsPrec2 :: Int -> a i j -> ShowS
showsPrec2 Int
_ a i j
x String
s = a i j -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2 a i j
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
show2 :: a i j -> String
show2 a i j
x = a i j -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> ShowS
shows2 a i j
x String
""
shows2 :: (Show2 a) => a i j -> ShowS
shows2 :: a i j -> ShowS
shows2 = Int -> a i j -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
0
showList2 :: Show2 a => [a i j] -> ShowS
showList2 :: [a i j] -> ShowS
showList2 = (a i j -> ShowS) -> [a i j] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showListWith a i j -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> ShowS
shows2
showListWith :: (a -> ShowS) -> [a] -> ShowS
showListWith :: (a -> ShowS) -> [a] -> ShowS
showListWith a -> ShowS
f = [a] -> ShowS
start
where
start :: [a] -> ShowS
start [] String
s = String
"[]" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
start (a
x:[a]
xs) String
s = Char
'[' Char -> ShowS
forall a. a -> [a] -> [a]
: a -> ShowS
f a
x ([a] -> String
go [a]
xs)
where
go :: [a] -> String
go [] = Char
']' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s
go (a
y:[a]
ys) = Char
',' Char -> ShowS
forall a. a -> [a] -> [a]
: a -> ShowS
f a
y ([a] -> String
go [a]
ys)
showTuple :: [ShowS] -> ShowS
showTuple :: [ShowS] -> ShowS
showTuple [ShowS]
ss
= Char -> ShowS
showChar Char
'('
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (ShowS -> ShowS -> ShowS) -> [ShowS] -> ShowS
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ShowS
s ShowS
r -> ShowS
s ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Char -> ShowS
showChar Char
',' ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ShowS
r) [ShowS]
ss
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Char -> ShowS
showChar Char
')'
showParen_0 :: Show a => Int -> String -> a -> ShowS
showParen_0 :: Int -> String -> a -> ShowS
showParen_0 Int
p String
s a
e =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
e
)
showParen_1 :: Show1 a => Int -> String -> a i -> ShowS
showParen_1 :: Int -> String -> a i -> ShowS
showParen_1 Int
p String
s a i
e =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 a i
e
)
showParen_2 :: Show2 a => Int -> String -> a i j -> ShowS
showParen_2 :: Int -> String -> a i j -> ShowS
showParen_2 Int
p String
s a i j
e =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a i j -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
11 a i j
e
)
showParen_01 :: (Show b, Show1 a) => Int -> String -> b -> a i -> ShowS
showParen_01 :: Int -> String -> b -> a i -> ShowS
showParen_01 Int
p String
s b
e1 a i
e2 =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 b
e1
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 a i
e2
)
showParen_02 :: (Show b, Show2 a) => Int -> String -> b -> a i j -> ShowS
showParen_02 :: Int -> String -> b -> a i j -> ShowS
showParen_02 Int
p String
s b
e1 a i j
e2 =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 b
e1
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a i j -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
11 a i j
e2
)
showParen_11 :: (Show1 a, Show1 b) => Int -> String -> a i -> b j -> ShowS
showParen_11 :: Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
s a i
e1 b j
e2 =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 a i
e1
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> b j -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 b j
e2
)
showParen_12 :: (Show1 a, Show2 b) => Int -> String -> a i -> b j l -> ShowS
showParen_12 :: Int -> String -> a i -> b j l -> ShowS
showParen_12 Int
p String
s a i
e1 b j l
e2 =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 a i
e1
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> b j l -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
11 b j l
e2
)
showParen_22 :: (Show2 a, Show2 b) => Int -> String -> a i1 j1 -> b i2 j2 -> ShowS
showParen_22 :: Int -> String -> a i1 j1 -> b i2 j2 -> ShowS
showParen_22 Int
p String
s a i1 j1
e1 b i2 j2
e2 =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a i1 j1 -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
11 a i1 j1
e1
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> b i2 j2 -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
11 b i2 j2
e2
)
showParen_010
:: (Show a, Show1 b, Show c)
=> Int -> String -> a -> b i -> c -> ShowS
showParen_010 :: Int -> String -> a -> b i -> c -> ShowS
showParen_010 Int
p String
s a
e1 b i
e2 c
e3 =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
e1
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> b i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 b i
e2
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> c -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 c
e3
)
showParen_011
:: (Show a, Show1 b, Show1 c)
=> Int -> String -> a -> b i -> c j -> ShowS
showParen_011 :: Int -> String -> a -> b i -> c j -> ShowS
showParen_011 Int
p String
s a
e1 b i
e2 c j
e3 =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
e1
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> b i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 b i
e2
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> c j -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 c j
e3
)
showParen_111
:: (Show1 a, Show1 b, Show1 c)
=> Int -> String -> a i -> b j -> c k -> ShowS
showParen_111 :: Int -> String -> a i -> b j -> c k -> ShowS
showParen_111 Int
p String
s a i
e1 b j
e2 c k
e3 =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
s
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> a i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 a i
e1
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> b j -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 b j
e2
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> c k -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 c k
e3
)
class Eq1 (a :: k -> *) where
eq1 :: a i -> a i -> Bool
class Eq2 (a :: k1 -> k2 -> *) where
eq2 :: a i j -> a i j -> Bool
data TypeEq :: k -> k -> * where
Refl :: TypeEq a a
instance Category TypeEq where
id :: TypeEq a a
id = TypeEq a a
forall k (a :: k). TypeEq a a
Refl
TypeEq b c
Refl . :: TypeEq b c -> TypeEq a b -> TypeEq a c
. TypeEq a b
Refl = TypeEq a c
forall k (a :: k). TypeEq a a
Refl
symmetry :: TypeEq a b -> TypeEq b a
symmetry :: TypeEq a b -> TypeEq b a
symmetry TypeEq a b
Refl = TypeEq b a
forall k (a :: k). TypeEq a a
Refl
transitivity :: TypeEq a b -> TypeEq b c -> TypeEq a c
transitivity :: TypeEq a b -> TypeEq b c -> TypeEq a c
transitivity TypeEq a b
Refl TypeEq b c
Refl = TypeEq a c
forall k (a :: k). TypeEq a a
Refl
congruence :: TypeEq a b -> TypeEq (f a) (f b)
congruence :: TypeEq a b -> TypeEq (f a) (f b)
congruence TypeEq a b
Refl = TypeEq (f a) (f b)
forall k (a :: k). TypeEq a a
Refl
class Eq1 a => JmEq1 (a :: k -> *) where
jmEq1 :: a i -> a j -> Maybe (TypeEq i j)
class Eq2 a => JmEq2 (a :: k1 -> k2 -> *) where
jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
class Functor11 (f :: (k1 -> *) -> k2 -> *) where
fmap11 :: (forall i. a i -> b i) -> f a j -> f b j
class Functor12 (f :: (k1 -> *) -> k2 -> k3 -> *) where
fmap12 :: (forall i. a i -> b i) -> f a j l -> f b j l
class Functor21 (f :: (k1 -> k2 -> *) -> k3 -> *) where
fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j
class Functor22 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where
fmap22 :: (forall h i. a h i -> b h i) -> f a j l -> f b j l
newtype Fix11 (f :: (k -> *) -> k -> *) (i :: k) =
Fix11 { Fix11 f i -> f (Fix11 f) i
unFix11 :: f (Fix11 f) i }
cata11
:: forall f a j
. (Functor11 f)
=> (forall i. f a i -> a i)
-> Fix11 f j -> a j
cata11 :: (forall (i :: k). f a i -> a i) -> Fix11 f j -> a j
cata11 forall (i :: k). f a i -> a i
alg = Fix11 f j -> a j
forall (j' :: k). Fix11 f j' -> a j'
go
where
go :: forall j'. Fix11 f j' -> a j'
go :: Fix11 f j' -> a j'
go = f a j' -> a j'
forall (i :: k). f a i -> a i
alg (f a j' -> a j') -> (Fix11 f j' -> f a j') -> Fix11 f j' -> a j'
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall (j' :: k). Fix11 f j' -> a j') -> f (Fix11 f) j' -> f a j'
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (j' :: k). Fix11 f j' -> a j'
go (f (Fix11 f) j' -> f a j')
-> (Fix11 f j' -> f (Fix11 f) j') -> Fix11 f j' -> f a j'
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Fix11 f j' -> f (Fix11 f) j'
forall k (f :: (k -> *) -> k -> *) (i :: k).
Fix11 f i -> f (Fix11 f) i
unFix11
ana11
:: forall f a j
. (Functor11 f)
=> (forall i. a i -> f a i)
-> a j -> Fix11 f j
ana11 :: (forall (i :: k). a i -> f a i) -> a j -> Fix11 f j
ana11 forall (i :: k). a i -> f a i
coalg = a j -> Fix11 f j
forall (j' :: k). a j' -> Fix11 f j'
go
where
go :: forall j'. a j' -> Fix11 f j'
go :: a j' -> Fix11 f j'
go = f (Fix11 f) j' -> Fix11 f j'
forall k (f :: (k -> *) -> k -> *) (i :: k).
f (Fix11 f) i -> Fix11 f i
Fix11 (f (Fix11 f) j' -> Fix11 f j')
-> (a j' -> f (Fix11 f) j') -> a j' -> Fix11 f j'
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall (j' :: k). a j' -> Fix11 f j') -> f a j' -> f (Fix11 f) j'
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (j' :: k). a j' -> Fix11 f j'
go (f a j' -> f (Fix11 f) j')
-> (a j' -> f a j') -> a j' -> f (Fix11 f) j'
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a j' -> f a j'
forall (i :: k). a i -> f a i
coalg
hylo11
:: forall f a b j
. (Functor11 f)
=> (forall i. a i -> f a i)
-> (forall i. f b i -> b i)
-> a j
-> b j
hylo11 :: (forall (i :: k2). a i -> f a i)
-> (forall (i :: k2). f b i -> b i) -> a j -> b j
hylo11 forall (i :: k2). a i -> f a i
coalg forall (i :: k2). f b i -> b i
alg = a j -> b j
forall (j' :: k2). a j' -> b j'
go
where
go :: forall j'. a j' -> b j'
go :: a j' -> b j'
go = f b j' -> b j'
forall (i :: k2). f b i -> b i
alg (f b j' -> b j') -> (a j' -> f b j') -> a j' -> b j'
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall (j' :: k2). a j' -> b j') -> f a j' -> f b j'
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (j' :: k2). a j' -> b j'
go (f a j' -> f b j') -> (a j' -> f a j') -> a j' -> f b j'
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a j' -> f a j'
forall (i :: k2). a i -> f a i
coalg
class Functor11 f => Foldable11 (f :: (k1 -> *) -> k2 -> *) where
{-# MINIMAL fold11 | foldMap11 #-}
fold11 :: (Monoid m) => f (Lift1 m) i -> m
fold11 = (forall (i :: k1). Lift1 m i -> m) -> f (Lift1 m) i -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
(j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (i :: k1). Lift1 m i -> m
forall a k (i :: k). Lift1 a i -> a
unLift1
foldMap11 :: (Monoid m) => (forall i. a i -> m) -> f a j -> m
foldMap11 forall (i :: k1). a i -> m
f = f (Lift1 m) j -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (i :: k2).
(Foldable11 f, Monoid m) =>
f (Lift1 m) i -> m
fold11 (f (Lift1 m) j -> m) -> (f a j -> f (Lift1 m) j) -> f a j -> m
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall (i :: k1). a i -> Lift1 m i) -> f a j -> f (Lift1 m) j
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 (m -> Lift1 m i
forall k a (i :: k). a -> Lift1 a i
Lift1 (m -> Lift1 m i) -> (a i -> m) -> a i -> Lift1 m i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a i -> m
forall (i :: k1). a i -> m
f)
class Functor12 f => Foldable12 (f :: (k1 -> *) -> k2 -> k3 -> *) where
{-# MINIMAL fold12 | foldMap12 #-}
fold12 :: (Monoid m) => f (Lift1 m) j l -> m
fold12 = (forall (i :: k1). Lift1 m i -> m) -> f (Lift1 m) j l -> m
forall k1 k2 k3 (f :: (k1 -> *) -> k2 -> k3 -> *) m (a :: k1 -> *)
(j :: k2) (l :: k3).
(Foldable12 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j l -> m
foldMap12 forall (i :: k1). Lift1 m i -> m
forall a k (i :: k). Lift1 a i -> a
unLift1
foldMap12 :: (Monoid m) => (forall i. a i -> m) -> f a j l -> m
foldMap12 forall (i :: k1). a i -> m
f = f (Lift1 m) j l -> m
forall k1 k2 k3 (f :: (k1 -> *) -> k2 -> k3 -> *) m (j :: k2)
(l :: k3).
(Foldable12 f, Monoid m) =>
f (Lift1 m) j l -> m
fold12 (f (Lift1 m) j l -> m)
-> (f a j l -> f (Lift1 m) j l) -> f a j l -> m
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall (i :: k1). a i -> Lift1 m i) -> f a j l -> f (Lift1 m) j l
forall k1 k2 k3 (f :: (k1 -> *) -> k2 -> k3 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2) (l :: k3).
Functor12 f =>
(forall (i :: k1). a i -> b i) -> f a j l -> f b j l
fmap12 (m -> Lift1 m i
forall k a (i :: k). a -> Lift1 a i
Lift1 (m -> Lift1 m i) -> (a i -> m) -> a i -> Lift1 m i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a i -> m
forall (i :: k1). a i -> m
f)
class Functor21 f => Foldable21 (f :: (k1 -> k2 -> *) -> k3 -> *) where
{-# MINIMAL fold21 | foldMap21 #-}
fold21 :: (Monoid m) => f (Lift2 m) j -> m
fold21 = (forall (h :: k1) (i :: k2). Lift2 m h i -> m)
-> f (Lift2 m) j -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (h :: k1) (i :: k2). Lift2 m h i -> m
forall a k1 (i :: k1) k2 (j :: k2). Lift2 a i j -> a
unLift2
foldMap21 :: (Monoid m) => (forall h i. a h i -> m) -> f a j -> m
foldMap21 forall (h :: k1) (i :: k2). a h i -> m
f = f (Lift2 m) j -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m (j :: k3).
(Foldable21 f, Monoid m) =>
f (Lift2 m) j -> m
fold21 (f (Lift2 m) j -> m) -> (f a j -> f (Lift2 m) j) -> f a j -> m
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall (h :: k1) (i :: k2). a h i -> Lift2 m h i)
-> f a j -> f (Lift2 m) j
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 (m -> Lift2 m h i
forall k1 k2 a (i :: k1) (j :: k2). a -> Lift2 a i j
Lift2 (m -> Lift2 m h i) -> (a h i -> m) -> a h i -> Lift2 m h i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a h i -> m
forall (h :: k1) (i :: k2). a h i -> m
f)
class Functor22 f =>
Foldable22 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
where
{-# MINIMAL fold22 | foldMap22 #-}
fold22 :: (Monoid m) => f (Lift2 m) j l -> m
fold22 = (forall (h :: k1) (i :: k2). Lift2 m h i -> m)
-> f (Lift2 m) j l -> m
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) m
(a :: k1 -> k2 -> *) (j :: k3) (l :: k4).
(Foldable22 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j l -> m
foldMap22 forall (h :: k1) (i :: k2). Lift2 m h i -> m
forall a k1 (i :: k1) k2 (j :: k2). Lift2 a i j -> a
unLift2
foldMap22 :: (Monoid m) => (forall h i. a h i -> m) -> f a j l -> m
foldMap22 forall (h :: k1) (i :: k2). a h i -> m
f = f (Lift2 m) j l -> m
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) m
(j :: k3) (l :: k4).
(Foldable22 f, Monoid m) =>
f (Lift2 m) j l -> m
fold22 (f (Lift2 m) j l -> m)
-> (f a j l -> f (Lift2 m) j l) -> f a j l -> m
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall (h :: k1) (i :: k2). a h i -> Lift2 m h i)
-> f a j l -> f (Lift2 m) j l
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3) (l :: k4).
Functor22 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j l -> f b j l
fmap22 (m -> Lift2 m h i
forall k1 k2 a (i :: k1) (j :: k2). a -> Lift2 a i j
Lift2 (m -> Lift2 m h i) -> (a h i -> m) -> a h i -> Lift2 m h i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a h i -> m
forall (h :: k1) (i :: k2). a h i -> m
f)
class Foldable11 t => Traversable11 (t :: (k1 -> *) -> k2 -> *) where
traverse11
:: Applicative f
=> (forall i. a i -> f (b i))
-> t a j
-> f (t b j)
class Foldable12 t => Traversable12 (t :: (k1 -> *) -> k2 -> k3 -> *) where
traverse12
:: Applicative f
=> (forall i. a i -> f (b i))
-> t a j l
-> f (t b j l)
class Foldable21 t => Traversable21 (t :: (k1 -> k2 -> *) -> k3 -> *) where
traverse21
:: Applicative f
=> (forall h i. a h i -> f (b h i))
-> t a j
-> f (t b j)
class Foldable22 t =>
Traversable22 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
where
traverse22
:: Applicative f
=> (forall h i. a h i -> f (b h i))
-> t a j l
-> f (t b j l)
newtype Lift1 (a :: *) (i :: k) =
Lift1 { Lift1 a i -> a
unLift1 :: a }
deriving (ReadPrec [Lift1 a i]
ReadPrec (Lift1 a i)
Int -> ReadS (Lift1 a i)
ReadS [Lift1 a i]
(Int -> ReadS (Lift1 a i))
-> ReadS [Lift1 a i]
-> ReadPrec (Lift1 a i)
-> ReadPrec [Lift1 a i]
-> Read (Lift1 a i)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall a k (i :: k). Read a => ReadPrec [Lift1 a i]
forall a k (i :: k). Read a => ReadPrec (Lift1 a i)
forall a k (i :: k). Read a => Int -> ReadS (Lift1 a i)
forall a k (i :: k). Read a => ReadS [Lift1 a i]
readListPrec :: ReadPrec [Lift1 a i]
$creadListPrec :: forall a k (i :: k). Read a => ReadPrec [Lift1 a i]
readPrec :: ReadPrec (Lift1 a i)
$creadPrec :: forall a k (i :: k). Read a => ReadPrec (Lift1 a i)
readList :: ReadS [Lift1 a i]
$creadList :: forall a k (i :: k). Read a => ReadS [Lift1 a i]
readsPrec :: Int -> ReadS (Lift1 a i)
$creadsPrec :: forall a k (i :: k). Read a => Int -> ReadS (Lift1 a i)
Read, Int -> Lift1 a i -> ShowS
[Lift1 a i] -> ShowS
Lift1 a i -> String
(Int -> Lift1 a i -> ShowS)
-> (Lift1 a i -> String)
-> ([Lift1 a i] -> ShowS)
-> Show (Lift1 a i)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a k (i :: k). Show a => Int -> Lift1 a i -> ShowS
forall a k (i :: k). Show a => [Lift1 a i] -> ShowS
forall a k (i :: k). Show a => Lift1 a i -> String
showList :: [Lift1 a i] -> ShowS
$cshowList :: forall a k (i :: k). Show a => [Lift1 a i] -> ShowS
show :: Lift1 a i -> String
$cshow :: forall a k (i :: k). Show a => Lift1 a i -> String
showsPrec :: Int -> Lift1 a i -> ShowS
$cshowsPrec :: forall a k (i :: k). Show a => Int -> Lift1 a i -> ShowS
Show, Lift1 a i -> Lift1 a i -> Bool
(Lift1 a i -> Lift1 a i -> Bool)
-> (Lift1 a i -> Lift1 a i -> Bool) -> Eq (Lift1 a i)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a k (i :: k). Eq a => Lift1 a i -> Lift1 a i -> Bool
/= :: Lift1 a i -> Lift1 a i -> Bool
$c/= :: forall a k (i :: k). Eq a => Lift1 a i -> Lift1 a i -> Bool
== :: Lift1 a i -> Lift1 a i -> Bool
$c== :: forall a k (i :: k). Eq a => Lift1 a i -> Lift1 a i -> Bool
Eq, Eq (Lift1 a i)
Eq (Lift1 a i)
-> (Lift1 a i -> Lift1 a i -> Ordering)
-> (Lift1 a i -> Lift1 a i -> Bool)
-> (Lift1 a i -> Lift1 a i -> Bool)
-> (Lift1 a i -> Lift1 a i -> Bool)
-> (Lift1 a i -> Lift1 a i -> Bool)
-> (Lift1 a i -> Lift1 a i -> Lift1 a i)
-> (Lift1 a i -> Lift1 a i -> Lift1 a i)
-> Ord (Lift1 a i)
Lift1 a i -> Lift1 a i -> Bool
Lift1 a i -> Lift1 a i -> Ordering
Lift1 a i -> Lift1 a i -> Lift1 a i
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a k (i :: k). Ord a => Eq (Lift1 a i)
forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Bool
forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Ordering
forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Lift1 a i
min :: Lift1 a i -> Lift1 a i -> Lift1 a i
$cmin :: forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Lift1 a i
max :: Lift1 a i -> Lift1 a i -> Lift1 a i
$cmax :: forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Lift1 a i
>= :: Lift1 a i -> Lift1 a i -> Bool
$c>= :: forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Bool
> :: Lift1 a i -> Lift1 a i -> Bool
$c> :: forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Bool
<= :: Lift1 a i -> Lift1 a i -> Bool
$c<= :: forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Bool
< :: Lift1 a i -> Lift1 a i -> Bool
$c< :: forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Bool
compare :: Lift1 a i -> Lift1 a i -> Ordering
$ccompare :: forall a k (i :: k). Ord a => Lift1 a i -> Lift1 a i -> Ordering
$cp1Ord :: forall a k (i :: k). Ord a => Eq (Lift1 a i)
Ord)
instance Show a => Show1 (Lift1 a) where
showsPrec1 :: Int -> Lift1 a i -> ShowS
showsPrec1 Int
p (Lift1 a
x) = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
x
show1 :: Lift1 a i -> String
show1 (Lift1 a
x) = a -> String
forall a. Show a => a -> String
show a
x
instance Eq a => Eq1 (Lift1 a) where
eq1 :: Lift1 a i -> Lift1 a i -> Bool
eq1 (Lift1 a
a) (Lift1 a
b) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
newtype Lift2 (a :: *) (i :: k1) (j :: k2) =
Lift2 { Lift2 a i j -> a
unLift2 :: a }
deriving (ReadPrec [Lift2 a i j]
ReadPrec (Lift2 a i j)
Int -> ReadS (Lift2 a i j)
ReadS [Lift2 a i j]
(Int -> ReadS (Lift2 a i j))
-> ReadS [Lift2 a i j]
-> ReadPrec (Lift2 a i j)
-> ReadPrec [Lift2 a i j]
-> Read (Lift2 a i j)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall a k1 (i :: k1) k2 (j :: k2).
Read a =>
ReadPrec [Lift2 a i j]
forall a k1 (i :: k1) k2 (j :: k2).
Read a =>
ReadPrec (Lift2 a i j)
forall a k1 (i :: k1) k2 (j :: k2).
Read a =>
Int -> ReadS (Lift2 a i j)
forall a k1 (i :: k1) k2 (j :: k2). Read a => ReadS [Lift2 a i j]
readListPrec :: ReadPrec [Lift2 a i j]
$creadListPrec :: forall a k1 (i :: k1) k2 (j :: k2).
Read a =>
ReadPrec [Lift2 a i j]
readPrec :: ReadPrec (Lift2 a i j)
$creadPrec :: forall a k1 (i :: k1) k2 (j :: k2).
Read a =>
ReadPrec (Lift2 a i j)
readList :: ReadS [Lift2 a i j]
$creadList :: forall a k1 (i :: k1) k2 (j :: k2). Read a => ReadS [Lift2 a i j]
readsPrec :: Int -> ReadS (Lift2 a i j)
$creadsPrec :: forall a k1 (i :: k1) k2 (j :: k2).
Read a =>
Int -> ReadS (Lift2 a i j)
Read, Int -> Lift2 a i j -> ShowS
[Lift2 a i j] -> ShowS
Lift2 a i j -> String
(Int -> Lift2 a i j -> ShowS)
-> (Lift2 a i j -> String)
-> ([Lift2 a i j] -> ShowS)
-> Show (Lift2 a i j)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a k1 (i :: k1) k2 (j :: k2).
Show a =>
Int -> Lift2 a i j -> ShowS
forall a k1 (i :: k1) k2 (j :: k2).
Show a =>
[Lift2 a i j] -> ShowS
forall a k1 (i :: k1) k2 (j :: k2). Show a => Lift2 a i j -> String
showList :: [Lift2 a i j] -> ShowS
$cshowList :: forall a k1 (i :: k1) k2 (j :: k2).
Show a =>
[Lift2 a i j] -> ShowS
show :: Lift2 a i j -> String
$cshow :: forall a k1 (i :: k1) k2 (j :: k2). Show a => Lift2 a i j -> String
showsPrec :: Int -> Lift2 a i j -> ShowS
$cshowsPrec :: forall a k1 (i :: k1) k2 (j :: k2).
Show a =>
Int -> Lift2 a i j -> ShowS
Show, Lift2 a i j -> Lift2 a i j -> Bool
(Lift2 a i j -> Lift2 a i j -> Bool)
-> (Lift2 a i j -> Lift2 a i j -> Bool) -> Eq (Lift2 a i j)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a k1 (i :: k1) k2 (j :: k2).
Eq a =>
Lift2 a i j -> Lift2 a i j -> Bool
/= :: Lift2 a i j -> Lift2 a i j -> Bool
$c/= :: forall a k1 (i :: k1) k2 (j :: k2).
Eq a =>
Lift2 a i j -> Lift2 a i j -> Bool
== :: Lift2 a i j -> Lift2 a i j -> Bool
$c== :: forall a k1 (i :: k1) k2 (j :: k2).
Eq a =>
Lift2 a i j -> Lift2 a i j -> Bool
Eq, Eq (Lift2 a i j)
Eq (Lift2 a i j)
-> (Lift2 a i j -> Lift2 a i j -> Ordering)
-> (Lift2 a i j -> Lift2 a i j -> Bool)
-> (Lift2 a i j -> Lift2 a i j -> Bool)
-> (Lift2 a i j -> Lift2 a i j -> Bool)
-> (Lift2 a i j -> Lift2 a i j -> Bool)
-> (Lift2 a i j -> Lift2 a i j -> Lift2 a i j)
-> (Lift2 a i j -> Lift2 a i j -> Lift2 a i j)
-> Ord (Lift2 a i j)
Lift2 a i j -> Lift2 a i j -> Bool
Lift2 a i j -> Lift2 a i j -> Ordering
Lift2 a i j -> Lift2 a i j -> Lift2 a i j
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a k1 (i :: k1) k2 (j :: k2). Ord a => Eq (Lift2 a i j)
forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Bool
forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Ordering
forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Lift2 a i j
min :: Lift2 a i j -> Lift2 a i j -> Lift2 a i j
$cmin :: forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Lift2 a i j
max :: Lift2 a i j -> Lift2 a i j -> Lift2 a i j
$cmax :: forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Lift2 a i j
>= :: Lift2 a i j -> Lift2 a i j -> Bool
$c>= :: forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Bool
> :: Lift2 a i j -> Lift2 a i j -> Bool
$c> :: forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Bool
<= :: Lift2 a i j -> Lift2 a i j -> Bool
$c<= :: forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Bool
< :: Lift2 a i j -> Lift2 a i j -> Bool
$c< :: forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Bool
compare :: Lift2 a i j -> Lift2 a i j -> Ordering
$ccompare :: forall a k1 (i :: k1) k2 (j :: k2).
Ord a =>
Lift2 a i j -> Lift2 a i j -> Ordering
$cp1Ord :: forall a k1 (i :: k1) k2 (j :: k2). Ord a => Eq (Lift2 a i j)
Ord)
instance Show a => Show2 (Lift2 a) where
showsPrec2 :: Int -> Lift2 a i j -> ShowS
showsPrec2 Int
p (Lift2 a
x) = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
x
show2 :: Lift2 a i j -> String
show2 (Lift2 a
x) = a -> String
forall a. Show a => a -> String
show a
x
instance Show a => Show1 (Lift2 a i) where
showsPrec1 :: Int -> Lift2 a i i -> ShowS
showsPrec1 Int
p (Lift2 a
x) = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
x
show1 :: Lift2 a i i -> String
show1 (Lift2 a
x) = a -> String
forall a. Show a => a -> String
show a
x
instance Eq a => Eq2 (Lift2 a) where
eq2 :: Lift2 a i j -> Lift2 a i j -> Bool
eq2 (Lift2 a
a) (Lift2 a
b) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
instance Eq a => Eq1 (Lift2 a i) where
eq1 :: Lift2 a i i -> Lift2 a i i -> Bool
eq1 (Lift2 a
a) (Lift2 a
b) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
data Pointwise (f :: k0 -> *) (g :: k1 -> *) (x :: k0) (y :: k1) where
Pw :: f x -> g y -> Pointwise f g x y
data PointwiseP (f :: k0 -> *) (g :: k1 -> *) (xy :: (k0, k1)) where
PwP :: f x -> g y -> PointwiseP f g '(x,y)
data Some1 (a :: k -> *)
= forall i. Some1 !(a i)
instance Show1 a => Show (Some1 a) where
showsPrec :: Int -> Some1 a -> ShowS
showsPrec Int
p (Some1 a i
x) = Int -> String -> a i -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"Some1" a i
x
instance JmEq1 a => Eq (Some1 a) where
Some1 a i
x == :: Some1 a -> Some1 a -> Bool
== Some1 a i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (a i -> a i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 a i
x a i
y)
data Some2 (a :: k1 -> k2 -> *)
= forall i j. Some2 !(a i j)
instance Show2 a => Show (Some2 a) where
showsPrec :: Int -> Some2 a -> ShowS
showsPrec Int
p (Some2 a i j
x) = Int -> String -> a i j -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> String -> a i j -> ShowS
showParen_2 Int
p String
"Some2" a i j
x
instance JmEq2 a => Eq (Some2 a) where
Some2 a i j
x == :: Some2 a -> Some2 a -> Bool
== Some2 a i j
y = Bool
-> ((TypeEq i i, TypeEq j j) -> Bool)
-> Maybe (TypeEq i i, TypeEq j j)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> (TypeEq i i, TypeEq j j) -> Bool
forall a b. a -> b -> a
const Bool
True) (a i j -> a i j -> Maybe (TypeEq i i, TypeEq j j)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
(j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 a i j
x a i j
y)
data Pair1 (a :: k -> *) (b :: k -> *) (i :: k) =
Pair1 (a i) (b i)
fst1 :: Pair1 a b i -> a i
fst1 :: Pair1 a b i -> a i
fst1 (Pair1 a i
x b i
_) = a i
x
snd1 :: Pair1 a b i -> b i
snd1 :: Pair1 a b i -> b i
snd1 (Pair1 a i
_ b i
y) = b i
y
instance (Show1 a, Show1 b) => Show1 (Pair1 a b) where
showsPrec1 :: Int -> Pair1 a b i -> ShowS
showsPrec1 Int
p (Pair1 a i
x b i
y) = Int -> String -> a i -> b i -> ShowS
forall k k (a :: k -> *) (b :: k -> *) (i :: k) (j :: k).
(Show1 a, Show1 b) =>
Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
"Pair1" a i
x b i
y
instance (Show1 a, Show1 b) => Show (Pair1 a b i) where
showsPrec :: Int -> Pair1 a b i -> ShowS
showsPrec = Int -> Pair1 a b i -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Pair1 a b i -> String
show = Pair1 a b i -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
data Pair2 (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (i :: k1) (j :: k2) =
Pair2 (a i j) (b i j)
fst2 :: Pair2 a b i j -> a i j
fst2 :: Pair2 a b i j -> a i j
fst2 (Pair2 a i j
x b i j
_) = a i j
x
snd2 :: Pair2 a b i j -> b i j
snd2 :: Pair2 a b i j -> b i j
snd2 (Pair2 a i j
_ b i j
y) = b i j
y
instance (Show2 a, Show2 b) => Show2 (Pair2 a b) where
showsPrec2 :: Int -> Pair2 a b i j -> ShowS
showsPrec2 Int
p (Pair2 a i j
x b i j
y) = Int -> String -> a i j -> b i j -> ShowS
forall k1 k2 k1 k2 (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *)
(i1 :: k1) (j1 :: k2) (i2 :: k1) (j2 :: k2).
(Show2 a, Show2 b) =>
Int -> String -> a i1 j1 -> b i2 j2 -> ShowS
showParen_22 Int
p String
"Pair2" a i j
x b i j
y
instance (Show2 a, Show2 b) => Show1 (Pair2 a b i) where
showsPrec1 :: Int -> Pair2 a b i i -> ShowS
showsPrec1 = Int -> Pair2 a b i i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2
show1 :: Pair2 a b i i -> String
show1 = Pair2 a b i i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2
instance (Show2 a, Show2 b) => Show (Pair2 a b i j) where
showsPrec :: Int -> Pair2 a b i j -> ShowS
showsPrec = Int -> Pair2 a b i j -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Pair2 a b i j -> String
show = Pair2 a b i j -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)
eqAppendIdentity :: proxy xs -> TypeEq xs (xs ++ '[])
eqAppendIdentity :: proxy xs -> TypeEq xs (xs ++ '[])
eqAppendIdentity proxy xs
_ = TypeEq Any Any -> TypeEq xs (xs ++ '[])
forall a b. a -> b
unsafeCoerce TypeEq Any Any
forall k (a :: k). TypeEq a a
Refl
eqAppendAssoc
:: proxy1 xs
-> proxy2 ys
-> proxy3 zs
-> TypeEq ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
eqAppendAssoc :: proxy1 xs
-> proxy2 ys
-> proxy3 zs
-> TypeEq ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
eqAppendAssoc proxy1 xs
_ proxy2 ys
_ proxy3 zs
_ = TypeEq Any Any -> TypeEq ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
forall a b. a -> b
unsafeCoerce TypeEq Any Any
forall k (a :: k). TypeEq a a
Refl
infixr 5 `Cons1`
data List1 :: (k -> *) -> [k] -> * where
Nil1 :: List1 a '[]
Cons1 :: a x -> List1 a xs -> List1 a (x ': xs)
append1 :: List1 a xs -> List1 a ys -> List1 a (xs ++ ys)
append1 :: List1 a xs -> List1 a ys -> List1 a (xs ++ ys)
append1 List1 a xs
Nil1 List1 a ys
ys = List1 a ys
List1 a (xs ++ ys)
ys
append1 (Cons1 a x
x List1 a xs
xs) List1 a ys
ys = a x -> List1 a (xs ++ ys) -> List1 a (x : (xs ++ ys))
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 a x
x (List1 a xs -> List1 a ys -> List1 a (xs ++ ys)
forall k (a :: k -> *) (xs :: [k]) (ys :: [k]).
List1 a xs -> List1 a ys -> List1 a (xs ++ ys)
append1 List1 a xs
xs List1 a ys
ys)
instance Show1 a => Show1 (List1 a) where
showsPrec1 :: Int -> List1 a i -> ShowS
showsPrec1 Int
_ List1 a i
Nil1 = String -> ShowS
showString String
"Nil1"
showsPrec1 Int
p (Cons1 a x
x List1 a xs
xs) = Int -> String -> a x -> List1 a xs -> ShowS
forall k k (a :: k -> *) (b :: k -> *) (i :: k) (j :: k).
(Show1 a, Show1 b) =>
Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
"Cons1" a x
x List1 a xs
xs
instance Show1 a => Show (List1 a xs) where
showsPrec :: Int -> List1 a xs -> ShowS
showsPrec = Int -> List1 a xs -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: List1 a xs -> String
show = List1 a xs -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance JmEq1 a => JmEq1 (List1 a) where
jmEq1 :: List1 a i -> List1 a j -> Maybe (TypeEq i j)
jmEq1 List1 a i
Nil1 List1 a j
Nil1 = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 (Cons1 a x
x List1 a xs
xs) (Cons1 a x
y List1 a xs
ys) =
a x -> a x -> Maybe (TypeEq x x)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 a x
x a x
y Maybe (TypeEq x x)
-> (TypeEq x x -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq x x
Refl ->
List1 a xs -> List1 a xs -> Maybe (TypeEq xs xs)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 List1 a xs
xs List1 a xs
ys Maybe (TypeEq xs xs)
-> (TypeEq xs xs -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq xs xs
Refl ->
TypeEq (x : xs) (x : xs) -> Maybe (TypeEq (x : xs) (x : xs))
forall a. a -> Maybe a
Just TypeEq (x : xs) (x : xs)
forall k (a :: k). TypeEq a a
Refl
jmEq1 List1 a i
_ List1 a j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Eq1 a => Eq1 (List1 a) where
eq1 :: List1 a i -> List1 a i -> Bool
eq1 List1 a i
Nil1 List1 a i
Nil1 = Bool
True
eq1 (Cons1 a x
x List1 a xs
xs) (Cons1 a x
y List1 a xs
ys) = a x -> a x -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 a x
x a x
a x
y Bool -> Bool -> Bool
&& List1 a xs -> List1 a xs -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 List1 a xs
xs List1 a xs
List1 a xs
ys
instance Eq1 a => Eq (List1 a xs) where
== :: List1 a xs -> List1 a xs -> Bool
(==) = List1 a xs -> List1 a xs -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Functor11 List1 where
fmap11 :: (forall (i :: k1). a i -> b i) -> List1 a j -> List1 b j
fmap11 forall (i :: k1). a i -> b i
_ List1 a j
Nil1 = List1 b j
forall k (a :: k -> *). List1 a '[]
Nil1
fmap11 forall (i :: k1). a i -> b i
f (Cons1 a x
x List1 a xs
xs) = b x -> List1 b xs -> List1 b (x : xs)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 (a x -> b x
forall (i :: k1). a i -> b i
f a x
x) ((forall (i :: k1). a i -> b i) -> List1 a xs -> List1 b xs
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: k1). a i -> b i
f List1 a xs
xs)
instance Foldable11 List1 where
foldMap11 :: (forall (i :: k1). a i -> m) -> List1 a j -> m
foldMap11 forall (i :: k1). a i -> m
_ List1 a j
Nil1 = m
forall a. Monoid a => a
mempty
foldMap11 forall (i :: k1). a i -> m
f (Cons1 a x
x List1 a xs
xs) = a x -> m
forall (i :: k1). a i -> m
f a x
x m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (forall (i :: k1). a i -> m) -> List1 a xs -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
(j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (i :: k1). a i -> m
f List1 a xs
xs
instance Traversable11 List1 where
traverse11 :: (forall (i :: k1). a i -> f (b i)) -> List1 a j -> f (List1 b j)
traverse11 forall (i :: k1). a i -> f (b i)
_ List1 a j
Nil1 = List1 b '[] -> f (List1 b '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure List1 b '[]
forall k (a :: k -> *). List1 a '[]
Nil1
traverse11 forall (i :: k1). a i -> f (b i)
f (Cons1 a x
x List1 a xs
xs) = b x -> List1 b xs -> List1 b (x : xs)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 (b x -> List1 b xs -> List1 b (x : xs))
-> f (b x) -> f (List1 b xs -> List1 b (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a x -> f (b x)
forall (i :: k1). a i -> f (b i)
f a x
x f (List1 b xs -> List1 b (x : xs))
-> f (List1 b xs) -> f (List1 b (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (i :: k1). a i -> f (b i)) -> List1 a xs -> f (List1 b xs)
forall k1 k2 (t :: (k1 -> *) -> k2 -> *) (f :: * -> *)
(a :: k1 -> *) (b :: k1 -> *) (j :: k2).
(Traversable11 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j -> f (t b j)
traverse11 forall (i :: k1). a i -> f (b i)
f List1 a xs
xs
data List2 :: (k0 -> k1 -> *) -> [k0] -> [k1] -> * where
Nil2 :: List2 f '[] '[]
Cons2 :: f x y -> List2 f xs ys -> List2 f (x ': xs) (y ': ys)
data Holds (c :: k -> Constraint) (x :: k) where
Holds :: c x => Holds c x
class All (c :: k -> Constraint) (xs :: [k]) where
allHolds :: List1 (Holds c) xs
instance All c '[] where allHolds :: List1 (Holds c) '[]
allHolds = List1 (Holds c) '[]
forall k (a :: k -> *). List1 a '[]
Nil1
instance (All c xs, c x)
=> All c (x ': xs) where allHolds :: List1 (Holds c) (x : xs)
allHolds = Holds c x -> List1 (Holds c) xs -> List1 (Holds c) (x : xs)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 Holds c x
forall k (c :: k -> Constraint) (x :: k). c x => Holds c x
Holds List1 (Holds c) xs
forall k (c :: k -> Constraint) (xs :: [k]).
All c xs =>
List1 (Holds c) xs
allHolds
newtype DList1 a xs =
DList1 { DList1 a xs -> forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys)
unDList1 :: forall ys. List1 a ys -> List1 a (xs ++ ys) }
toList1 :: DList1 a xs -> List1 a xs
toList1 :: DList1 a xs -> List1 a xs
toList1 dx :: DList1 a xs
dx@(DList1 forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys)
xs) =
case DList1 a xs -> TypeEq xs (xs ++ '[])
forall k (proxy :: [k] -> *) (xs :: [k]).
proxy xs -> TypeEq xs (xs ++ '[])
eqAppendIdentity DList1 a xs
dx of
TypeEq xs (xs ++ '[])
Refl -> List1 a '[] -> List1 a (xs ++ '[])
forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys)
xs List1 a '[]
forall k (a :: k -> *). List1 a '[]
Nil1
fromList1 :: List1 a xs -> DList1 a xs
fromList1 :: List1 a xs -> DList1 a xs
fromList1 List1 a xs
xs = (forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys))
-> DList1 a xs
forall k (a :: k -> *) (xs :: [k]).
(forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys))
-> DList1 a xs
DList1 (List1 a xs -> List1 a ys -> List1 a (xs ++ ys)
forall k (a :: k -> *) (xs :: [k]) (ys :: [k]).
List1 a xs -> List1 a ys -> List1 a (xs ++ ys)
append1 List1 a xs
xs)
dnil1 :: DList1 a '[]
dnil1 :: DList1 a '[]
dnil1 = (forall (ys :: [k]). List1 a ys -> List1 a ('[] ++ ys))
-> DList1 a '[]
forall k (a :: k -> *) (xs :: [k]).
(forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys))
-> DList1 a xs
DList1 forall (ys :: [k]). List1 a ys -> List1 a ('[] ++ ys)
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
dcons1 :: a x -> DList1 a xs -> DList1 a (x ': xs)
dcons1 :: a x -> DList1 a xs -> DList1 a (x : xs)
dcons1 a x
x (DList1 forall (ys :: [a]). List1 a ys -> List1 a (xs ++ ys)
xs) = (forall (ys :: [a]). List1 a ys -> List1 a ((x : xs) ++ ys))
-> DList1 a (x : xs)
forall k (a :: k -> *) (xs :: [k]).
(forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys))
-> DList1 a xs
DList1 (a x -> List1 a (xs ++ ys) -> List1 a (x : (xs ++ ys))
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 a x
x (List1 a (xs ++ ys) -> List1 a (x : (xs ++ ys)))
-> (List1 a ys -> List1 a (xs ++ ys))
-> List1 a ys
-> List1 a (x : (xs ++ ys))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. List1 a ys -> List1 a (xs ++ ys)
forall (ys :: [a]). List1 a ys -> List1 a (xs ++ ys)
xs)
dsnoc1 :: DList1 a xs -> a x -> DList1 a (xs ++ '[ x ])
dsnoc1 :: DList1 a xs -> a x -> DList1 a (xs ++ '[x])
dsnoc1 dx :: DList1 a xs
dx@(DList1 forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys)
xs) a x
x =
(forall (ys :: [k]). List1 a ys -> List1 a ((xs ++ '[x]) ++ ys))
-> DList1 a (xs ++ '[x])
forall k (a :: k -> *) (xs :: [k]).
(forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys))
-> DList1 a xs
DList1 ((forall (ys :: [k]). List1 a ys -> List1 a ((xs ++ '[x]) ++ ys))
-> DList1 a (xs ++ '[x]))
-> (forall (ys :: [k]). List1 a ys -> List1 a ((xs ++ '[x]) ++ ys))
-> DList1 a (xs ++ '[x])
forall a b. (a -> b) -> a -> b
$ \List1 a ys
ys ->
case DList1 a xs
-> DList1 a '[x]
-> List1 a ys
-> TypeEq ((xs ++ '[x]) ++ ys) (xs ++ ('[x] ++ ys))
forall k (proxy1 :: [k] -> *) (xs :: [k]) (proxy2 :: [k] -> *)
(ys :: [k]) (proxy3 :: [k] -> *) (zs :: [k]).
proxy1 xs
-> proxy2 ys
-> proxy3 zs
-> TypeEq ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
eqAppendAssoc DList1 a xs
dx (a x -> DList1 a '[x]
forall k (a :: k -> *) (x :: k). a x -> DList1 a '[x]
dsingleton1 a x
x) List1 a ys
ys of
TypeEq ((xs ++ '[x]) ++ ys) (xs ++ ('[x] ++ ys))
Refl -> List1 a (x : ys) -> List1 a (xs ++ (x : ys))
forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys)
xs (a x -> List1 a ys -> List1 a (x : ys)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 a x
x List1 a ys
ys)
dsingleton1 :: a x -> DList1 a '[ x ]
dsingleton1 :: a x -> DList1 a '[x]
dsingleton1 a x
x = (forall (ys :: [k]). List1 a ys -> List1 a ('[x] ++ ys))
-> DList1 a '[x]
forall k (a :: k -> *) (xs :: [k]).
(forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys))
-> DList1 a xs
DList1 (a x -> List1 a ys -> List1 a (x : ys)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 a x
x)
dappend1 :: DList1 a xs -> DList1 a ys -> DList1 a (xs ++ ys)
dappend1 :: DList1 a xs -> DList1 a ys -> DList1 a (xs ++ ys)
dappend1 dx :: DList1 a xs
dx@(DList1 forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys)
xs) dy :: DList1 a ys
dy@(DList1 forall (ys :: [k]). List1 a ys -> List1 a (ys ++ ys)
ys) =
(forall (ys :: [k]). List1 a ys -> List1 a ((xs ++ ys) ++ ys))
-> DList1 a (xs ++ ys)
forall k (a :: k -> *) (xs :: [k]).
(forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys))
-> DList1 a xs
DList1 ((forall (ys :: [k]). List1 a ys -> List1 a ((xs ++ ys) ++ ys))
-> DList1 a (xs ++ ys))
-> (forall (ys :: [k]). List1 a ys -> List1 a ((xs ++ ys) ++ ys))
-> DList1 a (xs ++ ys)
forall a b. (a -> b) -> a -> b
$ \List1 a ys
zs ->
case DList1 a xs
-> DList1 a ys
-> List1 a ys
-> TypeEq ((xs ++ ys) ++ ys) (xs ++ (ys ++ ys))
forall k (proxy1 :: [k] -> *) (xs :: [k]) (proxy2 :: [k] -> *)
(ys :: [k]) (proxy3 :: [k] -> *) (zs :: [k]).
proxy1 xs
-> proxy2 ys
-> proxy3 zs
-> TypeEq ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
eqAppendAssoc DList1 a xs
dx DList1 a ys
dy List1 a ys
zs of
TypeEq ((xs ++ ys) ++ ys) (xs ++ (ys ++ ys))
Refl -> List1 a (ys ++ ys) -> List1 a (xs ++ (ys ++ ys))
forall (ys :: [k]). List1 a ys -> List1 a (xs ++ ys)
xs (List1 a ys -> List1 a (ys ++ ys)
forall (ys :: [k]). List1 a ys -> List1 a (ys ++ ys)
ys List1 a ys
zs)