cartesian-profunctors
Safe HaskellNone
LanguageHaskell2010

Data.Finitary.TreeRep

Synopsis

Base Type and its algebra

type Rep = [TreeRep] Source #

Representation of a finitary functor.

If we write {r} to mean the type r :: Rep represents,

r = [t1, t2, ...]

represent sum type

{t1} + {t2} + ...

Theories

Rep can be thought of as a datatype representing a thing called skew semiring freely generated from one generator.

Semiring is an abstract algebraic structure with addition and multiplication, but not necessarily have subtraction. Typical instance of semiring is Integer or Natural.

Skew semiring is another abstract algebraic structure similar to semiring: it has addition + and multiplication * with their respective units 0 and 1. What differentiates skew semiring is it distinguishes the order of additions. In any semiring, x + y and y + x must be equal; but in a skew semiring they can be different.

Formally, a skew semiring is a set A equipped with two binary operations (+),(*) :: A -> A -> A and two nullary operations 0,1 :: A, satisfying following equational axioms:

  • Addition (A, (+), 0) is a monoid
  • x + (y + z) === (x + y) + z
  • x + 0 === x === 0 + x
  • Multiplication (A, (*), 1) is a monoid
  • x * (y * z) === (x * y) * z
  • x * 1 === x === 1 * x
  • Multiplication from right distributes to left addition
  • 0 * z === 0
  • (x + y) * z === (x * z) + (y * z)

Note that both addition (+) and multiplication (*) are not guaranteed to be commutative, and distributive law exists only for one side.

Rep can be thought of as the free skew semiring on one generator a, or in other words the type of normal forms of skew semiring expressions built from (+,*,0,1) and one variable a.

Rep := 0 | TreeRep + Rep
TreeRep := 1 | a * Rep

Why skew semiring, and not a full semiring?

The Enum class assigns every finitary type x a canonical bijection x ≅ Finite n, giving each value a unique index from 0 to n-1. Two types with the same cardinality are "equal" in the semiring when this bijection is order-preserving. Under this notion of equality, the familiar type constructors satisfy some semiring laws but not all:

Addition is Either
Either a b encodes all Left-values before Right-values. Concatenating the two sequences is order-preserving.
Multiplication is (,)
(a, b) encodes in row-major (lexicographic) order: (a₀,b₀),(a₀,b₁),…,(a₁,b₀),…
Right distributivity holds
(Either a b, c) ≅ Either (a,c) (b,c) is order-preserving: the first |a|·|c| indices map to Left, the remaining |b|·|c| to Right. ✓
Left distributivity fails
(a, Either b c) ≅ Either (a,b) (a,c) is NOT order-preserving in general. The left side interleaves b- and c-values as it sweeps through a, whereas the right side puts all (a,b) pairs before all (a,c) pairs. ✗
Addition is not commutative
Either a b ≇ Either b a as ordered types: the first puts a-values first, the second puts b-values first.

This is exactly the definition of a skew semiring.

Because Rep is the free skew semiring on one generator, Eval r a describes finitary functors that respect this structure: given any Enum instance for a, Eval r a inherits a canonical Enum instance determined entirely by r.

data TreeRep Source #

Representation of a simple (= not a sum of multiple reps) finitary functor.

  • UnitRep represents a unit type: {UnitRep}(a) = ().
  • ParRep r represents a type with one parameter type prepended: {ParRep r}(a) = (a, {r}(a)).

Constructors

UnitRep 
ParRep Rep 

Instances

Instances details
Show TreeRep Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

showsPrec :: Int -> TreeRep -> ShowS #

show :: TreeRep -> String #

showList :: [TreeRep] -> ShowS #

Eq TreeRep Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

(==) :: TreeRep -> TreeRep -> Bool #

(/=) :: TreeRep -> TreeRep -> Bool #

Ord TreeRep Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

compare :: TreeRep -> TreeRep -> Ordering #

(<) :: TreeRep -> TreeRep -> Bool #

(<=) :: TreeRep -> TreeRep -> Bool #

(>) :: TreeRep -> TreeRep -> Bool #

