Copyright | (c) Eitan Chatav 2019 |
---|---|
Maintainer | eitan@morphism.tech |
Stability | experimental |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Haskell singly-linked lists are very powerful. This module provides functionality for type-level lists, heterogeneous lists and type aligned lists.
Synopsis
- data NP (a :: k -> Type) (b :: [k]) where
- (*:) :: f x -> f y -> NP f '[x, y]
- one :: f x -> NP f '[x]
- data Path (p :: k -> k -> Type) (x :: k) (y :: k) where
- type family Join xs ys where ...
- disjoin :: forall xs ys expr. SListI xs => NP expr (Join xs ys) -> (NP expr xs, NP expr ys)
- class Additional expr where
- type family Elem x xs where ...
- type family In x xs :: Constraint where ...
- type family Length (xs :: [k]) :: Nat where ...
- type family SubList (xs :: [k]) (ys :: [k]) :: Bool where ...
- type family SubsetList (xs :: [k]) (ys :: [k]) :: Bool where ...
- type Sort ls = MergeSort (Twos ls)
- type family MergeSort (ls :: [[Symbol]]) :: [Symbol] where ...
- type family Twos (ls :: [k]) :: [[k]] where ...
- type family FoldMerge (ls :: [[Symbol]]) :: [[Symbol]] where ...
- type family Merge (ls :: [Symbol]) (rs :: [Symbol]) :: [Symbol] where ...
- type family MergeHelper (ls :: [Symbol]) (rs :: [Symbol]) (cmp :: Ordering) where ...
- type family MapFst (ls :: [(j, k)]) :: [j] where ...
Heterogeneous List
data NP (a :: k -> Type) (b :: [k]) where #
An n-ary product.
The product is parameterized by a type constructor f
and
indexed by a type-level list xs
. The length of the list
determines the number of elements in the product, and if the
i
-th element of the list is of type x
, then the i
-th
element of the product is of type f x
.
The constructor names are chosen to resemble the names of the list constructors.
Two common instantiations of f
are the identity functor I
and the constant functor K
. For I
, the product becomes a
heterogeneous list, where the type-level list describes the
types of its components. For
, the product becomes a
homogeneous list, where the contents of the type-level list are
ignored, but its length still specifies the number of elements.K
a
In the context of the SOP approach to generic programming, an n-ary product describes the structure of the arguments of a single data constructor.
Examples:
I 'x' :* I True :* Nil :: NP I '[ Char, Bool ] K 0 :* K 1 :* Nil :: NP (K Int) '[ Char, Bool ] Just 'x' :* Nothing :* Nil :: NP Maybe '[ Char, Bool ]
Nil :: forall {k} (a :: k -> Type). NP a ('[] :: [k]) | |
(:*) :: forall {k} (a :: k -> Type) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x ': xs) infixr 5 |
Instances
(Has rel rels cols, Has col cols ty, bys ~ '['(rel, col)]) => IsQualified rel col (NP (By rels) bys) Source # | |
(Has tab (Join from lat) row, Has col row ty, GroupedBy tab col bys, tys ~ '[ty]) => IsQualified tab col (NP (Expression ('Grouped bys) lat with db params from) tys) Source # | |
Defined in Squeal.PostgreSQL.Expression | |
(Has tab (Join from lat) row, Has col row ty, tys ~ '[ty]) => IsQualified tab col (NP (Expression 'Ungrouped lat with db params from) tys) Source # | |
Defined in Squeal.PostgreSQL.Expression | |
(Has tab (Join from lat) row, Has col row ty, GroupedBy tab col bys, columns ~ '[col ::: ty]) => IsQualified tab col (NP (Aliased (Expression ('Grouped bys) lat with db params from)) columns) Source # | |
Defined in Squeal.PostgreSQL.Expression | |
(Has tab (Join from lat) row, Has col row ty, columns ~ '[col ::: ty]) => IsQualified tab col (NP (Aliased (Expression 'Ungrouped lat with db params from)) columns) Source # | |
Defined in Squeal.PostgreSQL.Expression | |
HTrans (NP :: (k1 -> Type) -> [k1] -> Type) (NP :: (k2 -> Type) -> [k2] -> Type) | |
Defined in Data.SOP.NP htrans :: forall c (xs :: l1) (ys :: l2) proxy f g. AllZipN (Prod NP) c xs ys => proxy c -> (forall (x :: k10) (y :: k20). c x y => f x -> g y) -> NP f xs -> NP g ys # hcoerce :: forall (f :: k10 -> Type) (g :: k20 -> Type) (xs :: l1) (ys :: l2). AllZipN (Prod NP) (LiftedCoercible f g) xs ys => NP f xs -> NP g ys # | |
HAp (NP :: (k -> Type) -> [k] -> Type) | |
HCollapse (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP | |
HPure (NP :: (k -> Type) -> [k] -> Type) | |
HSequence (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP hsequence' :: forall (xs :: l) f (g :: k0 -> Type). (SListIN NP xs, Applicative f) => NP (f :.: g) xs -> f (NP g xs) # hctraverse' :: forall c (xs :: l) g proxy f f'. (AllN NP c xs, Applicative g) => proxy c -> (forall (a :: k0). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) # htraverse' :: forall (xs :: l) g f f'. (SListIN NP xs, Applicative g) => (forall (a :: k0). f a -> g (f' a)) -> NP f xs -> g (NP f' xs) # | |
HTraverse_ (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP hctraverse_ :: forall c (xs :: l) g proxy f. (AllN NP c xs, Applicative g) => proxy c -> (forall (a :: k0). c a => f a -> g ()) -> NP f xs -> g () # htraverse_ :: forall (xs :: l) g f. (SListIN NP xs, Applicative g) => (forall (a :: k0). f a -> g ()) -> NP f xs -> g () # | |
(KnownSymbol alias, tys ~ '[alias ::: ty]) => Aliasable alias (expression ty) (NP (Aliased expression) tys) Source # | |
Additional (NP expr :: [a] -> Type) Source # | |
IsPGlabel label (y -> NP (K y :: Symbol -> Type) '[label]) Source # | |
aliases ~ '[alias] => IsLabel alias (NP Alias aliases) Source # | |
Defined in Squeal.PostgreSQL.Type.Alias | |
(HasUnique tab (Join from lat) row, Has col row ty, GroupedBy tab col bys, tys ~ '[ty]) => IsLabel col (NP (Expression ('Grouped bys) lat with db params from) tys) Source # | |
Defined in Squeal.PostgreSQL.Expression fromLabel :: NP (Expression ('Grouped bys) lat with db params from) tys # | |
(HasUnique tab (Join from lat) row, Has col row ty, tys ~ '[ty]) => IsLabel col (NP (Expression 'Ungrouped lat with db params from) tys) Source # | |
Defined in Squeal.PostgreSQL.Expression fromLabel :: NP (Expression 'Ungrouped lat with db params from) tys # | |
(HasUnique tab (Join from lat) row, Has col row ty, GroupedBy tab col bys, columns ~ '[col ::: ty]) => IsLabel col (NP (Aliased (Expression ('Grouped bys) lat with db params from)) columns) Source # | |
Defined in Squeal.PostgreSQL.Expression | |
(HasUnique tab (Join from lat) row, Has col row ty, columns ~ '[col ::: ty]) => IsLabel col (NP (Aliased (Expression 'Ungrouped lat with db params from)) columns) Source # | |
Defined in Squeal.PostgreSQL.Expression | |
(HasUnique rel rels cols, Has col cols ty, bys ~ '['(rel, col)]) => IsLabel col (NP (By rels) bys) Source # | |
Defined in Squeal.PostgreSQL.Query.Table | |
labels ~ '[label] => IsPGlabel label (NP PGlabel labels) Source # | |
(All (Compose Monoid f) xs, All (Compose Semigroup f) xs) => Monoid (NP f xs) | Since: sop-core-0.4.0.0 |
All (Compose Semigroup f) xs => Semigroup (NP f xs) | Since: sop-core-0.4.0.0 |
All (Compose Show f) xs => Show (NP f xs) | |
All (Compose NFData f) xs => NFData (NP f xs) | Since: sop-core-0.2.5.0 |
Defined in Data.SOP.NP | |
All (Compose Eq f) xs => Eq (NP f xs) | |
(All (Compose Eq f) xs, All (Compose Ord f) xs) => Ord (NP f xs) | |
All KnownSymbol aliases => RenderSQL (NP Alias aliases) Source # | |
Defined in Squeal.PostgreSQL.Type.Alias | |
All KnownSymbol labels => RenderSQL (NP PGlabel labels) Source # | |
Defined in Squeal.PostgreSQL.Type.Schema | |
type AllZipN (NP :: (k -> Type) -> [k] -> Type) (c :: a -> b -> Constraint) | |
Defined in Data.SOP.NP | |
type Same (NP :: (k1 -> Type) -> [k1] -> Type) | |
type Prod (NP :: (k -> Type) -> [k] -> Type) | |
type UnProd (NP :: (k -> Type) -> [k] -> Type) | |
type SListIN (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP | |
type CollapseTo (NP :: (k -> Type) -> [k] -> Type) a | |
Defined in Data.SOP.NP | |
type AllN (NP :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) | |
Defined in Data.SOP.NP |
Path
data Path (p :: k -> k -> Type) (x :: k) (y :: k) where #
A Path
with steps in p
is a singly linked list of
"type-aligned" constructions of p
.
>>>
:{
let path :: Path (->) String Int path = length :>> (\x -> x^2) :>> Done in qfold path "hello" :} 25
Done :: forall {k} (p :: k -> k -> Type) (x :: k). Path p x x | |
(:>>) :: forall {k} (p :: k -> k -> Type) (x :: k) (y1 :: k) (y :: k). p x y1 -> Path p y1 y -> Path p x y infixr 7 |
Instances
QFunctor (Path :: (k3 -> k3 -> Type) -> k3 -> k3 -> Type) | |
Defined in Control.Category.Free | |
QMonad (Path :: (k1 -> k1 -> Type) -> k1 -> k1 -> Type) | |
QPointed (Path :: (k1 -> k1 -> Type) -> k1 -> k1 -> Type) | |
Defined in Control.Category.Free | |
CFree (Path :: (k -> k -> Type) -> k -> k -> Type) | |
Defined in Control.Category.Free | |
QFoldable (Path :: (k -> k -> Type) -> k -> k -> Type) | |
Defined in Control.Category.Free qfoldMap :: forall q p (x :: k0) (y :: k0). Category q => (forall (x1 :: k0) (y1 :: k0). p x1 y1 -> q x1 y1) -> Path p x y -> q x y # qfold :: forall q (x :: k0) (y :: k0). Category q => Path q x y -> q x y # qfoldr :: forall {k1} p q (y :: k0) (z :: k1) (x :: k0). (forall (x1 :: k0) (y1 :: k0) (z1 :: k1). p x1 y1 -> q y1 z1 -> q x1 z1) -> q y z -> Path p x y -> q x z # qfoldl :: forall {k1} q p (x :: k1) (y :: k0) (z :: k0). (forall (x1 :: k1) (y1 :: k0) (z1 :: k0). q x1 y1 -> p y1 z1 -> q x1 z1) -> q x y -> Path p y z -> q x z # qtoMonoid :: forall m p (x :: k0) (y :: k0). Monoid m => (forall (x1 :: k0) (y1 :: k0). p x1 y1 -> m) -> Path p x y -> m # qtoList :: forall p a (x :: k0) (y :: k0). (forall (x1 :: k0) (y1 :: k0). p x1 y1 -> a) -> Path p x y -> [a] # qtraverse_ :: forall m q p (x :: k0) (y :: k0). (Applicative m, Category q) => (forall (x1 :: k0) (y1 :: k0). p x1 y1 -> m (q x1 y1)) -> Path p x y -> m (q x y) # | |
QTraversable (Path :: (k -> k -> Type) -> k -> k -> Type) | |
Defined in Control.Category.Free qtraverse :: forall m p q (x :: k0) (y :: k0). Applicative m => (forall (x1 :: k0) (y1 :: k0). p x1 y1 -> m (q x1 y1)) -> Path p x y -> m (Path q x y) # | |
Category (Path p :: k -> k -> Type) | |
(KnownSymbol cte, with1 ~ ((cte ::: common) ': with)) => Aliasable cte (statement with db params common) (Path (CommonTableExpression statement db params) with with1) Source # | |
Defined in Squeal.PostgreSQL.Query.With | |
x ~ y => Monoid (Path p x y) | |
x ~ y => Semigroup (Path p x y) | |
(forall (x1 :: k) (y1 :: k). Show (p x1 y1)) => Show (Path p x y) | |
Type Level List
type family Join xs ys where ... Source #
Join
is simply promoted ++
and is used in JOIN
s in
FromClause
s.
disjoin :: forall xs ys expr. SListI xs => NP expr (Join xs ys) -> (NP expr xs, NP expr ys) Source #
class Additional expr where Source #
The Additional
class is for appending
type-level list parameterized constructors such as NP
,
Selection
, and FromClause
.
Instances
Additional (NP expr :: [a] -> Type) Source # | |
Additional (FromClause lat with db params :: FromType -> Type) Source # | |
Defined in Squeal.PostgreSQL.Query.From also :: forall (ys :: [a]) (xs :: [a]). FromClause lat with db params ys -> FromClause lat with db params xs -> FromClause lat with db params (Join xs ys) Source # | |
Additional (Selection grp lat with db params from :: [(Symbol, NullType)] -> Type) Source # | |
type family In x xs :: Constraint where ... Source #
In x xs
is a constraint that proves that x
is in xs
.
type family Length (xs :: [k]) :: Nat where ... Source #
Calculate the Length
of a type level list
>>>
:kind! Length '[Char,String,Bool,Double]
Length '[Char,String,Bool,Double] :: Nat = 4
type family SubList (xs :: [k]) (ys :: [k]) :: Bool where ... Source #
SubList
checks that one type level list is a sublist of another,
with the same ordering.
>>>
:kind! SubList '[1,2,3] '[4,5,6]
SubList '[1,2,3] '[4,5,6] :: Bool = 'False>>>
:kind! SubList '[1,2,3] '[1,2,3,4]
SubList '[1,2,3] '[1,2,3,4] :: Bool = 'True>>>
:kind! SubList '[1,2,3] '[0,1,0,2,0,3]
SubList '[1,2,3] '[0,1,0,2,0,3] :: Bool = 'True>>>
:kind! SubList '[1,2,3] '[3,2,1]
SubList '[1,2,3] '[3,2,1] :: Bool = 'False
type family SubsetList (xs :: [k]) (ys :: [k]) :: Bool where ... Source #
SubsetList
checks that one type level list is a subset of another,
regardless of ordering and repeats.
>>>
:kind! SubsetList '[1,2,3] '[4,5,6]
SubsetList '[1,2,3] '[4,5,6] :: Bool = 'False>>>
:kind! SubsetList '[1,2,3] '[1,2,3,4]
SubsetList '[1,2,3] '[1,2,3,4] :: Bool = 'True>>>
:kind! SubsetList '[1,2,3] '[0,1,0,2,0,3]
SubsetList '[1,2,3] '[0,1,0,2,0,3] :: Bool = 'True>>>
:kind! SubsetList '[1,2,3] '[3,2,1]
SubsetList '[1,2,3] '[3,2,1] :: Bool = 'True>>>
:kind! SubsetList '[1,1,1] '[3,2,1]
SubsetList '[1,1,1] '[3,2,1] :: Bool = 'True
SubsetList '[] ys = 'True | |
SubsetList (x ': xs) ys = Elem x ys && SubsetList xs ys |
Type Level Sort
type family Twos (ls :: [k]) :: [[k]] where ... Source #
Two
s splits a type-level list into a list of sorted lists of length 2 (with a singelton list potentially at the end)
It is required for implementing MergeSort
type family FoldMerge (ls :: [[Symbol]]) :: [[Symbol]] where ... Source #
FoldMerge
folds over a list of sorted lists, merging them into a single sorted list
type family Merge (ls :: [Symbol]) (rs :: [Symbol]) :: [Symbol] where ... Source #
Merge
two sorted lists into one list
Merge '[] r = r | |
Merge l '[] = l | |
Merge (l ': ls) (r ': rs) = MergeHelper (l ': ls) (r ': rs) (CmpSymbol l r) |
type family MergeHelper (ls :: [Symbol]) (rs :: [Symbol]) (cmp :: Ordering) where ... Source #
MergeHelper
decides whether to take an element from the right or left list next,
depending on the result of their comparison
MergeHelper ls (r ': rs) 'GT = r ': Merge ls rs | |
MergeHelper (l ': ls) rs leq = l ': Merge ls rs |