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

Contents

Showing indexed types
- Some more-generic helper functions for showing things
- some helpers for implementing the instances
Equality
Generalized abstract nonsense
Helper types
- List types

Description

A collection of classes generalizing standard classes in order to support indexed types.

TODO: DeriveDataTypeable for all our newtypes?

Synopsis

Showing indexed types

class Show1 a 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

showsPrec1 | show1

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

Instances

Show1 Hakaru Literal Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru Value Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Symbol (Sing Symbol) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 k (Sing k) => Show1 k (Variable k) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 HakaruCon (Sing HakaruCon) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 HakaruFun (Sing HakaruFun) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru (Sing Hakaru) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru (Pattern vars) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru ast => Show1 Hakaru (Datum ast) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show2 Hakaru [Hakaru] abt => Show1 Hakaru (LC_ abt) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show2 Hakaru [Hakaru] abt => Show1 Hakaru (Term abt) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Untyped (Sing Untyped) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show a => Show1 k (Lift1 k a) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show2 Hakaru [Hakaru] abt => Show1 Hakaru (Branch a abt) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru (PDatumFun x vars) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru (PDatumStruct xs vars) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru (PDatumCode xss vars) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru ast => Show1 Hakaru (DatumFun x ast) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru ast => Show1 Hakaru (DatumStruct xs ast) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 Hakaru ast => Show1 Hakaru (DatumCode xss ast) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show1 Hakaru ast, Show2 Hakaru [Hakaru] abt) => Show1 Hakaru (MatchResult ast abt) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show1 k a, Show1 k b) => Show1 k (Pair1 k a b) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show1 k (Sing k), Show1 k (syn (MemoizedABT k syn))) => Show1 k (MemoizedABT k syn xs) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show1 k (Sing k), Show1 k (syn (TrivialABT k syn))) => Show1 k (TrivialABT k syn xs) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show1 k (Sing k), Show1 k rec) => Show1 k (View k rec xs) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show a => Show1 k (Lift2 k k1 a i) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show1 k (Sing k), Show1 k (syn (MetaABT k meta syn)), Show meta) => Show1 k (MetaABT k meta syn xs) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show2 k k1 a, Show2 k k1 b) => Show1 k (Pair2 k k1 a b i) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 [[HakaruFun]] (Sing [[HakaruFun]]) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show2 Hakaru [Hakaru] abt => Show1 [([Hakaru], Hakaru)] (SArgs abt) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 [HakaruFun] (Sing [HakaruFun]) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Show1 k a => Show1 [k] (List1 k a) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #

shows1 :: Show1 a => a i -> ShowS Source #

showList1 :: Show1 a => [a i] -> ShowS Source #

class Show2 a where Source #

Minimal complete definition

showsPrec2 | show2

Methods

showsPrec2 :: Int -> a i j -> ShowS Source #

show2 :: a i j -> String Source #

Instances

Show a => Show2 k2 k1 (Lift2 k2 k1 a) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
(Show2 k2 k1 a, Show2 k2 k1 b) => Show2 k2 k1 (Pair2 k2 k1 a b) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
Show2 Hakaru [Hakaru] Pattern Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
Show2 Hakaru [Hakaru] (PDatumFun x) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
Show2 Hakaru [Hakaru] (PDatumStruct xs) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
Show2 Hakaru [Hakaru] (PDatumCode xss) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
(Show1 k (Sing k), Show1 k (syn (MemoizedABT k syn))) => Show2 k [k] (MemoizedABT k syn) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
(Show1 k (Sing k), Show1 k (syn (TrivialABT k syn))) => Show2 k [k] (TrivialABT k syn) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
(Show1 k (Sing k), Show1 k rec) => Show2 k [k] (View k rec) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
(Show1 k (Sing k), Show1 k (syn (MetaABT k meta syn)), Show meta) => Show2 k [k] (MetaABT k meta syn) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #

shows2 :: Show2 a => a i j -> ShowS Source #

showList2 :: Show2 a => [a i j] -> ShowS Source #

Some more-generic helper functions for showing things

showListWith :: (a -> ShowS) -> [a] -> ShowS Source #

showTuple :: [ShowS] -> ShowS Source #

some helpers for implementing the instances

