Safe Haskell	None
Language	Haskell2010

ADP.Fusion.Core.TyLvlIx

Description

Type-level indexing functionality

Synopsis

type family ToNat x :: Nat
type GetIx l r = ResolvedIx l r (CmpNat (ToNat l) (ToNat r))
type GetIndex l r = GetIndexGo l r (CmpNat (ToNat l) (ToNat r))
class GetIndexGo ixTy myTy (cmp :: Ordering) where
- type ResolvedIx ixTy myTy cmp :: *
- getIndexGo :: ixTy -> Proxy myTy -> Proxy cmp -> ResolvedIx ixTy myTy cmp
getIndex :: forall ixTy myTy. GetIndex ixTy myTy => ixTy -> Proxy myTy -> GetIx ixTy myTy
module GHC.TypeLits

Documentation

type family ToNat x :: Nat Source #

Given some index structure x, return the dimensional number in Nats.

Instances

type ToNat Z Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx type ToNat Z = 0
type ToNat (RunningIndex Z) Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx type ToNat (RunningIndex Z) = 0
type ToNat (RunningIndex (is :. i)) Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx type ToNat (RunningIndex (is :. i)) = ToNat (RunningIndex is) + 1
type ToNat (is :. i) Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx type ToNat (is :. i) = ToNat is + 1

type GetIx l r = ResolvedIx l r (CmpNat (ToNat l) (ToNat r)) Source #

type GetIndex l r = GetIndexGo l r (CmpNat (ToNat l) (ToNat r)) Source #

Wrap GetIndexGo and the type-level shenanigans.

class GetIndexGo ixTy myTy (cmp :: Ordering) where Source #

Given some complete index list ixTy and some lower-dimensional version myTy, walk down along ixTy until we have is:.i ~ ms:.m and return m.

Associated Types

type ResolvedIx ixTy myTy cmp :: * Source #

Methods

getIndexGo :: ixTy -> Proxy myTy -> Proxy cmp -> ResolvedIx ixTy myTy cmp Source #

Instances

GetIndexGo Z Z EQ Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx Associated Types type ResolvedIx Z Z EQ :: Type Source # Methods getIndexGo :: Z -> Proxy Z -> Proxy EQ -> ResolvedIx Z Z EQ Source #
GetIndexGo (RunningIndex Z) (RunningIndex Z) EQ Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx Associated Types type ResolvedIx (RunningIndex Z) (RunningIndex Z) EQ :: Type Source # Methods getIndexGo :: RunningIndex Z -> Proxy (RunningIndex Z) -> Proxy EQ -> ResolvedIx (RunningIndex Z) (RunningIndex Z) EQ Source #
GetIndexGo (RunningIndex ix) (RunningIndex Z) (CmpNat (ToNat (RunningIndex ix)) (ToNat (RunningIndex Z))) => GetIndexGo (RunningIndex (ix :. i)) (RunningIndex Z) GT Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx Associated Types type ResolvedIx (RunningIndex (ix :. i)) (RunningIndex Z) GT :: Type Source # Methods getIndexGo :: RunningIndex (ix :. i) -> Proxy (RunningIndex Z) -> Proxy GT -> ResolvedIx (RunningIndex (ix :. i)) (RunningIndex Z) GT Source #
GetIndexGo (RunningIndex ix) (RunningIndex (my :. m)) (CmpNat (ToNat (RunningIndex ix)) (ToNat (RunningIndex (my :. m)))) => GetIndexGo (RunningIndex (ix :. i)) (RunningIndex (my :. m) :: Type) GT Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx Associated Types type ResolvedIx (RunningIndex (ix :. i)) (RunningIndex (my :. m)) GT :: Type Source # Methods getIndexGo :: RunningIndex (ix :. i) -> Proxy (RunningIndex (my :. m)) -> Proxy GT -> ResolvedIx (RunningIndex (ix :. i)) (RunningIndex (my :. m)) GT Source #
GetIndexGo (RunningIndex (ix :. i)) (RunningIndex (my :. m) :: Type) EQ Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx Associated Types type ResolvedIx (RunningIndex (ix :. i)) (RunningIndex (my :. m)) EQ :: Type Source # Methods getIndexGo :: RunningIndex (ix :. i) -> Proxy (RunningIndex (my :. m)) -> Proxy EQ -> ResolvedIx (RunningIndex (ix :. i)) (RunningIndex (my :. m)) EQ Source #
GetIndexGo ix Z (CmpNat (ToNat ix) (ToNat Z)) => GetIndexGo (ix :. i) Z GT Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx Associated Types type ResolvedIx (ix :. i) Z GT :: Type Source # Methods getIndexGo :: (ix :. i) -> Proxy Z -> Proxy GT -> ResolvedIx (ix :. i) Z GT Source #
GetIndexGo ix (my :. m) (CmpNat (ToNat ix) (ToNat (my :. m))) => GetIndexGo (ix :. i) (my :. m :: Type) GT Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx Associated Types type ResolvedIx (ix :. i) (my :. m) GT :: Type Source # Methods getIndexGo :: (ix :. i) -> Proxy (my :. m) -> Proxy GT -> ResolvedIx (ix :. i) (my :. m) GT Source #
GetIndexGo (ix :. i) (my :. m :: Type) EQ Source #
Instance details Defined in ADP.Fusion.Core.TyLvlIx Associated Types type ResolvedIx (ix :. i) (my :. m) EQ :: Type Source # Methods getIndexGo :: (ix :. i) -> Proxy (my :. m) -> Proxy EQ -> ResolvedIx (ix :. i) (my :. m) EQ Source #

getIndex :: forall ixTy myTy. GetIndex ixTy myTy => ixTy -> Proxy myTy -> GetIx ixTy myTy Source #

Simplifying wrapper around getIndexGo.

module GHC.TypeLits