(>=) :: TreeRep -> TreeRep -> Bool #

max :: TreeRep -> TreeRep -> TreeRep #

min :: TreeRep -> TreeRep -> TreeRep #

KnownRep ('[] :: [TreeRep]) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

sRep :: SRep ('[] :: [TreeRep]) Source #

(KnownTreeRep t, KnownRep r) => KnownRep (t ': r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

sRep :: SRep (t ': r) Source #

addRep :: Rep -> Rep -> Rep Source #

multRep :: Rep -> Rep -> Rep Source #

emptyRep :: Rep Source #

unitRep :: Rep Source #

Example representations

idRep :: Rep Source #

Representation of the identity functor

maybeRep :: Rep Source #

Representation of Maybe

Type-level Rep algebra

type family AddRep (r1 :: Rep) (r2 :: Rep) :: Rep where ... Source #

addRep at type level

Equations

AddRep ('[] :: [TreeRep]) r2 = r2 
AddRep (t ': r1) r2 = t ': AddRep r1 r2 

type family MultRep (r1 :: Rep) (r2 :: Rep) :: Rep where ... Source #

multRep at type level

Equations

MultRep ('[] :: [TreeRep]) _1 = '[] :: [TreeRep] 
MultRep ('UnitRep ': r1) r2 = AddRep r2 (MultRep r1 r2) 
MultRep ('ParRep sub1 ': r1) r2 = 'ParRep (MultRep sub1 r2) ': MultRep r1 r2 

data SRep (r :: Rep) where Source #

Singleton value for type-level Rep

Constructors

SEmpty :: SRep ('[] :: [TreeRep]) 
SCase :: forall (t :: TreeRep) (r1 :: [TreeRep]). !(STreeRep t) -> !(SRep r1) -> SRep (t ': r1) 

Instances

Instances details
Show (SRep r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

showsPrec :: Int -> SRep r -> ShowS #

show :: SRep r -> String #

showList :: [SRep r] -> ShowS #

Eq (SRep r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

(==) :: SRep r -> SRep r -> Bool #

(/=) :: SRep r -> SRep r -> Bool #

Ord (SRep r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

compare :: SRep r -> SRep r -> Ordering #

(<) :: SRep r -> SRep r -> Bool #

(<=) :: SRep r -> SRep r -> Bool #

(>) :: SRep r -> SRep r -> Bool #

(>=) :: SRep r -> SRep r -> Bool #

max :: SRep r -> SRep r -> SRep r #

min :: SRep r -> SRep r -> SRep r #

data STreeRep (t :: TreeRep) where Source #

Singleton value for type-level TreeRep

Constructors

SUnit :: STreeRep 'UnitRep 
SPar :: forall (r :: Rep). !(SRep r) -> STreeRep ('ParRep r) 

Instances

Instances details
Show (STreeRep t) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

showsPrec :: Int -> STreeRep t -> ShowS #

show :: STreeRep t -> String #

showList :: [STreeRep t] -> ShowS #

Eq (STreeRep r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

(==) :: STreeRep r -> STreeRep r -> Bool #

(/=) :: STreeRep r -> STreeRep r -> Bool #

Ord (STreeRep r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

compare :: STreeRep r -> STreeRep r -> Ordering #

(<) :: STreeRep r -> STreeRep r -> Bool #

(<=) :: STreeRep r -> STreeRep r -> Bool #

(>) :: STreeRep r -> STreeRep r -> Bool #

(>=) :: STreeRep r -> STreeRep r -> Bool #

max :: STreeRep r -> STreeRep r -> STreeRep r #

min :: STreeRep r -> STreeRep r -> STreeRep r #

(%++) :: forall (r1 :: Rep) (r2 :: Rep). SRep r1 -> SRep r2 -> SRep (AddRep r1 r2) Source #

Compute the witness of AddRep

(%*) :: forall (r1 :: Rep) (r2 :: Rep). SRep r1 -> SRep r2 -> SRep (MultRep r1 r2) Source #

Compute the witness of MultRep

sEmptyRep :: SRep ('[] :: [TreeRep]) Source #

sUnitRep :: SRep '['UnitRep] Source #

sIdRep :: SRep '['ParRep '['UnitRep]] Source #

class KnownRep (r :: Rep) where Source #

Methods

sRep :: SRep r Source #

Instances

Instances details
KnownRep ('[] :: [TreeRep]) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

sRep :: SRep ('[] :: [TreeRep]) Source #

(KnownTreeRep t, KnownRep r) => KnownRep (t ': r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

sRep :: SRep (t ': r) Source #

class KnownTreeRep (t :: TreeRep) where Source #

Methods

sTreeRep :: STreeRep t Source #

Instances

Instances details
KnownTreeRep 'UnitRep Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

sTreeRep :: STreeRep 'UnitRep Source #

KnownRep r => KnownTreeRep ('ParRep r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

sTreeRep :: STreeRep ('ParRep r) Source #

withKnownRep :: forall (r :: Rep) result. SRep r -> (KnownRep r => result) -> result Source #

withKnownTreeRep :: forall (t :: TreeRep) result. STreeRep t -> (KnownTreeRep t => result) -> result Source #

Evaluating Rep as a Haskell Functor

data Eval (r :: Rep) a where Source #

Constructors

EHere :: forall (t :: TreeRep) a (r1 :: [TreeRep]). !(EvalT t a) -> Eval (t ': r1) a 
EThere :: forall (r1 :: [TreeRep]) a (t :: TreeRep). !(Eval r1 a) -> Eval (t ': r1) a 

Instances

Instances details
Eq1 (Eval r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

liftEq :: (a -> b -> Bool) -> Eval r a -> Eval r b -> Bool #

Ord1 (Eval r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

liftCompare :: (a -> b -> Ordering) -> Eval r a -> Eval r b -> Ordering #

KnownRep r => PTraversable (Eval r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

ptraverseWith :: (Cartesian p, Cocartesian p) => (as -> Eval r a) -> (Eval r b -> bs) -> p a b -> p as bs Source #

Functor (Eval r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

fmap :: (a -> b) -> Eval r a -> Eval r b #

(<$) :: a -> Eval r b -> Eval r a #

Foldable (Eval r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

fold :: Monoid m => Eval r m -> m #

foldMap :: Monoid m => (a -> m) -> Eval r a -> m #

foldMap' :: Monoid m => (a -> m) -> Eval r a -> m #

foldr :: (a -> b -> b) -> b -> Eval r a -> b #

foldr' :: (a -> b -> b) -> b -> Eval r a -> b #

foldl :: (b -> a -> b) -> b -> Eval r a -> b #

foldl' :: (b -> a -> b) -> b -> Eval r a -> b #

foldr1 :: (a -> a -> a) -> Eval r a -> a #

foldl1 :: (a -> a -> a) -> Eval r a -> a #

toList :: Eval r a -> [a] #

null :: Eval r a -> Bool #

length :: Eval r a -> Int #

elem :: Eq a => a -> Eval r a -> Bool #

maximum :: Ord a => Eval r a -> a #

minimum :: Ord a => Eval r a -> a #

sum :: Num a => Eval r a -> a #

product :: Num a => Eval r a -> a #

Traversable (Eval r) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

traverse :: Applicative f => (a -> f b) -> Eval r a -> f (Eval r b) #

sequenceA :: Applicative f => Eval r (f a) -> f (Eval r a) #

mapM :: Monad m => (a -> m b) -> Eval r a -> m (Eval r b) #

sequence :: Monad m => Eval r (m a) -> m (Eval r a) #

Eq a => Eq (Eval r a) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

(==) :: Eval r a -> Eval r a -> Bool #

(/=) :: Eval r a -> Eval r a -> Bool #

Ord a => Ord (Eval r a) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

compare :: Eval r a -> Eval r a -> Ordering #

(<) :: Eval r a -> Eval r a -> Bool #

(<=) :: Eval r a -> Eval r a -> Bool #

(>) :: Eval r a -> Eval r a -> Bool #

(>=) :: Eval r a -> Eval r a -> Bool #

max :: Eval r a -> Eval r a -> Eval r a #

min :: Eval r a -> Eval r a -> Eval r a #

data EvalT (t :: TreeRep) a where Source #

Constructors

EUnit :: forall a. EvalT 'UnitRep a 
EPar :: forall a (r :: Rep). a -> Eval r a -> EvalT ('ParRep r) a 

Instances

Instances details
Eq1 (EvalT t) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

liftEq :: (a -> b -> Bool) -> EvalT t a -> EvalT t b -> Bool #

Ord1 (EvalT t) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

liftCompare :: (a -> b -> Ordering) -> EvalT t a -> EvalT t b -> Ordering #

KnownTreeRep t => PTraversable (EvalT t) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

ptraverseWith :: (Cartesian p, Cocartesian p) => (as -> EvalT t a) -> (EvalT t b -> bs) -> p a b -> p as bs Source #

Functor (EvalT t) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

fmap :: (a -> b) -> EvalT t a -> EvalT t b #

(<$) :: a -> EvalT t b -> EvalT t a #

Foldable (EvalT t) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

fold :: Monoid m => EvalT t m -> m #

foldMap :: Monoid m => (a -> m) -> EvalT t a -> m #

foldMap' :: Monoid m => (a -> m) -> EvalT t a -> m #

foldr :: (a -> b -> b) -> b -> EvalT t a -> b #

foldr' :: (a -> b -> b) -> b -> EvalT t a -> b #

foldl :: (b -> a -> b) -> b -> EvalT t a -> b #

foldl' :: (b -> a -> b) -> b -> EvalT t a -> b #

foldr1 :: (a -> a -> a) -> EvalT t a -> a #

foldl1 :: (a -> a -> a) -> EvalT t a -> a #

toList :: EvalT t a -> [a] #

null :: EvalT t a -> Bool #

length :: EvalT t a -> Int #

elem :: Eq a => a -> EvalT t a -> Bool #

maximum :: Ord a => EvalT t a -> a #

minimum :: Ord a => EvalT t a -> a #

sum :: Num a => EvalT t a -> a #

product :: Num a => EvalT t a -> a #

Traversable (EvalT t) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

traverse :: Applicative f => (a -> f b) -> EvalT t a -> f (EvalT t b) #

sequenceA :: Applicative f => EvalT t (f a) -> f (EvalT t a) #

mapM :: Monad m => (a -> m b) -> EvalT t a -> m (EvalT t b) #

sequence :: Monad m => EvalT t (m a) -> m (EvalT t a) #

Eq a => Eq (EvalT t a) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

(==) :: EvalT t a -> EvalT t a -> Bool #

(/=) :: EvalT t a -> EvalT t a -> Bool #

Ord a => Ord (EvalT t a) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

compare :: EvalT t a -> EvalT t a -> Ordering #

(<) :: EvalT t a -> EvalT t a -> Bool #

(<=) :: EvalT t a -> EvalT t a -> Bool #

(>) :: EvalT t a -> EvalT t a -> Bool #

(>=) :: EvalT t a -> EvalT t a -> Bool #

max :: EvalT t a -> EvalT t a -> EvalT t a #

min :: EvalT t a -> EvalT t a -> EvalT t a #

Correspondence between sums and products of Rep and its evaluation

fromSum :: forall (r1 :: Rep) proxy (r2 :: Rep) x. SRep r1 -> proxy r2 -> Either (Eval r1 x) (Eval r2 x) -> Eval (AddRep r1 r2) x Source #

inlEval :: forall (r1 :: Rep) proxy (r2 :: Rep) x. SRep r1 -> proxy r2 -> Eval r1 x -> Eval (AddRep r1 r2) x Source #

inrEval :: forall (r1 :: Rep) proxy (r2 :: Rep) x. SRep r1 -> proxy r2 -> Eval r2 x -> Eval (AddRep r1 r2) x Source #

toSum :: forall (r1 :: Rep) proxy (r2 :: Rep) x. SRep r1 -> proxy r2 -> Eval (AddRep r1 r2) x -> Either (Eval r1 x) (Eval r2 x) Source #

fromProduct :: forall (r1 :: Rep) (r2 :: Rep) x. SRep r1 -> SRep r2 -> Eval r1 x -> Eval r2 x -> Eval (MultRep r1 r2) x Source #

toProduct :: forall (r1 :: Rep) (r2 :: Rep) x. SRep r1 -> SRep r2 -> Eval (MultRep r1 r2) x -> (Eval r1 x, Eval r2 x) Source #

absurdEval :: Eval ('[] :: [TreeRep]) a -> any Source #

unitEval :: Eval '['UnitRep] a Source #

Profunctor traversal

ptraverseEval :: forall p (r :: Rep) a b. (Cartesian p, Cocartesian p) => SRep r -> p a b -> p (Eval r a) (Eval r b) Source #

ptraverseEvalT :: forall p (t :: TreeRep) a b. (Cartesian p, Cocartesian p) => STreeRep t -> p a b -> p (EvalT t a) (EvalT t b) Source #

Building bidirectional encodings as a Eval r with Profunctor

data Encoder a b s t where Source #

Constructors

Encoder :: forall (r :: Rep) s a b t. !(SRep r) -> (s -> Eval r a) -> (Eval r b -> t) -> Encoder a b s t 

Instances

Instances details
Cartesian (Encoder a b) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

proUnit :: Encoder a b a0 () Source #

proProduct :: (a0 -> (a1, a2)) -> ((b1, b2) -> b0) -> Encoder a b a1 b1 -> Encoder a b a2 b2 -> Encoder a b a0 b0 Source #

(***) :: Encoder a b a0 b0 -> Encoder a b a' b' -> Encoder a b (a0, a') (b0, b') Source #

(&&&) :: Encoder a b a0 b0 -> Encoder a b a0 b' -> Encoder a b a0 (b0, b') Source #

proPower :: forall (n :: Nat) a0 b0. KnownNat n => Encoder a b a0 b0 -> Encoder a b (Finite n -> a0) (Finite n -> b0) Source #

Cocartesian (Encoder a b) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

proEmpty :: Encoder a b Void b0 Source #

proSum :: (a0 -> Either a1 a2) -> (Either b1 b2 -> b0) -> Encoder a b a1 b1 -> Encoder a b a2 b2 -> Encoder a b a0 b0 Source #

(+++) :: Encoder a b a0 b0 -> Encoder a b a' b' -> Encoder a b (Either a0 a') (Either b0 b') Source #

(|||) :: Encoder a b a0 b0 -> Encoder a b a' b0 -> Encoder a b (Either a0 a') b0 Source #

proTimes :: forall (n :: Nat) a0 b0. KnownNat n => Encoder a b a0 b0 -> Encoder a b (Finite n, a0) (Finite n, b0) Source #

Profunctor (Encoder a b) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

dimap :: (a0 -> b0) -> (c -> d) -> Encoder a b b0 c -> Encoder a b a0 d #

lmap :: (a0 -> b0) -> Encoder a b b0 c -> Encoder a b a0 c #

rmap :: (b0 -> c) -> Encoder a b a0 b0 -> Encoder a b a0 c #

(#.) :: forall a0 b0 c q. Coercible c b0 => q b0 c -> Encoder a b a0 b0 -> Encoder a b a0 c #

(.#) :: forall a0 b0 c q. Coercible b0 a0 => Encoder a b b0 c -> q a0 b0 -> Encoder a b a0 c #

Functor (Encoder a b s) Source # 
Instance details

Defined in Data.Finitary.TreeRep

Methods

fmap :: (a0 -> b0) -> Encoder a b s a0 -> Encoder a b s b0 #

(<$) :: a0 -> Encoder a b s b0 -> Encoder a b s a0 #

idEncoder :: Encoder a b a b Source #

Encoder for the identity functor.

It can be used to construct an encoder for arbitrary PTraversable functor using ptraverse idEncoder.