hakaru-0.3.0: A probabilistic programming language

CopyrightCopyright (c) 2016 the Hakaru team
LicenseBSD3
Maintainerwren@community.haskell.org
Stabilityexperimental
PortabilityGHC-only
Safe HaskellNone
LanguageHaskell2010

Language.Hakaru.Syntax.IClasses

Contents

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 #

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:

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

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

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

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

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

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 #