Safe Haskell | None |
---|---|
Language | Haskell98 |
- data S n :: * -> *
- data Z :: *
- class ((~) Nat (ToNat a) b, (~) * (ToPeano b) a) => NatIso a b
- type family ToPeano b :: *
- type family ToNat a :: Nat
- type family Fn as b
- newtype Fun as b = Fun {}
- newtype TFun f as b = TFun {}
- funToTFun :: Fun (Wrap f xs) b -> TFun f xs b
- tfunToFun :: TFun f xs b -> Fun (Wrap f xs) b
- data Proxy t :: k -> * = Proxy
- type family xs ++ ys :: [α]
- type family Len xs :: *
- type family Wrap f a :: [β]
- type family HomList n a :: [α]
- class Arity (Len xs) => Arity xs where
- accum :: (forall a as. t (a : as) -> a -> t as) -> (t [] -> b) -> t xs -> Fn xs b
- apply :: (forall a as. t (a : as) -> (a, t as)) -> t xs -> ContVec xs
- applyM :: Monad m => (forall a as. t (a : as) -> m (a, t as)) -> t xs -> m (ContVec xs)
- accumTy :: (forall a as. t (a : as) -> f a -> t as) -> (t [] -> b) -> t xs -> Fn (Wrap f xs) b
- applyTy :: (forall a as. t (a : as) -> (f a, t as)) -> t xs -> ContVecF xs f
- arity :: p xs -> Int
- witWrapped :: WitWrapped f xs
- witConcat :: Arity ys => WitConcat xs ys
- witNestedFun :: WitNestedFun xs ys r
- witLenWrap :: WitLenWrap f xs
- class Arity xs => ArityC c xs where
- witAllInstances :: WitAllInstances c xs
- class Arity (Elems v) => HVector v where
- class Arity (ElemsF v) => HVectorF v where
- data WitWrapped f xs where
- WitWrapped :: Arity (Wrap f xs) => WitWrapped f xs
- data WitConcat xs ys where
- data WitNestedFun xs ys r where
- WitNestedFun :: (Fn (xs ++ ys) r ~ Fn xs (Fn ys r)) => WitNestedFun xs ys r
- data WitLenWrap f xs where
- WitLenWrap :: (Len xs ~ Len (Wrap f xs)) => WitLenWrap f xs
- data WitWrapIndex f n xs where
- WitWrapIndex :: (ValueAt n (Wrap f xs) ~ f (ValueAt n xs), Index n (Wrap f xs), Arity (Wrap f xs)) => WitWrapIndex f n xs
- data WitAllInstances c xs where
- WitAllInstancesNil :: WitAllInstances c []
- WitAllInstancesCons :: c x => WitAllInstances c xs -> WitAllInstances c (x : xs)
- newtype ContVec xs = ContVec {
- runContVec :: forall r. Fun xs r -> r
- newtype ContVecF xs f = ContVecF (forall r. TFun f xs r -> r)
- toContVec :: ContVecF xs f -> ContVec (Wrap f xs)
- toContVecF :: ContVec (Wrap f xs) -> ContVecF xs f
- cons :: x -> ContVec xs -> ContVec (x : xs)
- consF :: f x -> ContVecF xs f -> ContVecF (x : xs) f
- class (Arity n, Arity (HomList n a)) => HomArity n a where
- toHeterogeneous :: Fun n a r -> Fun (HomList n a) r
- toHomogeneous :: Fun (HomList n a) r -> Fun n a r
- homInspect :: (Vector v a, HomArity (Dim v) a) => v a -> Fun (HomList (Dim v) a) r -> r
- homConstruct :: forall v a. (Vector v a, HomArity (Dim v) a) => Fun (HomList (Dim v) a) (v a)
- curryFun :: Fun (x : xs) r -> x -> Fun xs r
- uncurryFun :: (x -> Fun xs r) -> Fun (x : xs) r
- uncurryFun2 :: Arity xs => (x -> y -> Fun xs (Fun ys r)) -> Fun (x : xs) (Fun (y : ys) r)
- curryMany :: forall xs ys r. Arity xs => Fun (xs ++ ys) r -> Fun xs (Fun ys r)
- constFun :: Fun xs r -> Fun (x : xs) r
- stepFun :: (Fun xs a -> Fun ys b) -> Fun (x : xs) a -> Fun (x : ys) b
- curryTFun :: TFun f (x : xs) r -> f x -> TFun f xs r
- uncurryTFun :: (f x -> TFun f xs r) -> TFun f (x : xs) r
- uncurryTFun2 :: (Arity xs, Arity ys) => (f x -> f y -> TFun f xs (TFun f ys r)) -> TFun f (x : xs) (TFun f (y : ys) r)
- shuffleTF :: forall f x xs r. Arity xs => (x -> TFun f xs r) -> TFun f xs (x -> r)
- concatF :: (Arity xs, Arity ys) => (a -> b -> c) -> Fun xs a -> Fun ys b -> Fun (xs ++ ys) c
- shuffleF :: forall x xs r. Arity xs => (x -> Fun xs r) -> Fun xs (x -> r)
- lensWorkerF :: forall f r x y xs. (Functor f, Arity xs) => (x -> f y) -> Fun (y : xs) r -> Fun (x : xs) (f r)
- class Arity n => Index n xs where
- type ValueAt n xs :: *
- type NewElems n xs a :: [*]
- getF :: n -> Fun xs (ValueAt n xs)
- putF :: n -> ValueAt n xs -> Fun xs r -> Fun xs r
- lensF :: (Functor f, v ~ ValueAt n xs) => n -> (v -> f v) -> Fun xs r -> Fun xs (f r)
- lensChF :: Functor f => n -> (ValueAt n xs -> f a) -> Fun (NewElems n xs a) r -> Fun xs (f r)
- witWrapIndex :: WitWrapIndex f n xs
Types and type classes
Peano numbers
data S n :: * -> *
Successor of n
Arity n => Index Z (S n) | |
Arity n => Arity (S n) | |
(NatIso k ((-) n 1), (~) * (ToPeano ((-) n 1)) k, (~) * (ToPeano n) (S k), (~) Nat n ((+) 1 ((-) n 1))) => NatIso (S k) n | |
HomArity n a => HomArity (S n) a | |
Index k n => Index (S k) (S n) | |
Index n xs => Index (S n) ((:) * x xs) | |
Typeable (* -> *) S | |
type HomList k (S n) a = (:) k a (HomList k n a) | |
type Add (S n) k = S (Add n k) | |
type Fn (S n) a b = a -> Fn n a b | |
type ValueAt (S n) ((:) * x xs) = ValueAt n xs | |
type NewElems (S n) ((:) * x xs) a = (:) * x (NewElems n xs a) |
data Z :: *
Type level zero
Isomorphism between Peano numbers and Nats
class ((~) Nat (ToNat a) b, (~) * (ToPeano b) a) => NatIso a b
Isomorphism between two representations of natural numbers
type family ToPeano b :: *
Convert Nat number to Peano represenation
N-ary functions
Type family for N-ary function. Types of function parameters are encoded as the list of types.
Newtype wrapper to work around of type families' lack of injectivity.
Newtype wrapper for function where all type parameters have same type constructor. This type is required for writing function which works with monads, appicatives etc.
Type functions
data Proxy t :: k -> *
A concrete, poly-kinded proxy type
Monad (Proxy *) | |
Functor (Proxy *) | |
Applicative (Proxy *) | |
Vector (Proxy *) a | |
Bounded (Proxy k s) | |
Enum (Proxy k s) | |
Eq (Proxy k s) | |
Ord (Proxy k s) | |
Read (Proxy k s) | |
Show (Proxy k s) | |
Ix (Proxy k s) | |
Generic (Proxy * t) | |
Monoid (Proxy * s) | |
type Dim (Proxy *) = Z | |
type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy U1) |
type family Len xs :: * Source
Length of type list expressed as type level naturals from
fixed-vector
.
type family HomList n a :: [α] Source
Homogeneous type list with length n and element of type a. It
uses type level natural defined in fixed-vector
.
Type classes
class Arity (Len xs) => Arity xs where Source
Type class for dealing with N-ary function in generic way. Both
accum
and apply
work with accumulator data types which are
polymorphic. So it's only possible to write functions which
rearrange elements in vector using plain ADT. It's possible to
get around it by using GADT as accumulator (See ArityC
and
function which use it)
This is also somewhat a kitchen sink module. It contains witnesses which could be used to prove type equalities or to bring instance in scope.
:: (forall a as. t (a : as) -> a -> t as) | Step function. Applies element to accumulator. |
-> (t [] -> b) | Extract value from accumulator. |
-> t xs | Initial state. |
-> Fn xs b |
Fold over N elements exposed as N-ary function.
:: (forall a as. t (a : as) -> (a, t as)) | Extract value to be applied to function. |
-> t xs | Initial state. |
-> ContVec xs |
Apply values to N-ary function
:: Monad m | |
=> (forall a as. t (a : as) -> m (a, t as)) | Extract value to be applied to function |
-> t xs | Initial state |
-> m (ContVec xs) |
Apply value to N-ary function using monadic actions
accumTy :: (forall a as. t (a : as) -> f a -> t as) -> (t [] -> b) -> t xs -> Fn (Wrap f xs) b Source
Analog of accum
applyTy :: (forall a as. t (a : as) -> (f a, t as)) -> t xs -> ContVecF xs f Source
Analog of apply
which allows to works with vectors which
elements are wrapped in the newtype constructor.
Size of type list as integer.
witWrapped :: WitWrapped f xs Source
witConcat :: Arity ys => WitConcat xs ys Source
witNestedFun :: WitNestedFun xs ys r Source
witLenWrap :: WitLenWrap f xs Source
class Arity xs => ArityC c xs where Source
Declares that every type in list satisfy constraint c
witAllInstances :: WitAllInstances c xs Source
class Arity (Elems v) => HVector v where Source
Type class for heterogeneous vectors. Instance should specify way to construct and deconstruct itself
Note that this type class is extremely generic. Almost any single constructor data type could be made instance. It could be monomorphic, it could be polymorphic in some or all fields it doesn't matter. Only law instance should obey is:
inspect v construct = v
Default implementation which uses Generic
is provided.
Nothing
construct :: Fun (Elems v) v Source
Function for constructing vector
inspect :: v -> Fun (Elems v) a -> a Source
Function for deconstruction of vector. It applies vector's elements to N-ary function.
HVector () | Unit is empty heterogeneous vector |
HVector (Complex a) | |
Arity xs => HVector (ContVec xs) | |
Arity xs => HVector (VecList xs) | |
Arity xs => HVector (HVec xs) | |
HVector (a, b) | |
(Storable a, HomArity n a) => HVector (Vec n a) | |
(Unbox n a, HomArity n a) => HVector (Vec n a) | |
(Prim a, HomArity n a) => HVector (Vec n a) | |
HomArity n a => HVector (Vec n a) | |
(Arity (Wrap * * f xs), Arity xs) => HVector (HVecF xs f) | It's not possible to remove constrain |
HVector (a, b, c) | |
HVector (a, b, c, d) | |
HVector (a, b, c, d, e) | |
HVector (a, b, c, d, e, f) | |
HVector (a, b, c, d, e, f, g) | |
HVector (a, b, c, d, e, f, g, h) | |
HVector (a, b, c, d, e, f, g, h, i) | |
HVector (a, b, c, d, e, f, g, h, i, j) | |
HVector (a, b, c, d, e, f, g, h, i, j, k) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z) | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a') | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a', b') | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a', b', c') | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a', b', c', d') | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a', b', c', d', e') | |
HVector (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a', b', c', d', e', f') |
class Arity (ElemsF v) => HVectorF v where Source
Type class for partially homogeneous vector where every element in the vector have same type constructor. Vector itself is parametrized by that constructor
Witnesses
data WitWrapped f xs where Source
Witness that observe fact that if we have instance Arity xs
than we have instance Arity (Wrap f xs)
.
WitWrapped :: Arity (Wrap f xs) => WitWrapped f xs |
data WitConcat xs ys where Source
Witness that observe fact that (Arity xs, Arity ys)
implies
Arity (xs++ys)
data WitNestedFun xs ys r where Source
Observes fact that Fn (xs++ys) r ~ Fn xs (Fn ys r)
WitNestedFun :: (Fn (xs ++ ys) r ~ Fn xs (Fn ys r)) => WitNestedFun xs ys r |
data WitLenWrap f xs where Source
Observe fact than Len xs ~ Len (Wrap f xs)
WitLenWrap :: (Len xs ~ Len (Wrap f xs)) => WitLenWrap f xs |
data WitWrapIndex f n xs where Source
Proofs for the indexing of wrapped type lists.
WitWrapIndex :: (ValueAt n (Wrap f xs) ~ f (ValueAt n xs), Index n (Wrap f xs), Arity (Wrap f xs)) => WitWrapIndex f n xs |
data WitAllInstances c xs where Source
Witness that all elements of type list satisfy predicate c
.
WitAllInstancesNil :: WitAllInstances c [] | |
WitAllInstancesCons :: c x => WitAllInstances c xs -> WitAllInstances c (x : xs) |
CPS-encoded vector
CPS-encoded heterogeneous vector.
ContVec | |
|
CPS-encoded partially heterogeneous vector.
toContVecF :: ContVec (Wrap f xs) -> ContVecF xs f Source
Interop with homogeneous vectors
class (Arity n, Arity (HomList n a)) => HomArity n a where Source
Conversion between homogeneous and heterogeneous N-ary functions.
toHeterogeneous :: Fun n a r -> Fun (HomList n a) r Source
Convert n-ary homogeneous function to heterogeneous.
toHomogeneous :: Fun (HomList n a) r -> Fun n a r Source
Convert heterogeneous n-ary function to homogeneous.
homInspect :: (Vector v a, HomArity (Dim v) a) => v a -> Fun (HomList (Dim v) a) r -> r Source
Default implementation of inspect
for homogeneous vector.
homConstruct :: forall v a. (Vector v a, HomArity (Dim v) a) => Fun (HomList (Dim v) a) (v a) Source
Default implementation of construct
for homogeneous vector.
Operations of Fun
Primitives for Fun
uncurryFun :: (x -> Fun xs r) -> Fun (x : xs) r Source
Uncurry N-ary function.
curryMany :: forall xs ys r. Arity xs => Fun (xs ++ ys) r -> Fun xs (Fun ys r) Source
Curry first n arguments of N-ary function.
stepFun :: (Fun xs a -> Fun ys b) -> Fun (x : xs) a -> Fun (x : ys) b Source
Transform function but leave outermost parameter untouched.
Primitives for TFun
uncurryTFun :: (f x -> TFun f xs r) -> TFun f (x : xs) r Source
Uncurry single parameter
uncurryTFun2 :: (Arity xs, Arity ys) => (f x -> f y -> TFun f xs (TFun f ys r)) -> TFun f (x : xs) (TFun f (y : ys) r) Source
Uncurry two parameters for nested TFun.
shuffleTF :: forall f x xs r. Arity xs => (x -> TFun f xs r) -> TFun f xs (x -> r) Source
Move first argument of function to its result. This function is useful for implementation of lens.
More complicated functions
concatF :: (Arity xs, Arity ys) => (a -> b -> c) -> Fun xs a -> Fun ys b -> Fun (xs ++ ys) c Source
Concatenate n-ary functions. This function combine results of both N-ary functions and merge their parameters into single list.
shuffleF :: forall x xs r. Arity xs => (x -> Fun xs r) -> Fun xs (x -> r) Source
Move first argument of function to its result. This function is useful for implementation of lens.
lensWorkerF :: forall f r x y xs. (Functor f, Arity xs) => (x -> f y) -> Fun (y : xs) r -> Fun (x : xs) (f r) Source
Helper for lens implementation.
class Arity n => Index n xs where Source
Indexing of vectors
getF :: n -> Fun xs (ValueAt n xs) Source
Getter function for vectors
putF :: n -> ValueAt n xs -> Fun xs r -> Fun xs r Source
Putter function. It applies value x
to n
th parameter of
function.
lensF :: (Functor f, v ~ ValueAt n xs) => n -> (v -> f v) -> Fun xs r -> Fun xs (f r) Source
Helper for implementation of lens
lensChF :: Functor f => n -> (ValueAt n xs -> f a) -> Fun (NewElems n xs a) r -> Fun xs (f r) Source
Helper for type-changing lens
witWrapIndex :: WitWrapIndex f n xs Source