| Copyright | Copyright (c) 2016 the Hakaru team |
|---|---|
| License | BSD3 |
| Maintainer | wren@community.haskell.org |
| Stability | experimental |
| Portability | GHC-only |
| Safe Haskell | None |
| Language | Haskell2010 |
Language.Hakaru.Syntax.IClasses
Description
A collection of classes generalizing standard classes in order to support indexed types.
TODO: DeriveDataTypeable for all our newtypes?
Synopsis
- class Show1 (a :: k -> *) where
- showsPrec1 :: Int -> a i -> ShowS
- show1 :: a i -> String
- shows1 :: Show1 a => a i -> ShowS
- showList1 :: Show1 a => [a i] -> ShowS
- class Show2 (a :: k1 -> k2 -> *) where
- showsPrec2 :: Int -> a i j -> ShowS
- show2 :: a i j -> String
- shows2 :: Show2 a => a i j -> ShowS
- showList2 :: Show2 a => [a i j] -> ShowS
- showListWith :: (a -> ShowS) -> [a] -> ShowS
- showTuple :: [ShowS] -> ShowS
- showParen_0 :: Show a => Int -> String -> a -> ShowS
- showParen_1 :: Show1 a => Int -> String -> a i -> ShowS
- showParen_2 :: Show2 a => Int -> String -> a i j -> ShowS
- showParen_01 :: (Show b, Show1 a) => Int -> String -> b -> a i -> ShowS
- showParen_02 :: (Show b, Show2 a) => Int -> String -> b -> a i j -> ShowS
- showParen_11 :: (Show1 a, Show1 b) => Int -> String -> a i -> b j -> ShowS
- showParen_12 :: (Show1 a, Show2 b) => Int -> String -> a i -> b j l -> ShowS
- showParen_22 :: (Show2 a, Show2 b) => Int -> String -> a i1 j1 -> b i2 j2 -> ShowS
- showParen_010 :: (Show a, Show1 b, Show c) => Int -> String -> a -> b i -> c -> ShowS
- showParen_011 :: (Show a, Show1 b, Show1 c) => Int -> String -> a -> b i -> c j -> ShowS
- showParen_111 :: (Show1 a, Show1 b, Show1 c) => Int -> String -> a i -> b j -> c k -> ShowS
- class Eq1 (a :: k -> *) where
- class Eq2 (a :: k1 -> k2 -> *) where
- data TypeEq :: k -> k -> * where
- symmetry :: TypeEq a b -> TypeEq b a
- transitivity :: TypeEq a b -> TypeEq b c -> TypeEq a c
- congruence :: TypeEq a b -> TypeEq (f a) (f b)
- class Eq1 a => JmEq1 (a :: k -> *) where
- class Eq2 a => JmEq2 (a :: k1 -> k2 -> *) where
- class Functor11 (f :: (k1 -> *) -> k2 -> *) where
- fmap11 :: (forall i. a i -> b i) -> f a j -> f b j
- newtype Fix11 (f :: (k -> *) -> k -> *) (i :: k) = Fix11 {}
- cata11 :: forall f a j. Functor11 f => (forall i. f a i -> a i) -> Fix11 f j -> a j
- ana11 :: forall f a j. Functor11 f => (forall i. a i -> f a i) -> a j -> Fix11 f j
- hylo11 :: forall f a b j. Functor11 f => (forall i. a i -> f a i) -> (forall i. f b i -> b i) -> a j -> b j
- class Functor12 (f :: (k1 -> *) -> k2 -> k3 -> *) where
- fmap12 :: (forall i. a i -> b i) -> f a j l -> f b j l
- class Functor21 (f :: (k1 -> k2 -> *) -> k3 -> *) where
- fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j
- class Functor22 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where
- fmap22 :: (forall h i. a h i -> b h i) -> f a j l -> f b j l
- class Functor11 f => Foldable11 (f :: (k1 -> *) -> k2 -> *) where
- newtype Lift1 (a :: *) (i :: k) = Lift1 {
- unLift1 :: a
- class Functor12 f => Foldable12 (f :: (k1 -> *) -> k2 -> k3 -> *) where
- class Functor21 f => Foldable21 (f :: (k1 -> k2 -> *) -> k3 -> *) where
- newtype Lift2 (a :: *) (i :: k1) (j :: k2) = Lift2 {
- unLift2 :: a
- class Functor22 f => Foldable22 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where
- class Foldable11 t => Traversable11 (t :: (k1 -> *) -> k2 -> *) where
- traverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j)
- class Foldable12 t => Traversable12 (t :: (k1 -> *) -> k2 -> k3 -> *) where
- traverse12 :: Applicative f => (forall i. a i -> f (b i)) -> t a j l -> f (t b j l)
- class Foldable21 t => Traversable21 (t :: (k1 -> k2 -> *) -> k3 -> *) where
- traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j)
- class Foldable22 t => Traversable22 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where
- traverse22 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j l -> f (t b j l)
- data Some1 (a :: k -> *) = forall i. Some1 !(a i)
- data Some2 (a :: k1 -> k2 -> *) = forall i j. Some2 !(a i j)
- data Pair1 (a :: k -> *) (b :: k -> *) (i :: k) = Pair1 (a i) (b i)
- fst1 :: Pair1 a b i -> a i
- snd1 :: Pair1 a b i -> b i
- data Pair2 (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (i :: k1) (j :: k2) = Pair2 (a i j) (b i j)
- fst2 :: Pair2 a b i j -> a i j
- snd2 :: Pair2 a b i j -> b i j
- data Pointwise (f :: k0 -> *) (g :: k1 -> *) (x :: k0) (y :: k1) where
- data PointwiseP (f :: k0 -> *) (g :: k1 -> *) (xy :: (k0, k1)) where
- PwP :: f x -> g y -> PointwiseP f g '(x, y)
- type family (xs :: [k]) ++ (ys :: [k]) :: [k] where ...
- eqAppendIdentity :: proxy xs -> TypeEq xs (xs ++ '[])
- eqAppendAssoc :: proxy1 xs -> proxy2 ys -> proxy3 zs -> TypeEq ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
- data List1 :: (k -> *) -> [k] -> * where
- append1 :: List1 a xs -> List1 a ys -> List1 a (xs ++ ys)
- data List2 :: (k0 -> k1 -> *) -> [k0] -> [k1] -> * where
- newtype DList1 a xs = DList1 {}
- toList1 :: DList1 a xs -> List1 a xs
- fromList1 :: List1 a xs -> DList1 a xs
- dnil1 :: DList1 a '[]
- dcons1 :: a x -> DList1 a xs -> DList1 a (x ': xs)
- dsnoc1 :: DList1 a xs -> a x -> DList1 a (xs ++ '[x])
- dsingleton1 :: a x -> DList1 a '[x]
- dappend1 :: DList1 a xs -> DList1 a ys -> DList1 a (xs ++ ys)
- class All (c :: k -> Constraint) (xs :: [k]) where
- data Holds (c :: k -> Constraint) (x :: k) where
Showing indexed types
class Show1 (a :: k -> *) where Source #
Uniform variant of Show for k-indexed types. This differs
from transformers:Show1 in being
polykinded, like it ought to be.
Alas, I don't think there's any way to derive instances the way
we can derive for Show.
Minimal complete definition
Instances
class Show2 (a :: k1 -> k2 -> *) where Source #
Minimal complete definition
Instances
| Show a => Show2 (Lift2 a :: k1 -> k2 -> Type) Source # | |
| (Show2 a, Show2 b) => Show2 (Pair2 a b :: k1 -> k2 -> Type) Source # | |
| Show2 Pattern Source # | |
| Show2 (PDatumFun x :: [Hakaru] -> Hakaru -> Type) Source # | |
| Show2 (PDatumStruct xs :: [Hakaru] -> Hakaru -> Type) Source # | |
Defined in Language.Hakaru.Syntax.Datum Methods showsPrec2 :: forall (i :: k1) (j :: k2). Int -> PDatumStruct xs i j -> ShowS Source # show2 :: forall (i :: k1) (j :: k2). PDatumStruct xs i j -> String Source # | |
| Show2 (PDatumCode xss :: [Hakaru] -> Hakaru -> Type) Source # | |
Defined in Language.Hakaru.Syntax.Datum Methods showsPrec2 :: forall (i :: k1) (j :: k2). Int -> PDatumCode xss i j -> ShowS Source # show2 :: forall (i :: k1) (j :: k2). PDatumCode xss i j -> String Source # | |
| (Show1 (Sing :: k -> Type), Show1 (syn (MemoizedABT syn))) => Show2 (MemoizedABT syn :: [k] -> k -> Type) Source # | |
Defined in Language.Hakaru.Syntax.ABT Methods showsPrec2 :: forall (i :: k1) (j :: k2). Int -> MemoizedABT syn i j -> ShowS Source # show2 :: forall (i :: k1) (j :: k2). MemoizedABT syn i j -> String Source # | |
| (Show1 (Sing :: k -> Type), Show1 (syn (TrivialABT syn))) => Show2 (TrivialABT syn :: [k] -> k -> Type) Source # | |
Defined in Language.Hakaru.Syntax.ABT Methods showsPrec2 :: forall (i :: k1) (j :: k2). Int -> TrivialABT syn i j -> ShowS Source # show2 :: forall (i :: k1) (j :: k2). TrivialABT syn i j -> String Source # | |
| (Show1 (Sing :: k -> Type), Show1 rec) => Show2 (View rec :: [k] -> k -> Type) Source # | |
| (Show1 (Sing :: k -> Type), Show1 (syn (MetaABT meta syn)), Show meta) => Show2 (MetaABT meta syn :: [k] -> k -> Type) Source # | |
Some more-generic helper functions for showing things
showListWith :: (a -> ShowS) -> [a] -> ShowS Source #
some helpers for implementing the instances
showParen_111 :: (Show1 a, Show1 b, Show1 c) => Int -> String -> a i -> b j -> c k -> ShowS Source #
Equality
class Eq1 (a :: k -> *) where Source #
Uniform variant of Eq for homogeneous k-indexed types.
N.B., we keep this separate from the JmEq1 class because for
some types we may be able to decide eq1 while not being able
to decide jmEq1 (e.g., if using phantom types rather than
GADTs). N.B., this function returns value/term equality! That
is, the following four laws must hold relating the Eq1 class
to the Eq class:
- if
eq1 x y == True, thenxandyhave the same type index and(x == y) == True - if
eq1 x y == Falsewherexandyhave the same type index, then(x == y) == False - if
(x == y) == True, theneq1 x y == True - if
(x == y) == False, theneq1 x y == False
Alas, I don't think there's any way to derive instances the way
we can derive for Eq.
Instances
class Eq2 (a :: k1 -> k2 -> *) where Source #
Instances
data TypeEq :: k -> k -> * where Source #
Concrete proofs of type equality. In order to make use of a
proof p :: TypeEq a b, you must pattern-match on the Refl
constructor in order to show GHC that the types a and b are
equal.
transitivity :: TypeEq a b -> TypeEq b c -> TypeEq a c Source #
Type equality is transitive. N.B., this is has a more general
type than (.)
congruence :: TypeEq a b -> TypeEq (f a) (f b) Source #
Type constructors are extensional.
class Eq1 a => JmEq1 (a :: k -> *) where Source #
Uniform variant of Eq for heterogeneous k-indexed types.
N.B., this function returns value/term equality! That is, the
following four laws must hold relating the JmEq1 class to the
Eq1 class:
- if
jmEq1 x y == Just Refl, thenxandyhave the same type index andeq1 x y == True - if
jmEq1 x y == Nothingwherexandyhave the same type index, theneq1 x y == False - if
eq1 x y == True, thenjmEq1 x y == Just Refl - if
eq1 x y == False, thenjmEq1 x y == Nothing
Alas, I don't think there's any way to derive instances the way
we can derive for Eq.
Instances
class Eq2 a => JmEq2 (a :: k1 -> k2 -> *) where Source #
Instances
| JmEq2 PrimCoercion Source # | |
Defined in Language.Hakaru.Types.Coercion Methods jmEq2 :: forall (i1 :: k1) (j1 :: k2) (i2 :: k1) (j2 :: k2). PrimCoercion i1 j1 -> PrimCoercion i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2) Source # | |
| JmEq2 MeasureOp Source # | |
| JmEq2 ArrayOp Source # | |
| JmEq2 PrimOp Source # | |
| (Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type), JmEq1 (syn (TrivialABT syn)), Foldable21 syn) => JmEq2 (TrivialABT syn :: [k] -> k -> Type) Source # | |
Defined in Language.Hakaru.Syntax.AST.Eq Methods jmEq2 :: forall (i1 :: k1) (j1 :: k2) (i2 :: k1) (j2 :: k2). TrivialABT syn i1 j1 -> TrivialABT syn i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2) Source # | |
Generalized abstract nonsense
class Functor11 (f :: (k1 -> *) -> k2 -> *) where Source #
A functor on the category of k-indexed types (i.e., from
k-indexed types to k-indexed types). We unify the two indices,
because that seems the most helpful for what we're doing; we
could, of course, offer a different variant that maps k1-indexed
types to k2-indexed types...
Alas, I don't think there's any way to derive instances the way
we can derive for Functor.
Instances
| Functor11 Datum Source # | |
| Functor11 (DatumFun x :: (Hakaru -> Type) -> Hakaru -> Type) Source # | |
| Functor11 (DatumStruct xs :: (Hakaru -> Type) -> Hakaru -> Type) Source # | |
Defined in Language.Hakaru.Syntax.Datum Methods fmap11 :: forall a b (j :: k2). (forall (i :: k1). a i -> b i) -> DatumStruct xs a j -> DatumStruct xs b j Source # | |
| Functor11 (DatumCode xss :: (Hakaru -> Type) -> Hakaru -> Type) Source # | |
| Functor11 (List1 :: (k1 -> Type) -> [k1] -> Type) Source # | |
hylo11 :: forall f a b j. Functor11 f => (forall i. a i -> f a i) -> (forall i. f b i -> b i) -> a j -> b j Source #
class Functor21 (f :: (k1 -> k2 -> *) -> k3 -> *) where Source #
A functor from (k1,k2)-indexed types to k3-indexed types.
Instances
| Functor21 Term Source # | |
| Functor21 Head Source # | |
| Functor21 Term Source # | |
| Functor21 (Branch a :: ([Hakaru] -> Hakaru -> Type) -> Hakaru -> Type) Source # | |
| Functor21 (Reducer xs :: ([Untyped] -> Untyped -> Type) -> Untyped -> Type) Source # | |
| Functor21 SArgs Source # | |
| Functor21 (SArgs :: ([Untyped] -> Untyped -> Type) -> [([k], k)] -> Type) Source # | |
class Functor22 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where Source #
A functor from (k1,k2)-indexed types to (k3,k4)-indexed types.
class Functor11 f => Foldable11 (f :: (k1 -> *) -> k2 -> *) where Source #
A foldable functor on the category of k-indexed types.
Alas, I don't think there's any way to derive instances the way
we can derive for Foldable.
Methods
fold11 :: Monoid m => f (Lift1 m) i -> m Source #
foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source #
Instances
| Foldable11 Datum Source # | |
| Foldable11 (DatumFun x :: (Hakaru -> Type) -> Hakaru -> Type) Source # | |
| Foldable11 (DatumStruct xs :: (Hakaru -> Type) -> Hakaru -> Type) Source # | |
Defined in Language.Hakaru.Syntax.Datum | |
| Foldable11 (DatumCode xss :: (Hakaru -> Type) -> Hakaru -> Type) Source # | |
| Foldable11 (List1 :: (k1 -> Type) -> [k1] -> Type) Source # | |
newtype Lift1 (a :: *) (i :: k) Source #
Any unindexed type can be lifted to be (trivially) k-indexed.
Instances
| Eq a => Eq1 (Lift1 a :: k -> Type) Source # | |
| Show a => Show1 (Lift1 a :: k -> Type) Source # | |
| Eq a => Eq (Lift1 a i) Source # | |
| Ord a => Ord (Lift1 a i) Source # | |
| Read a => Read (Lift1 a i) Source # | |
| Show a => Show (Lift1 a i) Source # | |
class Functor12 f => Foldable12 (f :: (k1 -> *) -> k2 -> k3 -> *) where Source #
Methods
fold12 :: Monoid m => f (Lift1 m) j l -> m Source #
foldMap12 :: Monoid m => (forall i. a i -> m) -> f a j l -> m Source #
class Functor21 f => Foldable21 (f :: (k1 -> k2 -> *) -> k3 -> *) where Source #
Methods
fold21 :: Monoid m => f (Lift2 m) j -> m Source #
foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m Source #
Instances
| Foldable21 Term Source # | |
| Foldable21 Head Source # | |
| Foldable21 Term Source # | |
| Foldable21 (Branch a :: ([Hakaru] -> Hakaru -> Type) -> Hakaru -> Type) Source # | |
| Foldable21 (Reducer xs :: ([Untyped] -> Untyped -> Type) -> Untyped -> Type) Source # | |
| Foldable21 SArgs Source # | |
| Foldable21 (SArgs :: ([Untyped] -> Untyped -> Type) -> [([k], k)] -> Type) Source # | |
newtype Lift2 (a :: *) (i :: k1) (j :: k2) Source #
Any unindexed type can be lifted to be (trivially) (k1,k2)-indexed.
Instances
| Eq a => Eq2 (Lift2 a :: k1 -> k2 -> Type) Source # | |
| Show a => Show2 (Lift2 a :: k1 -> k2 -> Type) Source # | |
| Eq a => Eq1 (Lift2 a i :: k -> Type) Source # | |
| Show a => Show1 (Lift2 a i :: k -> Type) Source # | |
| Eq a => Eq (Lift2 a i j) Source # | |
| Ord a => Ord (Lift2 a i j) Source # | |
Defined in Language.Hakaru.Syntax.IClasses | |
| Read a => Read (Lift2 a i j) Source # | |
| Show a => Show (Lift2 a i j) Source # | |
class Functor22 f => Foldable22 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where Source #
Methods
fold22 :: Monoid m => f (Lift2 m) j l -> m Source #
foldMap22 :: Monoid m => (forall h i. a h i -> m) -> f a j l -> m Source #
Instances
class Foldable11 t => Traversable11 (t :: (k1 -> *) -> k2 -> *) where Source #
Methods
traverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source #
Instances
| Traversable11 Datum Source # | |
Defined in Language.Hakaru.Syntax.Datum Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k1). a i -> f (b i)) -> Datum a j -> f (Datum b j) Source # | |
| Traversable11 (DatumFun x :: (Hakaru -> Type) -> Hakaru -> Type) Source # | |
Defined in Language.Hakaru.Syntax.Datum Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumFun x a j -> f (DatumFun x b j) Source # | |
| Traversable11 (DatumStruct xs :: (Hakaru -> Type) -> Hakaru -> Type) Source # | |
Defined in Language.Hakaru.Syntax.Datum Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumStruct xs a j -> f (DatumStruct xs b j) Source # | |
| Traversable11 (DatumCode xss :: (Hakaru -> Type) -> Hakaru -> Type) Source # | |
Defined in Language.Hakaru.Syntax.Datum Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumCode xss a j -> f (DatumCode xss b j) Source # | |
| Traversable11 (List1 :: (k1 -> Type) -> [k1] -> Type) Source # | |
Defined in Language.Hakaru.Syntax.IClasses Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k10). a i -> f (b i)) -> List1 a j -> f (List1 b j) Source # | |
class Foldable12 t => Traversable12 (t :: (k1 -> *) -> k2 -> k3 -> *) where Source #
Methods
traverse12 :: Applicative f => (forall i. a i -> f (b i)) -> t a j l -> f (t b j l) Source #
Instances
| Traversable12 (View :: (k3 -> Type) -> [k3] -> k3 -> Type) Source # | |
Defined in Language.Hakaru.Syntax.ABT Methods traverse12 :: forall f a b (j :: k2) (l :: k30). Applicative f => (forall (i :: k1). a i -> f (b i)) -> View a j l -> f (View b j l) Source # | |
class Foldable21 t => Traversable21 (t :: (k1 -> k2 -> *) -> k3 -> *) where Source #
Methods
traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source #
Instances
| Traversable21 Term Source # | |
Defined in Language.Hakaru.Syntax.AST Methods traverse21 :: forall f a b (j :: k3). Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> Term a j -> f (Term b j) Source # | |
| Traversable21 Head Source # | |
Defined in Language.Hakaru.Evaluation.Types Methods traverse21 :: forall f a b (j :: k3). Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> Head a j -> f (Head b j) Source # | |
| Traversable21 (Branch a :: ([Hakaru] -> Hakaru -> Type) -> Hakaru -> Type) Source # | |
Defined in Language.Hakaru.Syntax.Datum Methods traverse21 :: forall f a0 b (j :: k3). Applicative f => (forall (h :: k1) (i :: k2). a0 h i -> f (b h i)) -> Branch a a0 j -> f (Branch a b j) Source # | |
| Traversable21 SArgs Source # | |
Defined in Language.Hakaru.Syntax.SArgs Methods traverse21 :: forall f a b (j :: k3). Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> SArgs a j -> f (SArgs b j) Source # | |
class Foldable22 t => Traversable22 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where Source #
Methods
traverse22 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j l -> f (t b j l) Source #
Instances
| Traversable22 Reducer Source # | |
Defined in Language.Hakaru.Syntax.Reducer Methods traverse22 :: forall f a b (j :: k3) (l :: k4). Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> Reducer a j l -> f (Reducer b j l) Source # | |
Helper types
data Some1 (a :: k -> *) Source #
Existentially quantify over a single index.
TODO: replace SomeVariable with (Some1 Variable)
Constructors
| forall i. Some1 !(a i) |
data Some2 (a :: k1 -> k2 -> *) Source #
Existentially quantify over two indices.
Constructors
| forall i j. Some2 !(a i j) |
data Pair1 (a :: k -> *) (b :: k -> *) (i :: k) Source #
A lazy pairing of identically k-indexed values.
Constructors
| Pair1 (a i) (b i) |
data Pair2 (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (i :: k1) (j :: k2) Source #
A lazy pairing of identically (k1,k2)-indexed values.
Constructors
| Pair2 (a i j) (b i j) |
data PointwiseP (f :: k0 -> *) (g :: k1 -> *) (xy :: (k0, k1)) where Source #
Constructors
| PwP :: f x -> g y -> PointwiseP f g '(x, y) |
List types
eqAppendIdentity :: proxy xs -> TypeEq xs (xs ++ '[]) Source #
eqAppendAssoc :: proxy1 xs -> proxy2 ys -> proxy3 zs -> TypeEq ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs)) Source #
( is associative. This identity doesn't come for free
but rather must be proven.++)
data List1 :: (k -> *) -> [k] -> * where Source #
A lazy list of k-indexed elements, itself indexed by the
list of indices
Instances
| Traversable11 (List1 :: (k1 -> Type) -> [k1] -> Type) Source # | |
Defined in Language.Hakaru.Syntax.IClasses Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k10). a i -> f (b i)) -> List1 a j -> f (List1 b j) Source # | |
| Foldable11 (List1 :: (k1 -> Type) -> [k1] -> Type) Source # | |
| Functor11 (List1 :: (k1 -> Type) -> [k1] -> Type) Source # | |
| JmEq1 a => JmEq1 (List1 a :: [k] -> Type) Source # | |
| Eq1 a => Eq1 (List1 a :: [k] -> Type) Source # | |
| Show1 a => Show1 (List1 a :: [k] -> Type) Source # | |
| Eq1 a => Eq (List1 a xs) Source # | |
| Show1 a => Show (List1 a xs) Source # | |
data List2 :: (k0 -> k1 -> *) -> [k0] -> [k1] -> * where Source #
Lifting of relations pointwise to lists
A difference-list variant of List1.
dsingleton1 :: a x -> DList1 a '[x] Source #
Constraints
class All (c :: k -> Constraint) (xs :: [k]) where Source #
Instances
| All (c :: k -> Constraint) ('[] :: [k]) Source # | |
| (All c xs, c x) => All (c :: a -> Constraint) (x ': xs :: [a]) Source # | |