Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
Nat
s.
Instances
type ToNat Z Source # | |
Defined in ADP.Fusion.Core.TyLvlIx | |
type ToNat (RunningIndex Z) Source # | |
Defined in ADP.Fusion.Core.TyLvlIx | |
type ToNat (RunningIndex (is :. i)) Source # | |
Defined in ADP.Fusion.Core.TyLvlIx | |
type ToNat (is :. i) Source # | |
Defined in ADP.Fusion.Core.TyLvlIx |
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
.
type ResolvedIx ixTy myTy cmp :: * Source #
getIndexGo :: ixTy -> Proxy myTy -> Proxy cmp -> ResolvedIx ixTy myTy cmp Source #
Instances
getIndex :: forall ixTy myTy. GetIndex ixTy myTy => ixTy -> Proxy myTy -> GetIx ixTy myTy Source #
Simplifying wrapper around getIndexGo
.
module GHC.TypeLits