showParen_0 :: Show a => Int -> String -> a -> ShowS Source #

showParen_1 :: Show1 a => Int -> String -> a i -> ShowS Source #

showParen_2 :: Show2 a => Int -> String -> a i j -> ShowS Source #

showParen_01 :: (Show b, Show1 a) => Int -> String -> b -> a i -> ShowS Source #

showParen_02 :: (Show b, Show2 a) => Int -> String -> b -> a i j -> ShowS Source #

showParen_11 :: (Show1 a, Show1 b) => Int -> String -> a i -> b j -> ShowS Source #

showParen_12 :: (Show1 a, Show2 b) => Int -> String -> a i -> b j l -> ShowS Source #

showParen_22 :: (Show2 a, Show2 b) => Int -> String -> a i1 j1 -> b i2 j2 -> ShowS Source #

showParen_010 :: (Show a, Show1 b, Show c) => Int -> String -> a -> b i -> c -> ShowS Source #

showParen_011 :: (Show a, Show1 b, Show1 c) => Int -> String -> a -> b i -> c j -> ShowS Source #

showParen_111 :: (Show1 a, Show1 b, Show1 c) => Int -> String -> a i -> b j -> c k -> ShowS Source #

Equality

class Eq1 a 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, then x and y have the same type index and (x == y) == True
if eq1 x y == False where x and y have the same type index, then (x == y) == False
if (x == y) == True, then eq1 x y == True
if (x == y) == False, then eq1 x y == False

Alas, I don't think there's any way to derive instances the way we can derive for Eq.

Minimal complete definition

eq1

Methods

eq1 :: a i -> a i -> Bool Source #

Instances

Eq1 Hakaru HContinuous Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru HDiscrete Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru HIntegrable Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru HRadical Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru HFractional Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru HRing Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru HSemiring Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru NaryOp Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru Literal Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru Value Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Symbol (Sing Symbol) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 k (Variable k) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 HakaruCon (Sing HakaruCon) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 HakaruFun (Sing HakaruFun) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (Sing Hakaru) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (Coercion a) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (PrimCoercion a) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (Pattern vars) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru ast => Eq1 Hakaru (Datum ast) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (MeasureOp typs) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (ArrayOp args) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (PrimOp args) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Untyped (Sing Untyped) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq a => Eq1 k (Lift1 k a) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq2 Hakaru [Hakaru] abt => Eq1 Hakaru (Branch a abt) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (PDatumFun x vars) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (PDatumStruct xs vars) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru (PDatumCode xss vars) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru ast => Eq1 Hakaru (DatumFun x ast) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru ast => Eq1 Hakaru (DatumStruct xs ast) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 Hakaru ast => Eq1 Hakaru (DatumCode xss ast) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq a => Eq1 k (Lift2 k k1 a i) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 [[HakaruFun]] (Sing [[HakaruFun]]) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq2 Hakaru [Hakaru] abt => Eq1 [([Hakaru], Hakaru)] (SArgs abt) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 [HakaruFun] (Sing [HakaruFun]) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Eq1 k a => Eq1 [k] (List1 k a) Source #
Methods eq1 :: a i -> a i -> Bool Source #

class Eq2 a where Source #

Minimal complete definition

eq2

Methods

eq2 :: a i j -> a i j -> Bool Source #

Instances

Eq2 Hakaru Hakaru Coercion Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq2 Hakaru Hakaru PrimCoercion Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq a => Eq2 k2 k1 (Lift2 k2 k1 a) Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq2 Hakaru [Hakaru] Pattern Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq2 Hakaru [Hakaru] MeasureOp Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq2 Hakaru [Hakaru] ArrayOp Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq2 Hakaru [Hakaru] PrimOp Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq2 Hakaru [Hakaru] (PDatumFun x) Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq2 Hakaru [Hakaru] (PDatumStruct xs) Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq2 Hakaru [Hakaru] (PDatumCode xss) Source #
Methods eq2 :: a i j -> a i j -> Bool Source #

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.

Constructors

Refl :: TypeEq a a

Instances

Category k (TypeEq k) Source #
Methods id :: cat a a # (.) :: cat b c -> cat a b -> cat a c #

symmetry :: TypeEq a b -> TypeEq b a Source #

