Safe Haskell  None 

 newtype Only a = Only {
 just :: a
 class Reversable t where
 class Shiftable t where
 viewr :: (Symmetric (>) p, Shiftable t, ShiftedR t ~ p a b) => t > p b a
 type :*: = (,)
 type :*! x y = (x, (y, ()))
 type :+: = Either
 class Product as => Homogeneous a as  as > a where
 repeat :: a > as
 toFList :: as > FixedList (Length as) a
 fromFList :: (as ~ Replicated len a, len ~ Length as) => FixedList len a > Replicated len a
 data FixedList length a
 (!!) :: (Product as, as ~ (i :=>> a), i ~ Length as, Exponent i) => as > i > a
 ($$:) :: (Length as ~ len, Replicated len b ~ bs, Homogeneous b bs, Homogeneous a as, Length bs ~ len) => (FixedList len a > FixedList len b) > as > bs
 replicate :: (Homogeneous a as, as ~ Replicated len a, len ~ Length as) => Proxy len > a > Replicated len a
 single :: a > (a, ())
 (*:) :: Product xs => x > xs > (x, xs)
 (*!) :: x > y > (x, (y, ()))
 class (Product p, Length p ~ c) => HavingLength c p  c > p
 ary :: HavingLength c p => Proxy c > (p > x) > p > x
 class MassageableNormal x y where
 massageNormal :: x > y
 extract :: (FactorPrefix t (Either t ts), Constant (Either t ts :/ t)) => Either t ts > t
 class Product ab => FactorPrefix ab abcs where
 type abcs :/ ab
 factorPrefix :: abcs > (ab, abcs :/ ab)
 class DistributeTerm xs where
 type family a :*<: xs
 class Multiply xs ys where
 class Exponent abc where
 type family abc :=>> x
 class Base abc where
 type family x :>=> abc
 constructorsOfNormal :: Exponent r => r > r :=>> r
 class Constant c
 type family Length t
 type family Replicated len a
 type One = ()
 type Two = One :+: One
 type Three = One :+: Two
 type Four = One :+: Three
 type Five = One :+: Four
 type Six = One :+: Five
 type Seven = One :+: Six
 _1 :: Proxy One
 _2 :: Proxy Two
 _3 :: Proxy Three
 _4 :: Proxy Four
 _5 :: Proxy Five
 _6 :: Proxy Six
 _7 :: Proxy Seven
 class Constant c => OneOrMore c where
 _1st :: c
 _2nd :: OneOrMore c => One :+: c
 _3rd :: OneOrMore c => One :+: (One :+: c)
 _4th :: OneOrMore c => One :+: (One :+: (One :+: c))
 _5th :: OneOrMore c => One :+: (One :+: (One :+: (One :+: c)))
 _6th :: OneOrMore c => One :+: (One :+: (One :+: (One :+: (One :+: c))))
 _7th :: OneOrMore c => One :+: (One :+: (One :+: (One :+: (One :+: (One :+: c)))))
 length :: Product as => as > Proxy (Length as)
 _of :: c > Proxy c > c
Documentation
Functions for composing and modifying our Normal
form types.
These take their names from the familiar functions in Data.List and Prelude, but are given more general forms, sometimes loosely after the constructions in Edward Kmett's categories package. There are probably many improvements and additions possible here.
You probably want to import this in one of the following ways:
import Data.Shapely.Normal as Sh import qualified Data.Shapely.Normal as Sh import Data.Shapely.Normal hiding ((!!),repeat,replicate,concat,reverse, map, length)
NOTE: The structure of the classes, type functions, and class constraints here are likely to change a lot.
A singleton inhabited Sum
. This is an intermediate type useful for
constructing sums, and in our instances (see e.g. Tail
)
Reordering Product
and Sum
terms
class Reversable t whereSource
Reversing Products
and Sum
s
Reversable ()  
(~ * xs (Either y zs), ~ * (Reversed (Either x xs)) (ShiftedL (Either x (Reversed xs))), Reversable xs, Shiftable (Either x (Reversed xs))) => Reversable (Either x (Either y zs))  
Reversable (Either x (a, b))  
Reversable (Either x ())  
(Reversable xs, Shiftable (x, Reversed xs)) => Reversable (x, xs) 
a class for shifting a sum or product left or right by one element, i.e. a logical shift
(Shiftable (Either y zs), Shiftable (Either x zs), ~ * xs (Either y zs), ~ * (Tail (Either x zs)) (Tail xs), ~ * (:< (Last xs) (:< x (Init xs))) (Either a0 (Either x c0)), ~ * (:< (Last xs) (Init xs)) (Either a0 c0)) => Shiftable (Either x (Either y zs))  
Shiftable (Either a (x, y))  
Shiftable (Either a ())  
(Shiftable (y, zs), Shiftable (x, zs), ~ * (ShiftedR (y, zs)) (Last (y, zs), Init (y, zs))) => Shiftable (x, (y, zs))  
Shiftable (x, ()) 
viewr :: (Symmetric (>) p, Shiftable t, ShiftedR t ~ p a b) => t > p b aSource
Note: viewl
would be simply id
.
viewr = swap . shiftr
Convenience Type synonyms
Operations on Products
Homogeneous (listlike) products
class Product as => Homogeneous a as  as > a whereSource
A class for homogeneous Product
s with terms all of type a
.
Fill a product with an initial value. If the size of the resulting product can't be inferred from context, provide a sype signature:
truths = repeat True :: (Bool,(Bool,(Bool,())))
toFList :: as > FixedList (Length as) aSource
Convert a homogeneous product to a fixedlength list.
fromFList :: (as ~ Replicated len a, len ~ Length as) => FixedList len a > Replicated len aSource
Convert a list back into a homogeneous Product
.
Homogeneous a ()  
(Homogeneous a as, ~ * (Replicated (Length as) a) as) => Homogeneous a (a, as) 
data FixedList length a Source
An opaque wrapper type allowing application of useful class methods on
Homogeneous
Product
s. Only operations that don't modify the length of
the product (which is stored in the len
parameter) are supported.
(!!) :: (Product as, as ~ (i :=>> a), i ~ Length as, Exponent i) => as > i > aSource
Return the term at the 1based index n
of the Homogeneous
Product
xs
.
as !! i = 'fanin' as (i `'_of'` 'length' as)
($$:) :: (Length as ~ len, Replicated len b ~ bs, Homogeneous b bs, Homogeneous a as, Length bs ~ len) => (FixedList len a > FixedList len b) > as > bsSource
($$:) f = fromFList . f . toFList
replicate :: (Homogeneous a as, as ~ Replicated len a, len ~ Length as) => Proxy len > a > Replicated len aSource
Replicate a
, producing a Product
of length len
.
replicate _ = 'repeat'
Construction convenience operators
Forcing types
class (Product p, Length p ~ c) => HavingLength c p  c > pSource
this inverts Length
HavingLength () (a, ())  
(HavingLength c p, ~ * (Length (a, p)) (Either () c)) => HavingLength (Either () c) (a, p) 
ary :: HavingLength c p => Proxy c > (p > x) > p > xSource
ary _ = id
Force the arity of an aritypolymorphic function on Product
s. e.g.
>>>
:t _3 `ary` shiftl
_3 `ary` shiftl :: (a, (a1, (a2, ()))) > ShiftedL (a, (a1, (a2, ())))
Product and Sum Conversions
class MassageableNormal x y whereSource
A class for massaging Normal
representation types. This works as
described in Massageable
, except that it doesn't recurse into subterms.
massageNormal :: x > ySource
Convert a Normal
type x
into some Massageable
normalform type y
MassageableNormalRec FLAT FLAT x y => MassageableNormal x y 
Algebraic
Factoring
class Product ab => FactorPrefix ab abcs whereSource
factorPrefix :: abcs > (ab, abcs :/ ab)Source
FactorPrefix () ()  
(FactorPrefix () abc, FactorPrefix () abcs) => FactorPrefix () (Either abc abcs)  
FactorPrefix () (x, y)  
(FactorPrefix (x, y) abc, FactorPrefix (x, y) abcs) => FactorPrefix (x, y) (Either abc abcs)  
FactorPrefix bs bcs => FactorPrefix (a, bs) (a, bcs) 
Distributing
class DistributeTerm xs whereSource
Algebraic multiplication of a term with some Normal
type xs
. When xs
is a Product
these are simple Cons/Snoc (see *:
). For Sum
s the
operation is distributed over all constructors, as in:
a(x + y + z) = (ax + ay + az)
(*<) :: a > xs > a :*<: xsSource
prepend the term a
.
(>*) :: xs > a > xs :>*: aSource
append the term a
.
DistributeTerm ()  
(DistributeTerm xs, DistributeTerm yss) => DistributeTerm (Either xs yss)  
DistributeTerm xs => DistributeTerm (x, xs) 
class Multiply xs ys whereSource
Algebraic multiplication of two Normal
form types xs
and ys
. When
both are Product
s this operation is like the Prelude (++)
. When both are
Sum
s the ordering of constructors follow the "FOIL" pattern, e.g.
(a + b + c)*(x + y) == (ax + ay + bx + by + cx + cy)
Just like normal multiplication, this is a monoid with ()
as our identity
object.
Exponentiation
In the algebra of algebraic datatypes, (>)
is analogous to
exponentiation, where xᵇ == (b > x)
. The operations here come from
translating the algebraic laws of exponents to their equivalents on
ADTs.
class Exponent abc whereSource
A class for the exponent laws with the Normal
form abc
in the exponent
place. See the instance documentation for concrete types and examples.
Exponent ()  
Exponent a => Exponent (Only a)  
(EitherTail bs, Exponent bs, Exponent (AsTail bs), Exponent a) => Exponent (Either a bs) 
Examples:

Exponent bs => Exponent (a, bs) 
Examples:

type family abc :=>> x Source
The algebraic normal form Exponent
abc
distributed over the single
base variable x
.
A class for the exponent laws with the Normal
form abc
in the base
place. See the instance documentation for concrete types and examples.
type family x :>=> abc Source
The single exponent variable x
distributed over the algebraic normal
form Base
abc
.
constructorsOfNormal :: Exponent r => r > r :=>> rSource
constructorsOfNormal = 'unfanin' id
See also constructorsOf
. E.g.
constructorsOfNormal ('a',('b',())) 'x' 'y' == ('x',('y',()))
Constants
Sum
s of the unit type are our constants in the algebra of ADTs.
They are cardinal numbers at the type level (length), while their values
are ordinal numbers (indicating position).
type family Replicated len a Source