Algebra.Internal

Synopsis

• toProxy :: a -> Proxy a
• data Nat
  • = Z
  • | S Nat
• data SNat n where
  • SZ :: SNat Z
  • SS :: SNat n -> SNat (S n)
• data Vector a n where
  • Nil :: Vector a Z
  • :- :: a -> Vector a n -> Vector a (S n)
• class Sing n where
  • sing :: SNat n
• data SingInstance a where
  • SingInstance :: Sing a => SingInstance a
• singInstance :: SNat n -> SingInstance n
• toInt :: SNat n -> Int
• type family Min n m :: Nat
• type family Max n m :: Nat
• sMin :: SNat n -> SNat m -> SNat (Min n m)
• sMax :: SNat n -> SNat m -> SNat (Max n m)
• sZ :: SNat Z
• sS :: SNat n -> SNat (S n)
• type family n :+: m :: Nat
• (%+) :: SNat n -> SNat m -> SNat (n :+: m)
• type family n :-: m :: Nat
• (%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m)
• sZero :: SZero
• sOne :: SOne
• sTwo :: STwo
• sThree :: SThree
• type Zero = Z
• type One = S Z
• type Two = S (S Z)
• type Three = S (S (S Z))
• type SZero = SNat Zero
• type SOne = SNat One
• type STwo = SNat Two
• type SThree = SNat Three
• lengthV :: Vector a n -> Int
• sLengthV :: Vector a n -> SNat n
• takeV :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a n
• dropV :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)
• splitAtV :: (n :<<= m) ~ True => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))
• appendV :: Vector a n -> Vector a m -> Vector a (n :+: m)
• foldrV :: (a -> b -> b) -> b -> Vector a n -> b
• foldlV :: (a -> b -> a) -> a -> Vector b n -> a
• singletonV :: a -> Vector a (S Z)
• zipWithV :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n
• toList :: Vector a n -> [a]
• allV :: (a -> Bool) -> Vector a n -> Bool
• mapV :: (a -> b) -> Vector a n -> Vector b n
• headV :: Vector a (S n) -> a
• tailV :: Vector a (S n) -> Vector a n
• data Leq n m where
  • ZeroLeq :: SNat m -> Leq Zero m
  • SuccLeqSucc :: Leq n m -> Leq (S n) (S m)
• type family n :<<= m :: Bool
• class n :<= m
• data LeqInstance n m where
  • LeqInstance :: n :<= m => LeqInstance n m
• data LeqTrueInstance a b where
  • LeqTrueInstance :: (a :<<= b) ~ True => LeqTrueInstance a b
• boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
• boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
• propToClassLeq :: Leq n m -> LeqInstance n m
• propToBoolLeq :: Leq n m -> LeqTrueInstance n m
• leqRefl :: SNat n -> Leq n n
• leqSucc :: SNat n -> Leq n (S n)
• data Eql a b where
  • Eql :: Eql a a
• eqlRefl :: SNat a -> Eql a a
• eqlSymm :: Eql a b -> Eql b a
• eqlTrans :: Eql a b -> Eql b c -> Eql a c
• plusZR :: SNat n -> Eql (n :+: Z) n
• plusZL :: SNat n -> Eql (Z :+: n) n
• eqPreservesS :: Eql n m -> Eql (S n) (S m)
• plusAssociative :: SNat n -> SNat m -> SNat l -> Eql (n :+: (m :+: l)) ((n :+: m) :+: l)
• sAndPlusOne :: SNat n -> Eql (S n) (n :+: One)
• plusCommutative :: SNat n -> SNat m -> Eql (n :+: m) (m :+: n)
• minusCongEq :: Eql n m -> SNat l -> Eql (n :-: l) (m :-: l)
• minusNilpotent :: SNat n -> Eql (n :-: n) Zero
• eqSuccMinus :: (m :<<= n) ~ True => SNat n -> SNat m -> Eql (S n :-: m) (S (n :-: m))
• plusMinusEqL :: SNat n -> SNat m -> Eql ((n :+: m) :-: m) n
• plusMinusEqR :: SNat n -> SNat m -> Eql ((m :+: n) :-: m) n
• plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)
• plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)
• zAbsorbsMinR :: SNat n -> Eql (Min n Z) Z
• zAbsorbsMinL :: SNat n -> Eql (Min Z n) Z
• minLeqL :: SNat n -> SNat m -> Leq (Min n m) n
• minLeqR :: SNat n -> SNat m -> Leq (Min n m) m
• leqRhs :: Leq n m -> SNat m
• leqLhs :: Leq n m -> SNat n
• leqTrans :: Leq n m -> Leq m l -> Leq n l
• minComm :: SNat n -> SNat m -> Eql (Min n m) (Min m n)
• leqAnitsymmetric :: Leq n m -> Leq m n -> Eql n m
• maxZL :: SNat n -> Eql (Max Z n) n
• maxComm :: SNat n -> SNat m -> Eql (Max n m) (Max m n)
• maxZR :: SNat n -> Eql (Max n Z) n
• maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)
• maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)
• data Monomorphic k = forall a . Monomorphic (k a)
• class Monomorphicable k where
  • type MonomorphicRep k :: *
  • promote :: MonomorphicRep k -> Monomorphic k
  • demote :: Monomorphic k -> MonomorphicRep k
• demote' :: Monomorphicable k => k a -> MonomorphicRep k
• demoteComposed :: Monomorphicable (f :.: g) => f (g a) -> MonomorphicRep (f :.: g)
• monomorphicCompose :: f (g a) -> Monomorphic (f :.: g)
• withPolymorhic :: Monomorphicable k => MonomorphicRep k -> (forall a. k a -> b) -> b
• liftPoly :: Monomorphicable k => (forall a. k a -> b) -> MonomorphicRep k -> b
• viaPoly :: (Monomorphicable k, Monomorphicable k') => (forall x y. k x -> k' y) -> MonomorphicRep k -> MonomorphicRep k'
• newtype (f :.: g) a = Comp (f (g a))

Documentation