Type equality is symmetric.

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 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, then x and y have the same type index and eq1 x y == True
if jmEq1 x y == Nothing where x and y have the same type index, then eq1 x y == False
if eq1 x y == True, then jmEq1 x y == Just Refl
if eq1 x y == False, then jmEq1 x y == Nothing

Alas, I don't think there's any way to derive instances the way we can derive for Eq.

Minimal complete definition

jmEq1

Methods

jmEq1 :: a i -> a j -> Maybe (TypeEq i j) Source #

Instances

JmEq1 Hakaru HContinuous Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq HContinuous i j) Source #
JmEq1 Hakaru HDiscrete Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq HDiscrete i j) Source #
JmEq1 Hakaru HIntegrable Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq HIntegrable i j) Source #
JmEq1 Hakaru HRadical Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq HRadical i j) Source #
JmEq1 Hakaru HFractional Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq HFractional i j) Source #
JmEq1 Hakaru HRing Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq HRing i j) Source #
JmEq1 Hakaru HSemiring Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq HSemiring i j) Source #
JmEq1 Hakaru NaryOp Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq NaryOp i j) Source #
JmEq1 Hakaru Literal Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq Literal i j) Source #
JmEq1 Symbol (Sing Symbol) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (Sing Symbol) i j) Source #
JmEq1 HakaruCon (Sing HakaruCon) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (Sing HakaruCon) i j) Source #
JmEq1 HakaruFun (Sing HakaruFun) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (Sing HakaruFun) i j) Source #
JmEq1 Hakaru (Sing Hakaru) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (Sing Hakaru) i j) Source #
JmEq1 Hakaru (PrimCoercion a) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (PrimCoercion a) i j) Source #
Eq1 Hakaru ast => JmEq1 Hakaru (Datum ast) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (Datum ast) i j) Source #
JmEq1 Untyped (Sing Untyped) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (Sing Untyped) i j) Source #
JmEq1 [[HakaruFun]] (Sing [[HakaruFun]]) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (Sing [[HakaruFun]]) i j) Source #
JmEq1 [HakaruFun] (Sing [HakaruFun]) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (Sing [HakaruFun]) i j) Source #
JmEq1 k a => JmEq1 [k] (List1 k a) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (List1 k a) i j) Source #

class Eq2 a => JmEq2 a where Source #

Minimal complete definition

jmEq2

Methods

jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2) Source #

Instances

JmEq2 Hakaru Hakaru PrimCoercion Source #
Methods jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq PrimCoercion j1 j2) Source #
JmEq2 Hakaru [Hakaru] MeasureOp Source #
Methods jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq MeasureOp j1 j2) Source #
JmEq2 Hakaru [Hakaru] ArrayOp Source #
Methods jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq ArrayOp j1 j2) Source #
JmEq2 Hakaru [Hakaru] PrimOp Source #
Methods jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq PrimOp j1 j2) Source #

Generalized abstract nonsense

class Functor11 f 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.

Minimal complete definition

fmap11

Methods

fmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source #

Instances

Functor11 Hakaru Hakaru Datum Source #
Methods fmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source #
Functor11 Hakaru Hakaru (DatumFun x) Source #
Methods fmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source #
Functor11 Hakaru Hakaru (DatumStruct xs) Source #
Methods fmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source #
Functor11 Hakaru Hakaru (DatumCode xss) Source #
Methods fmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source #
Functor11 [k1] k1 (List1 k1) Source #
Methods fmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source #

newtype Fix11 f i Source #

Constructors

Fix11
Fields unFix11 :: f (Fix11 f) i

cata11 :: forall f a j. Functor11 f => (forall i. f a i -> a i) -> Fix11 f j -> a j Source #

ana11 :: forall f a j. Functor11 f => (forall i. a i -> f a i) -> a j -> Fix11 f j 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 Functor12 f where Source #

Minimal complete definition

fmap12

Methods

fmap12 :: (forall i. a i -> b i) -> f a j l -> f b j l Source #

Instances

Functor12 k3 [k3] k3 (View k3) Source #
Methods fmap12 :: (forall i. a i -> b i) -> f a j l -> f b j l Source #

class Functor21 f where Source #

A functor from (k1,k2)-indexed types to k3-indexed types.

Minimal complete definition

fmap21

Methods

fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source #

