NType

General definitions

type family AllConstrained c ts :: Constraint where ...

Equations

AllConstrained c '[] = ()

AllConstrained c (t ': ts) = (c t, AllConstrained c ts)

type family IdentityElement (tensor :: Type -> Type -> Type)

Instances

type IdentityElement Either

Defined in NType

type IdentityElement Either = Void

type IdentityElement (,)

Defined in NType

type IdentityElement (,) = ()

class MonoidOf tensor m where

Minimal complete definition

mu, eta

Methods

mu :: tensor m m -> m

eta :: IdentityElement tensor -> m

Instances

MonoidOf Either m

Defined in NType

Methods

mu :: Either m m -> m

eta :: IdentityElement Either -> m

Monoid m => MonoidOf (,) m

Defined in NType

Methods

mu :: (m, m) -> m

eta :: IdentityElement (,) -> m

data N :: (Type -> Type -> Type) -> (k -> Type) -> [k] -> Type where

Constructors

Base :: !(IdentityElement tensor) -> N tensor f '[]

Step :: !(tensor (f x) (N tensor f xs)) -> N tensor f (x ': xs)

Instances

Eq (tensor (f x) (N tensor f xs)) => Eq (N tensor f (x ': xs))

Defined in NType

Methods

(==) :: N tensor f (x ': xs) -> N tensor f (x ': xs) -> Bool

(/=) :: N tensor f (x ': xs) -> N tensor f (x ': xs) -> Bool

Eq (IdentityElement tensor) => Eq (N tensor f ([] :: [k]))

Defined in NType

Methods

(==) :: N tensor f [] -> N tensor f [] -> Bool

(/=) :: N tensor f [] -> N tensor f [] -> Bool

Ord (tensor (f x) (N tensor f xs)) => Ord (N tensor f (x ': xs))

Defined in NType

Methods

compare :: N tensor f (x ': xs) -> N tensor f (x ': xs) -> Ordering

(<) :: N tensor f (x ': xs) -> N tensor f (x ': xs) -> Bool

(<=) :: N tensor f (x ': xs) -> N tensor f (x ': xs) -> Bool

(>) :: N tensor f (x ': xs) -> N tensor f (x ': xs) -> Bool

(>=) :: N tensor f (x ': xs) -> N tensor f (x ': xs) -> Bool

max :: N tensor f (x ': xs) -> N tensor f (x ': xs) -> N tensor f (x ': xs)

min :: N tensor f (x ': xs) -> N tensor f (x ': xs) -> N tensor f (x ': xs)

Ord (IdentityElement tensor) => Ord (N tensor f ([] :: [k]))

Defined in NType

Methods

compare :: N tensor f [] -> N tensor f [] -> Ordering

(<) :: N tensor f [] -> N tensor f [] -> Bool

(<=) :: N tensor f [] -> N tensor f [] -> Bool

(>) :: N tensor f [] -> N tensor f [] -> Bool

(>=) :: N tensor f [] -> N tensor f [] -> Bool

max :: N tensor f [] -> N tensor f [] -> N tensor f []

min :: N tensor f [] -> N tensor f [] -> N tensor f []

Show (tensor (f x) (N tensor f xs)) => Show (N tensor f (x ': xs))

Defined in NType

Methods

showsPrec :: Int -> N tensor f (x ': xs) -> ShowS

show :: N tensor f (x ': xs) -> String

showList :: [N tensor f (x ': xs)] -> ShowS

Show (IdentityElement tensor) => Show (N tensor f ([] :: [k]))

Defined in NType

Methods

showsPrec :: Int -> N tensor f [] -> ShowS

show :: N tensor f [] -> String

showList :: [N tensor f []] -> ShowS

nmap :: forall f g tensor. Bifunctor tensor => (forall x. f x -> g x) -> forall xs. N tensor f xs -> N tensor g xs

nmapConstrained :: forall c f g tensor. Bifunctor tensor => (forall x. c x => f x -> g x) -> forall xs. AllConstrained c xs => N tensor f xs -> N tensor g xs

nfold :: forall f r tensor. (Bifunctor tensor, MonoidOf tensor r) => (forall x. f x -> r) -> forall xs. N tensor f xs -> r

nfoldConstrained :: forall c f r tensor. (Bifunctor tensor, MonoidOf tensor r) => (forall x. c x => f x -> r) -> forall xs. AllConstrained c xs => N tensor f xs -> r

Product types

type Rec = N (,)

rmap :: forall f g. (forall x. f x -> g x) -> forall xs. Rec f xs -> Rec g xs

rmapConstrained :: forall c f g. (forall x. c x => f x -> g x) -> forall xs. AllConstrained c xs => Rec f xs -> Rec g xs

rfold :: forall f r. Monoid r => (forall x. f x -> r) -> forall xs. Rec f xs -> r

rfoldConstrained :: forall c f r. Monoid r => (forall x. c x => f x -> r) -> forall xs. AllConstrained c xs => Rec f xs -> r

rget :: forall f xs a. Elem xs a => Rec f xs -> f a

type HList = Rec Identity

type Spine = Rec Proxy

class KnownSpine xs where

Minimal complete definition

knownSpine

Methods

knownSpine :: Spine xs

Instances

KnownSpine ([] :: [k])

Defined in NType

Methods

knownSpine :: Spine []

KnownSpine xs => KnownSpine (x ': xs :: [k])

Defined in NType

Methods

knownSpine :: Spine (x ': xs)

Sum types

type Union = N Either

umap :: forall f g. (forall x. f x -> g x) -> forall xs. Union f xs -> Union g xs

umapConstrained :: forall c f g. (forall x. c x => f x -> g x) -> forall xs. AllConstrained c xs => Union f xs -> Union g xs

ufold :: forall f r. (forall x. f x -> r) -> forall xs. Union f xs -> r

ufoldConstrained :: forall c f r. (forall x. c x => f x -> r) -> forall xs. AllConstrained c xs => Union f xs -> r

umatch :: forall f xs a. Elem xs a => Union f xs -> Maybe (f a)

ulift :: forall f xs a. Elem xs a => f a -> Union f xs

type OpenUnion = Union Identity

type ElemEv a = Union ((:~:) a)

class Elem' (Index x xs) x xs => Elem xs x

Instances

Elem' (Index x xs) x xs => Elem (xs :: [k]) (x :: k)

Defined in NType

elemEv :: forall xs a. Elem xs a => ElemEv a xs