Language.Hakaru.Syntax.IClasses

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

TODO: DeriveDataTypeable for all our newtypes?

Showing indexed types

class Show1 (a :: k -> *) where

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

show1 :: a i -> String

Instances

Show1 Value

Methods

showsPrec1 :: Int -> Value i -> ShowS

show1 :: Value i -> String

Show1 Literal

Methods

showsPrec1 :: Int -> Literal i -> ShowS

show1 :: Literal i -> String

Show1 (Sing :: Symbol -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Sing :: k -> *) => Show1 (Variable :: k -> *)

Methods

showsPrec1 :: Int -> Variable i -> ShowS

show1 :: Variable i -> String

Show1 (Sing :: HakaruCon -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Sing :: HakaruFun -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Sing :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Pattern vars :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Pattern vars i -> ShowS

show1 :: Pattern vars i -> String

Show1 ast => Show1 (Datum ast :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Datum ast i -> ShowS

show1 :: Datum ast i -> String

Show2 abt => Show1 (LC_ abt :: Hakaru -> *)

Methods

showsPrec1 :: Int -> LC_ abt i -> ShowS

show1 :: LC_ abt i -> String

Show2 abt => Show1 (Term abt :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Term abt i -> ShowS

show1 :: Term abt i -> String

Show1 (Sing :: Untyped -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show a => Show1 (Lift1 a :: k -> *)

Methods

showsPrec1 :: Int -> Lift1 a i -> ShowS

show1 :: Lift1 a i -> String

Show2 abt => Show1 (Branch a abt :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Branch a abt i -> ShowS

show1 :: Branch a abt i -> String

Show1 (PDatumFun x vars :: Hakaru -> *)

Methods

showsPrec1 :: Int -> PDatumFun x vars i -> ShowS

show1 :: PDatumFun x vars i -> String

Show1 (PDatumStruct xs vars :: Hakaru -> *)

Methods

showsPrec1 :: Int -> PDatumStruct xs vars i -> ShowS

show1 :: PDatumStruct xs vars i -> String

Show1 (PDatumCode xss vars :: Hakaru -> *)

Methods

showsPrec1 :: Int -> PDatumCode xss vars i -> ShowS

show1 :: PDatumCode xss vars i -> String

Show1 ast => Show1 (DatumFun x ast :: Hakaru -> *)

Methods

showsPrec1 :: Int -> DatumFun x ast i -> ShowS

show1 :: DatumFun x ast i -> String

Show1 ast => Show1 (DatumStruct xs ast :: Hakaru -> *)

Methods

showsPrec1 :: Int -> DatumStruct xs ast i -> ShowS

show1 :: DatumStruct xs ast i -> String

Show1 ast => Show1 (DatumCode xss ast :: Hakaru -> *)

Methods

showsPrec1 :: Int -> DatumCode xss ast i -> ShowS

show1 :: DatumCode xss ast i -> String

(Show1 ast, Show2 abt) => Show1 (MatchResult ast abt :: Hakaru -> *)

Methods

showsPrec1 :: Int -> MatchResult ast abt i -> ShowS

show1 :: MatchResult ast abt i -> String

(Show1 a, Show1 b) => Show1 (Pair1 a b :: k -> *)

Methods

showsPrec1 :: Int -> Pair1 a b i -> ShowS

show1 :: Pair1 a b i -> String

(Show1 (Sing :: k -> *), Show1 (syn (MemoizedABT syn))) => Show1 (MemoizedABT syn xs :: k -> *)

Methods

showsPrec1 :: Int -> MemoizedABT syn xs i -> ShowS

show1 :: MemoizedABT syn xs i -> String

(Show1 (Sing :: k -> *), Show1 (syn (TrivialABT syn))) => Show1 (TrivialABT syn xs :: k -> *)

Methods

showsPrec1 :: Int -> TrivialABT syn xs i -> ShowS

show1 :: TrivialABT syn xs i -> String

(Show1 (Sing :: k -> *), Show1 rec) => Show1 (View rec xs :: k -> *)

Methods

showsPrec1 :: Int -> View rec xs i -> ShowS

show1 :: View rec xs i -> String

Show a => Show1 (Lift2 a i :: k -> *)

Methods

showsPrec1 :: Int -> Lift2 a i i0 -> ShowS

show1 :: Lift2 a i i0 -> String

(Show1 (Sing :: k -> *), Show1 (syn (MetaABT meta syn)), Show meta) => Show1 (MetaABT meta syn xs :: k -> *)

Methods

showsPrec1 :: Int -> MetaABT meta syn xs i -> ShowS

show1 :: MetaABT meta syn xs i -> String

(Show2 a, Show2 b) => Show1 (Pair2 a b i :: k -> *)

Methods

showsPrec1 :: Int -> Pair2 a b i i0 -> ShowS

show1 :: Pair2 a b i i0 -> String

Show1 (Sing :: [[HakaruFun]] -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show2 abt => Show1 (SArgs abt :: [([Hakaru], Hakaru)] -> *)

Methods

showsPrec1 :: Int -> SArgs abt i -> ShowS

show1 :: SArgs abt i -> String

Show1 (Sing :: [HakaruFun] -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 a => Show1 (List1 a :: [k] -> *)

Methods

showsPrec1 :: Int -> List1 a i -> ShowS

show1 :: List1 a i -> String

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

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

class Show2 (a :: k1 -> k2 -> *) where

Minimal complete definition

showsPrec2 | show2

Methods

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

show2 :: a i j -> String

Instances

Show a => Show2 (Lift2 a :: k1 -> k2 -> *)

Methods

showsPrec2 :: Int -> Lift2 a i j -> ShowS

show2 :: Lift2 a i j -> String

(Show2 a, Show2 b) => Show2 (Pair2 a b :: k1 -> k2 -> *)

Methods

showsPrec2 :: Int -> Pair2 a b i j -> ShowS

show2 :: Pair2 a b i j -> String

Show2 Pattern

Methods

showsPrec2 :: Int -> Pattern i j -> ShowS

show2 :: Pattern i j -> String

Show2 (PDatumFun x :: [Hakaru] -> Hakaru -> *)

Methods

showsPrec2 :: Int -> PDatumFun x i j -> ShowS

show2 :: PDatumFun x i j -> String

Show2 (PDatumStruct xs :: [Hakaru] -> Hakaru -> *)

Methods

showsPrec2 :: Int -> PDatumStruct xs i j -> ShowS

show2 :: PDatumStruct xs i j -> String

Show2 (PDatumCode xss :: [Hakaru] -> Hakaru -> *)

Methods

showsPrec2 :: Int -> PDatumCode xss i j -> ShowS

show2 :: PDatumCode xss i j -> String

(Show1 (Sing :: k -> *), Show1 (syn (MemoizedABT syn))) => Show2 (MemoizedABT syn :: [k] -> k -> *)

Methods

showsPrec2 :: Int -> MemoizedABT syn i j -> ShowS

show2 :: MemoizedABT syn i j -> String

(Show1 (Sing :: k -> *), Show1 (syn (TrivialABT syn))) => Show2 (TrivialABT syn :: [k] -> k -> *)

Methods

showsPrec2 :: Int -> TrivialABT syn i j -> ShowS

show2 :: TrivialABT syn i j -> String

(Show1 (Sing :: k -> *), Show1 rec) => Show2 (View rec :: [k] -> k -> *)

Methods

showsPrec2 :: Int -> View rec i j -> ShowS

show2 :: View rec i j -> String

(Show1 (Sing :: k -> *), Show1 (syn (MetaABT meta syn)), Show meta) => Show2 (MetaABT meta syn :: [k] -> k -> *)

Methods

showsPrec2 :: Int -> MetaABT meta syn i j -> ShowS

show2 :: MetaABT meta syn i j -> String

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

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

Some more-generic helper functions for showing things

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

showTuple :: [ShowS] -> ShowS

some helpers for implementing the instances

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

Equality

class Eq1 (a :: k -> *) where

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:

1. if eq1 x y == True, then x and y have the same type index and (x == y) == True
2. if eq1 x y == False where x and y have the same type index, then (x == y) == False
3. if (x == y) == True, then eq1 x y == True
4. 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

Instances

Eq1 HContinuous

Methods

eq1 :: HContinuous i -> HContinuous i -> Bool

Eq1 HDiscrete

Methods

eq1 :: HDiscrete i -> HDiscrete i -> Bool

Eq1 HIntegrable

Methods

eq1 :: HIntegrable i -> HIntegrable i -> Bool

Eq1 HRadical

Methods

eq1 :: HRadical i -> HRadical i -> Bool

Eq1 HFractional

Methods

eq1 :: HFractional i -> HFractional i -> Bool

Eq1 HRing

Methods

eq1 :: HRing i -> HRing i -> Bool

Eq1 HSemiring

Methods

eq1 :: HSemiring i -> HSemiring i -> Bool

Eq1 Value

Methods

eq1 :: Value i -> Value i -> Bool

Eq1 NaryOp

Methods

eq1 :: NaryOp i -> NaryOp i -> Bool

Eq1 Literal

Methods

eq1 :: Literal i -> Literal i -> Bool

Eq1 (Sing :: Symbol -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 (Variable :: k -> *)

Methods

eq1 :: Variable i -> Variable i -> Bool

Eq1 (Sing :: HakaruCon -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 (Sing :: HakaruFun -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 (Sing :: Hakaru -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 (Coercion a :: Hakaru -> *)

Methods

eq1 :: Coercion a i -> Coercion a i -> Bool

Eq1 (PrimCoercion a :: Hakaru -> *)

Methods

eq1 :: PrimCoercion a i -> PrimCoercion a i -> Bool

Eq1 (Pattern vars :: Hakaru -> *)

Methods

eq1 :: Pattern vars i -> Pattern vars i -> Bool

Eq1 ast => Eq1 (Datum ast :: Hakaru -> *)

Methods

eq1 :: Datum ast i -> Datum ast i -> Bool

(ABT Term abt, JmEq2 abt) => Eq1 (Term abt :: Hakaru -> *)

Methods

eq1 :: Term abt i -> Term abt i -> Bool

Eq1 (MeasureOp typs :: Hakaru -> *)

Methods

eq1 :: MeasureOp typs i -> MeasureOp typs i -> Bool

Eq1 (ArrayOp args :: Hakaru -> *)

Methods

eq1 :: ArrayOp args i -> ArrayOp args i -> Bool

Eq1 (PrimOp args :: Hakaru -> *)

Methods

eq1 :: PrimOp args i -> PrimOp args i -> Bool

Eq1 (Sing :: Untyped -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq a => Eq1 (Lift1 a :: k -> *)

Methods

eq1 :: Lift1 a i -> Lift1 a i -> Bool

Eq2 abt => Eq1 (Reducer abt xs :: Hakaru -> *)

Methods

eq1 :: Reducer abt xs i -> Reducer abt xs i -> Bool

Eq2 abt => Eq1 (Branch a abt :: Hakaru -> *)

Methods

eq1 :: Branch a abt i -> Branch a abt i -> Bool

Eq1 (PDatumFun x vars :: Hakaru -> *)

Methods

eq1 :: PDatumFun x vars i -> PDatumFun x vars i -> Bool

Eq1 (PDatumStruct xs vars :: Hakaru -> *)

Methods

eq1 :: PDatumStruct xs vars i -> PDatumStruct xs vars i -> Bool

Eq1 (PDatumCode xss vars :: Hakaru -> *)

Methods

eq1 :: PDatumCode xss vars i -> PDatumCode xss vars i -> Bool

Eq1 ast => Eq1 (DatumFun x ast :: Hakaru -> *)

Methods

eq1 :: DatumFun x ast i -> DatumFun x ast i -> Bool

Eq1 ast => Eq1 (DatumStruct xs ast :: Hakaru -> *)

Methods

eq1 :: DatumStruct xs ast i -> DatumStruct xs ast i -> Bool

Eq1 ast => Eq1 (DatumCode xss ast :: Hakaru -> *)

Methods

eq1 :: DatumCode xss ast i -> DatumCode xss ast i -> Bool

(Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *), Foldable21 syn, JmEq1 (syn (TrivialABT syn))) => Eq1 (TrivialABT syn xs :: k -> *)

Methods

eq1 :: TrivialABT syn xs i -> TrivialABT syn xs i -> Bool

Eq a => Eq1 (Lift2 a i :: k -> *)

Methods

eq1 :: Lift2 a i i0 -> Lift2 a i i0 -> Bool

Eq1 (Sing :: [[HakaruFun]] -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq2 abt => Eq1 (SArgs abt :: [([Hakaru], Hakaru)] -> *)

Methods

eq1 :: SArgs abt i -> SArgs abt i -> Bool

Eq1 (Sing :: [HakaruFun] -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 a => Eq1 (List1 a :: [k] -> *)

Methods

eq1 :: List1 a i -> List1 a i -> Bool

class Eq2 (a :: k1 -> k2 -> *) where

Minimal complete definition

eq2

Methods

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

Instances

Eq2 Coercion

Methods

eq2 :: Coercion i j -> Coercion i j -> Bool

Eq2 PrimCoercion

Methods

eq2 :: PrimCoercion i j -> PrimCoercion i j -> Bool

Eq a => Eq2 (Lift2 a :: k1 -> k2 -> *)

Methods

eq2 :: Lift2 a i j -> Lift2 a i j -> Bool

Eq2 Pattern

Methods

eq2 :: Pattern i j -> Pattern i j -> Bool

Eq2 MeasureOp

Methods

eq2 :: MeasureOp i j -> MeasureOp i j -> Bool

Eq2 ArrayOp

Methods

eq2 :: ArrayOp i j -> ArrayOp i j -> Bool

Eq2 PrimOp

Methods

eq2 :: PrimOp i j -> PrimOp i j -> Bool

Eq2 (PDatumFun x :: [Hakaru] -> Hakaru -> *)

Methods

eq2 :: PDatumFun x i j -> PDatumFun x i j -> Bool

Eq2 (PDatumStruct xs :: [Hakaru] -> Hakaru -> *)

Methods

eq2 :: PDatumStruct xs i j -> PDatumStruct xs i j -> Bool

Eq2 (PDatumCode xss :: [Hakaru] -> Hakaru -> *)

Methods

eq2 :: PDatumCode xss i j -> PDatumCode xss i j -> Bool

(Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *), Foldable21 syn, JmEq1 (syn (TrivialABT syn))) => Eq2 (TrivialABT syn :: [k] -> k -> *)

Methods

eq2 :: TrivialABT syn i j -> TrivialABT syn i j -> Bool

data TypeEq :: k -> k -> * where

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 (TypeEq :: k -> k -> *)

Methods

id :: TypeEq a a

(.) :: TypeEq b c -> TypeEq a b -> TypeEq a c

symmetry :: TypeEq a b -> TypeEq b a

Type equality is symmetric.

transitivity :: TypeEq a b -> TypeEq b c -> TypeEq a c

Type equality is transitive. N.B., this is has a more general type than (.)

congruence :: TypeEq a b -> TypeEq (f a) (f b)

Type constructors are extensional.

class Eq1 a => JmEq1 (a :: k -> *) where

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:

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

Instances

JmEq1 HContinuous

Methods

jmEq1 :: HContinuous i -> HContinuous j -> Maybe (TypeEq i j)

JmEq1 HDiscrete

Methods

jmEq1 :: HDiscrete i -> HDiscrete j -> Maybe (TypeEq i j)

JmEq1 HIntegrable

Methods

jmEq1 :: HIntegrable i -> HIntegrable j -> Maybe (TypeEq i j)

JmEq1 HRadical

Methods

jmEq1 :: HRadical i -> HRadical j -> Maybe (TypeEq i j)

JmEq1 HFractional

Methods

jmEq1 :: HFractional i -> HFractional j -> Maybe (TypeEq i j)

JmEq1 HRing

Methods

jmEq1 :: HRing i -> HRing j -> Maybe (TypeEq i j)

JmEq1 HSemiring

Methods

jmEq1 :: HSemiring i -> HSemiring j -> Maybe (TypeEq i j)

JmEq1 NaryOp

Methods

jmEq1 :: NaryOp i -> NaryOp j -> Maybe (TypeEq i j)

JmEq1 Literal

Methods

jmEq1 :: Literal i -> Literal j -> Maybe (TypeEq i j)

JmEq1 (Sing :: Symbol -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 (Sing :: HakaruCon -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 (Sing :: HakaruFun -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 (Sing :: Hakaru -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 (PrimCoercion a :: Hakaru -> *)

Methods

jmEq1 :: PrimCoercion a i -> PrimCoercion a j -> Maybe (TypeEq i j)

Eq1 ast => JmEq1 (Datum ast :: Hakaru -> *)

Methods

jmEq1 :: Datum ast i -> Datum ast j -> Maybe (TypeEq i j)

(ABT Term abt, JmEq2 abt) => JmEq1 (Term abt :: Hakaru -> *)

Methods

jmEq1 :: Term abt i -> Term abt j -> Maybe (TypeEq i j)

JmEq1 (Sing :: Untyped -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq2 abt => JmEq1 (Reducer abt xs :: Hakaru -> *)

Methods

jmEq1 :: Reducer abt xs i -> Reducer abt xs j -> Maybe (TypeEq i j)

(Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *), JmEq1 (syn (TrivialABT syn)), Foldable21 syn) => JmEq1 (TrivialABT syn xs :: k -> *)

Methods

jmEq1 :: TrivialABT syn xs i -> TrivialABT syn xs j -> Maybe (TypeEq i j)

JmEq1 (Sing :: [[HakaruFun]] -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq2 abt => JmEq1 (SArgs abt :: [([Hakaru], Hakaru)] -> *)

Methods

jmEq1 :: SArgs abt i -> SArgs abt j -> Maybe (TypeEq i j)

JmEq1 (Sing :: [HakaruFun] -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 a => JmEq1 (List1 a :: [k] -> *)

Methods

jmEq1 :: List1 a i -> List1 a j -> Maybe (TypeEq i j)

class Eq2 a => JmEq2 (a :: k1 -> k2 -> *) where

Minimal complete definition

jmEq2

Methods

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

Instances

JmEq2 PrimCoercion

Methods

jmEq2 :: PrimCoercion i1 j1 -> PrimCoercion i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)

JmEq2 MeasureOp

Methods

jmEq2 :: MeasureOp i1 j1 -> MeasureOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)

JmEq2 ArrayOp

Methods

jmEq2 :: ArrayOp i1 j1 -> ArrayOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)

JmEq2 PrimOp

Methods

jmEq2 :: PrimOp i1 j1 -> PrimOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)

(Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *), JmEq1 (syn (TrivialABT syn)), Foldable21 syn) => JmEq2 (TrivialABT syn :: [k] -> k -> *)

Methods

jmEq2 :: TrivialABT syn i1 j1 -> TrivialABT syn i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)

Generalized abstract nonsense

class Functor11 (f :: (k1 -> *) -> k2 -> *) where

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

Instances

Functor11 Datum

Methods

fmap11 :: (forall (i :: k1). a i -> b i) -> Datum a j -> Datum b j

Functor11 (DatumFun x :: (Hakaru -> *) -> Hakaru -> *)

Methods

fmap11 :: (forall (i :: k1). a i -> b i) -> DatumFun x a j -> DatumFun x b j

Functor11 (DatumStruct xs :: (Hakaru -> *) -> Hakaru -> *)

Methods

fmap11 :: (forall (i :: k1). a i -> b i) -> DatumStruct xs a j -> DatumStruct xs b j

Functor11 (DatumCode xss :: (Hakaru -> *) -> Hakaru -> *)

Methods

fmap11 :: (forall (i :: k1). a i -> b i) -> DatumCode xss a j -> DatumCode xss b j

Functor11 (List1 :: (k1 -> *) -> [k1] -> *)

Methods

fmap11 :: (forall (i :: k10). a i -> b i) -> List1 a j -> List1 b j

newtype Fix11 (f :: (k -> *) -> k -> *) (i :: k)

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

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

Minimal complete definition

fmap12

Methods

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

Instances

Functor12 (View :: (k3 -> *) -> [k3] -> k3 -> *)

Methods

fmap12 :: (forall (i :: k1). a i -> b i) -> View a j l -> View b j l

class Functor21 (f :: (k1 -> k2 -> *) -> k3 -> *) where

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

Instances

Functor21 Term

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> Term a j -> Term b j

Functor21 Head

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> Head a j -> Head b j

Functor21 Term

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> Term a j -> Term b j

Functor21 (Branch a :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a0 h i -> b h i) -> Branch a a0 j -> Branch a b j

Functor21 (Reducer xs :: ([Untyped] -> Untyped -> *) -> Untyped -> *)

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> Reducer xs a j -> Reducer xs b j

Functor21 SArgs

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> SArgs a j -> SArgs b j

Functor21 (SArgs :: ([Untyped] -> Untyped -> *) -> [([k], k)] -> *)

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> SArgs a j -> SArgs b j

class Functor22 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where

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

Instances

Functor22 Reducer

Methods

fmap22 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> Reducer a j l -> Reducer b j l

class Functor11 f => Foldable11 (f :: (k1 -> *) -> k2 -> *) where

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

foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m

Instances

Foldable11 Datum

Methods

fold11 :: Monoid m => Datum (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k1). a i -> m) -> Datum a j -> m

Foldable11 (DatumFun x :: (Hakaru -> *) -> Hakaru -> *)

Methods

fold11 :: Monoid m => DatumFun x (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k1). a i -> m) -> DatumFun x a j -> m

Foldable11 (DatumStruct xs :: (Hakaru -> *) -> Hakaru -> *)

Methods

fold11 :: Monoid m => DatumStruct xs (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k1). a i -> m) -> DatumStruct xs a j -> m

Foldable11 (DatumCode xss :: (Hakaru -> *) -> Hakaru -> *)

Methods

fold11 :: Monoid m => DatumCode xss (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k1). a i -> m) -> DatumCode xss a j -> m

Foldable11 (List1 :: (k1 -> *) -> [k1] -> *)

Methods

fold11 :: Monoid m => List1 (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k10). a i -> m) -> List1 a j -> m

newtype Lift1 (a :: *) (i :: k)

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

Constructors

Lift1

Fields

• unLift1 :: a

Instances

Eq a => Eq1 (Lift1 a :: k -> *)

Methods

eq1 :: Lift1 a i -> Lift1 a i -> Bool

Show a => Show1 (Lift1 a :: k -> *)

Methods

showsPrec1 :: Int -> Lift1 a i -> ShowS

show1 :: Lift1 a i -> String

Eq a => Eq (Lift1 a i)

Methods

(==) :: Lift1 a i -> Lift1 a i -> Bool

(/=) :: Lift1 a i -> Lift1 a i -> Bool

Ord a => Ord (Lift1 a i)

Methods

compare :: Lift1 a i -> Lift1 a i -> Ordering

(<) :: Lift1 a i -> Lift1 a i -> Bool

(<=) :: Lift1 a i -> Lift1 a i -> Bool

(>) :: Lift1 a i -> Lift1 a i -> Bool

(>=) :: Lift1 a i -> Lift1 a i -> Bool

max :: Lift1 a i -> Lift1 a i -> Lift1 a i

min :: Lift1 a i -> Lift1 a i -> Lift1 a i

Read a => Read (Lift1 a i)

Methods

readsPrec :: Int -> ReadS (Lift1 a i)

readList :: ReadS [Lift1 a i]

readPrec :: ReadPrec (Lift1 a i)

readListPrec :: ReadPrec [Lift1 a i]

Show a => Show (Lift1 a i)

Methods

showsPrec :: Int -> Lift1 a i -> ShowS

show :: Lift1 a i -> String

showList :: [Lift1 a i] -> ShowS

class Functor12 f => Foldable12 (f :: (k1 -> *) -> k2 -> k3 -> *) where

Minimal complete definition

fold12 | foldMap12

Methods

fold12 :: Monoid m => f (Lift1 m) j l -> m

foldMap12 :: Monoid m => (forall i. a i -> m) -> f a j l -> m

Instances

Foldable12 (View :: (k3 -> *) -> [k3] -> k3 -> *)

Methods

fold12 :: Monoid m => View (Lift1 m) j l -> m

foldMap12 :: Monoid m => (forall (i :: k1). a i -> m) -> View a j l -> m

class Functor21 f => Foldable21 (f :: (k1 -> k2 -> *) -> k3 -> *) where

Minimal complete definition

fold21 | foldMap21

Methods

fold21 :: Monoid m => f (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m

Instances

Foldable21 Term

Methods

fold21 :: Monoid m => Term (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> Term a j -> m

Foldable21 Head

Methods

fold21 :: Monoid m => Head (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> Head a j -> m

Foldable21 Term

Methods

fold21 :: Monoid m => Term (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> Term a j -> m

Foldable21 (Branch a :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)

Methods

fold21 :: Monoid m => Branch a (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a0 h i -> m) -> Branch a a0 j -> m

Foldable21 (Reducer xs :: ([Untyped] -> Untyped -> *) -> Untyped -> *)

Methods

fold21 :: Monoid m => Reducer xs (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> Reducer xs a j -> m

Foldable21 SArgs

Methods

fold21 :: Monoid m => SArgs (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> SArgs a j -> m

Foldable21 (SArgs :: ([Untyped] -> Untyped -> *) -> [([k], k)] -> *)

Methods

fold21 :: Monoid m => SArgs (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> SArgs a j -> m

newtype Lift2 (a :: *) (i :: k1) (j :: k2)

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

Constructors

Lift2

Fields

• unLift2 :: a

Instances

Eq a => Eq2 (Lift2 a :: k1 -> k2 -> *)

Methods

eq2 :: Lift2 a i j -> Lift2 a i j -> Bool

Show a => Show2 (Lift2 a :: k1 -> k2 -> *)

Methods

showsPrec2 :: Int -> Lift2 a i j -> ShowS

show2 :: Lift2 a i j -> String

Eq a => Eq1 (Lift2 a i :: k -> *)

Methods

eq1 :: Lift2 a i i0 -> Lift2 a i i0 -> Bool

Show a => Show1 (Lift2 a i :: k -> *)

Methods

showsPrec1 :: Int -> Lift2 a i i0 -> ShowS

show1 :: Lift2 a i i0 -> String

Eq a => Eq (Lift2 a i j)

Methods

(==) :: Lift2 a i j -> Lift2 a i j -> Bool

(/=) :: Lift2 a i j -> Lift2 a i j -> Bool

Ord a => Ord (Lift2 a i j)

Methods

compare :: Lift2 a i j -> Lift2 a i j -> Ordering

(<) :: Lift2 a i j -> Lift2 a i j -> Bool

(<=) :: Lift2 a i j -> Lift2 a i j -> Bool

(>) :: Lift2 a i j -> Lift2 a i j -> Bool

(>=) :: Lift2 a i j -> Lift2 a i j -> Bool

max :: Lift2 a i j -> Lift2 a i j -> Lift2 a i j

min :: Lift2 a i j -> Lift2 a i j -> Lift2 a i j

Read a => Read (Lift2 a i j)

Methods

readsPrec :: Int -> ReadS (Lift2 a i j)

readList :: ReadS [Lift2 a i j]

readPrec :: ReadPrec (Lift2 a i j)

readListPrec :: ReadPrec [Lift2 a i j]

Show a => Show (Lift2 a i j)

Methods

showsPrec :: Int -> Lift2 a i j -> ShowS

show :: Lift2 a i j -> String

showList :: [Lift2 a i j] -> ShowS

class Functor22 f => Foldable22 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where

Minimal complete definition

fold22 | foldMap22

Methods

fold22 :: Monoid m => f (Lift2 m) j l -> m

foldMap22 :: Monoid m => (forall h i. a h i -> m) -> f a j l -> m

Instances

Foldable22 Reducer

Methods

fold22 :: Monoid m => Reducer (Lift2 m) j l -> m

foldMap22 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> Reducer a j l -> m

class Foldable11 t => Traversable11 (t :: (k1 -> *) -> k2 -> *) where

Minimal complete definition

traverse11

Methods

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

Instances

Traversable11 Datum

Methods

traverse11 :: Applicative f => (forall (i :: k1). a i -> f (b i)) -> Datum a j -> f (Datum b j)

Traversable11 (DatumFun x :: (Hakaru -> *) -> Hakaru -> *)

Methods

traverse11 :: Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumFun x a j -> f (DatumFun x b j)

Traversable11 (DatumStruct xs :: (Hakaru -> *) -> Hakaru -> *)

Methods

traverse11 :: Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumStruct xs a j -> f (DatumStruct xs b j)

Traversable11 (DatumCode xss :: (Hakaru -> *) -> Hakaru -> *)

Methods

traverse11 :: Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumCode xss a j -> f (DatumCode xss b j)

Traversable11 (List1 :: (k1 -> *) -> [k1] -> *)

Methods

traverse11 :: Applicative f => (forall (i :: k10). a i -> f (b i)) -> List1 a j -> f (List1 b j)

class Foldable12 t => Traversable12 (t :: (k1 -> *) -> k2 -> k3 -> *) where

Minimal complete definition

traverse12

Methods

traverse12 :: Applicative f => (forall i. a i -> f (b i)) -> t a j l -> f (t b j l)

Instances

Traversable12 (View :: (k3 -> *) -> [k3] -> k3 -> *)

Methods

traverse12 :: Applicative f => (forall (i :: k1). a i -> f (b i)) -> View a j l -> f (View b j l)

class Foldable21 t => Traversable21 (t :: (k1 -> k2 -> *) -> k3 -> *) where

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)

Instances

Traversable21 Term

Methods

traverse21 :: Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> Term a j -> f (Term b j)

Traversable21 Head

Methods

traverse21 :: Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> Head a j -> f (Head b j)

Traversable21 (Branch a :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)

Methods

traverse21 :: Applicative f => (forall (h :: k1) (i :: k2). a0 h i -> f (b h i)) -> Branch a a0 j -> f (Branch a b j)

Traversable21 SArgs

Methods

traverse21 :: Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> SArgs a j -> f (SArgs b j)

class Foldable22 t => Traversable22 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *) where

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)

Instances

Traversable22 Reducer

Methods

traverse22 :: Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> Reducer a j l -> f (Reducer b j l)

Helper types

data Some1 (a :: k -> *)

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

Constructors

Some1 !(a i)

Instances

JmEq1 a => Eq (Some1 a)

Methods

(==) :: Some1 a -> Some1 a -> Bool

(/=) :: Some1 a -> Some1 a -> Bool

Show1 a => Show (Some1 a)

Methods

showsPrec :: Int -> Some1 a -> ShowS

show :: Some1 a -> String

showList :: [Some1 a] -> ShowS

data Some2 (a :: k1 -> k2 -> *)

Existentially quantify over two indices.

Constructors

Some2 !(a i j)

Instances

Eq (Some2 Transform)

Methods

(==) :: Some2 Transform -> Some2 Transform -> Bool

(/=) :: Some2 Transform -> Some2 Transform -> Bool

JmEq2 a => Eq (Some2 a)

Methods

(==) :: Some2 a -> Some2 a -> Bool

(/=) :: Some2 a -> Some2 a -> Bool

Read (Some2 Transform)

Methods

readsPrec :: Int -> ReadS (Some2 Transform)

readList :: ReadS [Some2 Transform]

readPrec :: ReadPrec (Some2 Transform)

readListPrec :: ReadPrec [Some2 Transform]

Show2 a => Show (Some2 a)

Methods

showsPrec :: Int -> Some2 a -> ShowS

show :: Some2 a -> String

showList :: [Some2 a] -> ShowS

data Pair1 (a :: k -> *) (b :: k -> *) (i :: k)

A lazy pairing of identically k-indexed values.

Constructors

Pair1 (a i) (b i)

Instances

(Show1 a, Show1 b) => Show1 (Pair1 a b :: k -> *)

Methods

showsPrec1 :: Int -> Pair1 a b i -> ShowS

show1 :: Pair1 a b i -> String

(Show1 a, Show1 b) => Show (Pair1 a b i)

Methods

showsPrec :: Int -> Pair1 a b i -> ShowS

show :: Pair1 a b i -> String

showList :: [Pair1 a b i] -> ShowS

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)

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

Constructors

Pair2 (a i j) (b i j)

Instances

(Show2 a, Show2 b) => Show2 (Pair2 a b :: k1 -> k2 -> *)

Methods

showsPrec2 :: Int -> Pair2 a b i j -> ShowS

show2 :: Pair2 a b i j -> String

(Show2 a, Show2 b) => Show1 (Pair2 a b i :: k -> *)

Methods

showsPrec1 :: Int -> Pair2 a b i i0 -> ShowS

show1 :: Pair2 a b i i0 -> String

(Show2 a, Show2 b) => Show (Pair2 a b i j)

Methods

showsPrec :: Int -> Pair2 a b i j -> ShowS

show :: Pair2 a b i j -> String

showList :: [Pair2 a b i j] -> ShowS

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

Constructors

Pw :: f x -> g y -> Pointwise f g x y

data PointwiseP (f :: k0 -> *) (g :: k1 -> *) (xy :: (k0, k1)) where

Constructors

PwP :: f x -> g y -> PointwiseP f g '(x, y)

List types

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

Equations

'[] ++ ys = ys

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

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

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))

(++) is associative. This identity doesn't come for free but rather must be proven.

data List1 :: (k -> *) -> [k] -> * where

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 (List1 :: (k1 -> *) -> [k1] -> *)

Methods

traverse11 :: Applicative f => (forall (i :: k10). a i -> f (b i)) -> List1 a j -> f (List1 b j)

Foldable11 (List1 :: (k1 -> *) -> [k1] -> *)

Methods

fold11 :: Monoid m => List1 (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k10). a i -> m) -> List1 a j -> m

Functor11 (List1 :: (k1 -> *) -> [k1] -> *)

Methods

fmap11 :: (forall (i :: k10). a i -> b i) -> List1 a j -> List1 b j

JmEq1 a => JmEq1 (List1 a :: [k] -> *)

Methods

jmEq1 :: List1 a i -> List1 a j -> Maybe (TypeEq i j)

Eq1 a => Eq1 (List1 a :: [k] -> *)

Methods

eq1 :: List1 a i -> List1 a i -> Bool

Show1 a => Show1 (List1 a :: [k] -> *)

Methods

showsPrec1 :: Int -> List1 a i -> ShowS

show1 :: List1 a i -> String

Eq1 a => Eq (List1 a xs)

Methods

(==) :: List1 a xs -> List1 a xs -> Bool

(/=) :: List1 a xs -> List1 a xs -> Bool

Show1 a => Show (List1 a xs)

Methods

showsPrec :: Int -> List1 a xs -> ShowS

show :: List1 a xs -> String

showList :: [List1 a xs] -> ShowS

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

data List2 :: (k0 -> k1 -> *) -> [k0] -> [k1] -> * where

Lifting of relations pointwise to lists

Constructors

Nil2 :: List2 f '[] '[]

Cons2 :: f x y -> List2 f xs ys -> List2 f (x ': xs) (y ': ys)

newtype DList1 a xs

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

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)

Constraints

class All (c :: k -> Constraint) (xs :: [k]) where

Minimal complete definition

allHolds

Methods

allHolds :: List1 (Holds c) xs

Instances

All (c :: k -> Constraint) ([] :: [k])

Methods

allHolds :: List1 (Holds c) []

(All c xs, c x) => All (c :: a -> Constraint) (x ': xs :: [a])

Methods

allHolds :: List1 (Holds c) (x ': xs)

data Holds (c :: k -> Constraint) (x :: k) where

Constructors

Holds :: c x => Holds c x