Instances

Functor21 Hakaru Hakaru [Hakaru] Term Source #
Methods fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source #
Functor21 Hakaru Hakaru [Hakaru] Lazy Source #
Methods fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source #
Functor21 Hakaru Hakaru [Hakaru] Whnf Source #
Methods fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source #
Functor21 Hakaru Hakaru [Hakaru] Head Source #
Methods fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source #
Functor21 Untyped Untyped [Untyped] Term Source #
Methods fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source #
Functor21 Hakaru Hakaru [Hakaru] (Branch a) Source #
Methods fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source #
Functor21 [([Hakaru], Hakaru)] Hakaru [Hakaru] SArgs Source #
Methods fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source #

class Functor22 f where Source #

A functor from (k1,k2)-indexed types to (k3,k4)-indexed types.

Minimal complete definition

fmap22

Methods

fmap22 :: (forall h i. a h i -> b h i) -> f a j l -> f b j l Source #

class Functor11 f => Foldable11 f 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.

Minimal complete definition

fold11 | foldMap11

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 Hakaru Hakaru Datum Source #
Methods fold11 :: Monoid m => f (Lift1 k1 m) i -> m Source # foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source #
Foldable11 Hakaru Hakaru (DatumFun x) Source #
Methods fold11 :: Monoid m => f (Lift1 k1 m) i -> m Source # foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source #
Foldable11 Hakaru Hakaru (DatumStruct xs) Source #
Methods fold11 :: Monoid m => f (Lift1 k1 m) i -> m Source # foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source #
Foldable11 Hakaru Hakaru (DatumCode xss) Source #
Methods fold11 :: Monoid m => f (Lift1 k1 m) i -> m Source # foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source #
Foldable11 [k1] k1 (List1 k1) Source #
Methods fold11 :: Monoid m => f (Lift1 k1 m) i -> m Source # foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source #

newtype Lift1 a i Source #

Any unindexed type can be lifted to be (trivially) k-indexed.

Constructors

Lift1
Fields unLift1 :: a

Instances

Eq a => Eq1 k (Lift1 k a) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Show a => Show1 k (Lift1 k a) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Eq a => Eq (Lift1 k a i) Source #
Methods (==) :: Lift1 k a i -> Lift1 k a i -> Bool # (/=) :: Lift1 k a i -> Lift1 k a i -> Bool #
Ord a => Ord (Lift1 k a i) Source #
Methods compare :: Lift1 k a i -> Lift1 k a i -> Ordering # (<) :: Lift1 k a i -> Lift1 k a i -> Bool # (<=) :: Lift1 k a i -> Lift1 k a i -> Bool # (>) :: Lift1 k a i -> Lift1 k a i -> Bool # (>=) :: Lift1 k a i -> Lift1 k a i -> Bool # max :: Lift1 k a i -> Lift1 k a i -> Lift1 k a i # min :: Lift1 k a i -> Lift1 k a i -> Lift1 k a i #
Read a => Read (Lift1 k a i) Source #
Methods readsPrec :: Int -> ReadS (Lift1 k a i) # readList :: ReadS [Lift1 k a i] # readPrec :: ReadPrec (Lift1 k a i) # readListPrec :: ReadPrec [Lift1 k a i] #
Show a => Show (Lift1 k a i) Source #
Methods showsPrec :: Int -> Lift1 k a i -> ShowS # show :: Lift1 k a i -> String # showList :: [Lift1 k a i] -> ShowS #

class Functor21 f => Foldable21 f where Source #

Minimal complete definition

fold21 | foldMap21

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 Hakaru Hakaru [Hakaru] Term Source #
Methods fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m Source # foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m Source #
Foldable21 Hakaru Hakaru [Hakaru] Lazy Source #
Methods fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m Source # foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m Source #
Foldable21 Hakaru Hakaru [Hakaru] Whnf Source #
Methods fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m Source # foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m Source #
Foldable21 Hakaru Hakaru [Hakaru] Head Source #
Methods fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m Source # foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m Source #
Foldable21 Untyped Untyped [Untyped] Term Source #
Methods fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m Source # foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m Source #
Foldable21 Hakaru Hakaru [Hakaru] (Branch a) Source #
Methods fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m Source # foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m Source #
Foldable21 [([Hakaru], Hakaru)] Hakaru [Hakaru] SArgs Source #
Methods fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m Source # foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m Source #

newtype Lift2 a i j Source #

Any unindexed type can be lifted to be (trivially) (k1,k2)-indexed.

Constructors

Lift2
Fields unLift2 :: a

Instances

Eq a => Eq2 k2 k1 (Lift2 k2 k1 a) Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Show a => Show2 k2 k1 (Lift2 k2 k1 a) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
Eq a => Eq1 k (Lift2 k k1 a i) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Show a => Show1 k (Lift2 k k1 a i) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Eq a => Eq (Lift2 k2 k1 a i j) Source #
Methods (==) :: Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j -> Bool # (/=) :: Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j -> Bool #
Ord a => Ord (Lift2 k2 k1 a i j) Source #
Methods compare :: Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j -> Ordering # (<) :: Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j -> Bool # (<=) :: Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j -> Bool # (>) :: Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j -> Bool # (>=) :: Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j -> Bool # max :: Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j # min :: Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j -> Lift2 k2 k1 a i j #
Read a => Read (Lift2 k2 k1 a i j) Source #
Methods readsPrec :: Int -> ReadS (Lift2 k2 k1 a i j) # readList :: ReadS [Lift2 k2 k1 a i j] # readPrec :: ReadPrec (Lift2 k2 k1 a i j) # readListPrec :: ReadPrec [Lift2 k2 k1 a i j] #
Show a => Show (Lift2 k2 k1 a i j) Source #
Methods showsPrec :: Int -> Lift2 k2 k1 a i j -> ShowS # show :: Lift2 k2 k1 a i j -> String # showList :: [Lift2 k2 k1 a i j] -> ShowS #

class Functor22 f => Foldable22 f where Source #

Minimal complete definition

fold22 | foldMap22

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 #

class Foldable11 t => Traversable11 t where Source #

Minimal complete definition

traverse11

Methods

traverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source #

Instances

Traversable11 Hakaru Hakaru Datum Source #
Methods traverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source #
Traversable11 Hakaru Hakaru (DatumFun x) Source #
Methods traverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source #
Traversable11 Hakaru Hakaru (DatumStruct xs) Source #
Methods traverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source #
Traversable11 Hakaru Hakaru (DatumCode xss) Source #
Methods traverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source #
Traversable11 [k1] k1 (List1 k1) Source #
Methods traverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source #

class Foldable21 t => Traversable21 t where Source #

Minimal complete definition

traverse21

Methods

traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source #

Instances

Traversable21 Hakaru Hakaru [Hakaru] Term Source #
Methods traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source #
Traversable21 Hakaru Hakaru [Hakaru] Lazy Source #
Methods traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source #
Traversable21 Hakaru Hakaru [Hakaru] Whnf Source #
Methods traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source #
Traversable21 Hakaru Hakaru [Hakaru] Head Source #
Methods traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source #
Traversable21 Hakaru Hakaru [Hakaru] (Branch a) Source #
Methods traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source #
Traversable21 [([Hakaru], Hakaru)] Hakaru [Hakaru] SArgs Source #
Methods traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source #

class Foldable22 t => Traversable22 t where Source #

Minimal complete definition

traverse22

Methods

traverse22 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j l -> f (t b j l) Source #

Helper types

data Some1 a Source #

Existentially quantify over a single index. TODO: replace SomeVariable with (Some1 Variable)

Constructors

Some1 !(a i)

Instances

JmEq1 k a => Eq (Some1 k a) Source #
Methods (==) :: Some1 k a -> Some1 k a -> Bool # (/=) :: Some1 k a -> Some1 k a -> Bool #
Show1 k a => Show (Some1 k a) Source #
Methods showsPrec :: Int -> Some1 k a -> ShowS # show :: Some1 k a -> String # showList :: [Some1 k a] -> ShowS #

data Some2 a Source #

Existentially quantify over two indices.

Constructors

Some2 !(a i j)

Instances

JmEq2 k2 k1 a => Eq (Some2 k2 k1 a) Source #
Methods (==) :: Some2 k2 k1 a -> Some2 k2 k1 a -> Bool # (/=) :: Some2 k2 k1 a -> Some2 k2 k1 a -> Bool #
Show2 k2 k1 a => Show (Some2 k2 k1 a) Source #
Methods showsPrec :: Int -> Some2 k2 k1 a -> ShowS # show :: Some2 k2 k1 a -> String # showList :: [Some2 k2 k1 a] -> ShowS #

data Pair1 a b i Source #

A lazy pairing of identically k-indexed values.

Constructors

Pair1 (a i) (b i)

Instances

(Show1 k a, Show1 k b) => Show1 k (Pair1 k a b) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show1 k a, Show1 k b) => Show (Pair1 k a b i) Source #
Methods showsPrec :: Int -> Pair1 k a b i -> ShowS # show :: Pair1 k a b i -> String # showList :: [Pair1 k a b i] -> ShowS #

fst1 :: Pair1 a b i -> a i Source #

snd1 :: Pair1 a b i -> b i Source #

data Pair2 a b i j Source #

A lazy pairing of identically (k1,k2)-indexed values.

Constructors

Pair2 (a i j) (b i j)

Instances

(Show2 k2 k1 a, Show2 k2 k1 b) => Show2 k2 k1 (Pair2 k2 k1 a b) Source #
Methods showsPrec2 :: Int -> a i j -> ShowS Source # show2 :: a i j -> String Source #
(Show2 k k1 a, Show2 k k1 b) => Show1 k (Pair2 k k1 a b i) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show2 k2 k1 a, Show2 k2 k1 b) => Show (Pair2 k2 k1 a b i j) Source #
Methods showsPrec :: Int -> Pair2 k2 k1 a b i j -> ShowS # show :: Pair2 k2 k1 a b i j -> String # showList :: [Pair2 k2 k1 a b i j] -> ShowS #

fst2 :: Pair2 a b i j -> a i j Source #

snd2 :: Pair2 a b i j -> b i j Source #

List types

type family (xs :: [k]) ++ (ys :: [k]) :: [k] where ... Source #

Equations

'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)

eqAppendIdentity :: proxy xs -> TypeEq xs (xs ++ '[]) Source #

The empty list is (also) a right-identity for (++). Because we define (++) by induction on the first argument, this identity doesn't come for free but rather must be proven.

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

Constructors

Nil1 :: List1 a '[]
Cons1 :: a x -> List1 a xs -> List1 a (x ': xs) infixr 5

Instances

Traversable11 [k1] k1 (List1 k1) Source #
Methods traverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source #
Foldable11 [k1] k1 (List1 k1) Source #
Methods fold11 :: Monoid m => f (Lift1 k1 m) i -> m Source # foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source #
Functor11 [k1] k1 (List1 k1) Source #
Methods fmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source #
JmEq1 k a => JmEq1 [k] (List1 k a) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (List1 k a) i j) Source #
Eq1 k a => Eq1 [k] (List1 k a) Source #
Methods eq1 :: a i -> a i -> Bool Source #
Show1 k a => Show1 [k] (List1 k a) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
Eq1 k a => Eq (List1 k a xs) Source #
Methods (==) :: List1 k a xs -> List1 k a xs -> Bool # (/=) :: List1 k a xs -> List1 k a xs -> Bool #
Show1 k a => Show (List1 k a xs) Source #
Methods showsPrec :: Int -> List1 k a xs -> ShowS # show :: List1 k a xs -> String # showList :: [List1 k a xs] -> ShowS #

append1 :: List1 a xs -> List1 a ys -> List1 a (xs ++ ys) Source #

newtype DList1 a xs Source #

A difference-list variant of List1.

Constructors

DList1
Fields unDList1 :: forall ys. List1 a ys -> List1 a (xs ++ ys)

toList1 :: DList1 a xs -> List1 a xs Source #

fromList1 :: List1 a xs -> DList1 a xs Source #

dnil1 :: DList1 a '[] Source #

dcons1 :: a x -> DList1 a xs -> DList1 a (x ': xs) Source #

dsnoc1 :: DList1 a xs -> a x -> DList1 a (xs ++ '[x]) Source #

dsingleton1 :: a x -> DList1 a '[x] Source #

dappend1 :: DList1 a xs -> DList1 a ys -> DList1 a (xs ++ ys) Source #