diff --git a/dimensions.cabal b/dimensions.cabal --- a/dimensions.cabal +++ b/dimensions.cabal @@ -1,6 +1,6 @@ name: dimensions -version: 0.3.2.0 -cabal-version: >=1.20 +version: 1.0.0.0 +cabal-version: >=1.22 build-type: Simple license: BSD3 license-file: LICENSE @@ -19,24 +19,33 @@ subdir: dimensions +flag unsafeindices + description: + Disable bound checks on Idx and Idxs types. + default: False + + library + if flag(unsafeindices) + cpp-options: -DUNSAFE_INDICES exposed-modules: + Numeric.Dim + Numeric.Tuple + Numeric.Tuple.Lazy + Numeric.Tuple.Strict + Numeric.Type.Evidence + Numeric.Type.List + Numeric.TypedList Numeric.Dimensions - Numeric.Dimensions.Dim - Numeric.Dimensions.XDim - Numeric.Dimensions.Idx - Numeric.Dimensions.List - Numeric.Dimensions.Traverse - Numeric.Dimensions.Traverse.IO - Numeric.Dimensions.Traverse.ST - Numeric.TypeLits + Numeric.Dimensions.Dims + Numeric.Dimensions.Idxs + Numeric.Dimensions.Fold build-depends: - base >=4.9 && <5, - ghc-prim >= 0.5 + base >=4.9 && <5 default-language: Haskell2010 hs-source-dirs: src - ghc-options: -Wall -fwarn-tabs -O2 + ghc-options: -Wall test-suite dimensions-test @@ -44,12 +53,13 @@ type: exitcode-stdio-1.0 main-is: Spec.hs other-modules: - Numeric.Dimensions.ListTest + Numeric.DimTest + Numeric.Dimensions.DimsTest build-depends: base -any, - Cabal >=1.20, + Cabal -any, QuickCheck -any, dimensions -any default-language: Haskell2010 hs-source-dirs: test - ghc-options: -Wall -fwarn-tabs -O2 + ghc-options: -Wall diff --git a/src/Numeric/Dim.hs b/src/Numeric/Dim.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dim.hs @@ -0,0 +1,446 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE Strict #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +----------------------------------------------------------------------------- +-- | +-- Module : Numeric.Dim +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- This module is based on `GHC.TypeLits` and re-exports its functionality. +-- It provides `KnownDim` class that is similar to `KnownNat`, but keeps +-- `Int`s instead of `Integer`s; +-- Also it provides `Dim` data family serving as a customized `Proxy` type +-- and a singleton suitable for recovering an instance of the `KnownDim` class. +-- A set of utility functions provide inference functionality, so +-- that `KnownDim` can be preserved over some type-level operations. +-- +----------------------------------------------------------------------------- +module Numeric.Dim + ( -- * Type level numbers that can be unknown. + XNat (..), XN, N, XNatType (..) + -- * Term level dimension + , Dim (Dim, D, Dn, Dx), SomeDim + , KnownDim (..), KnownXNatType (..) + , dimVal, dimVal', someDimVal + , sameDim, sameDim' + , compareDim, compareDim' + , constrain, constrainBy, relax + -- * Simple Dim arithmetics + -- + -- The functions below create singleton values that work as a witness + -- of `KnownDim` instance for type-level Nat operations. + -- For example, to show that @(a + b)@ is a @KnownDim@, one writes: + -- + -- > case plusDim dA dB of + -- > D -> ... -- here we know KnownDim ( a + b ) + -- + -- There is a bug and a feature in these functions though: + -- they are implemented in terms of @Num Word@, which means that + -- their results are subject to integer overflow. + -- The good side is the confidence that they behave exactly as + -- their @Word@ counterparts. + , plusDim, minusDim, minusDimM, timesDim, powerDim + -- * Re-export part of `GHC.TypeLits` for convenience + , Nat, CmpNat, type (+), type (-), type (*), type (^) + , MinDim, FixedDim, inferDimLE + -- * Inferring kind of type-level dimension + , KnownDimKind (..), DimKind (..) + ) where + + +import Data.Type.Bool +import Data.Type.Equality +import GHC.Base (Type) +import GHC.Exts (Constraint, Proxy#, proxy#, unsafeCoerce#) +import GHC.TypeLits + +import Numeric.Type.Evidence + + +-- | Either known or unknown at compile-time natural number +data XNat = XN Nat | N Nat +-- | Unknown natural number, known to be not smaller than the given Nat +type XN (n::Nat) = 'XN n +-- | Known natural number +type N (n::Nat) = 'N n + +-- | Find out whether @XNat@ is of known or constrained type. +data XNatType :: XNat -> Type where + -- | Given @XNat@ is known + Nt :: XNatType ('N n) + -- | Given @XNat@ is constrained unknown + XNt :: XNatType ('XN m) + +-- | Same as `SomeNat` +type SomeDim = Dim ('XN 0) + +-- | Singleton type to store type-level dimension value. +-- +-- On the one hand, it can be used to let type-inference system know +-- relations between type-level naturals. +-- On the other hand, this is just a newtype wrapper on the @Word@ type. +-- +-- Usually, the type parameter of @Dim@ is either @Nat@ or @XNat@. +-- If dimensionality of your data is known in advance, use @Nat@; +-- if you know the size of some dimensions, but do not know the size +-- of others, use @XNat@s to represent them. +newtype Dim (x :: k) = DimSing Word +-- Starting from GHC 8.2, compiler supports specifying lists of complete +-- pattern synonyms. +#if __GLASGOW_HASKELL__ >= 802 +{-# COMPLETE D #-} +{-# COMPLETE Dn, Dx #-} +{-# COMPLETE Dim #-} +#endif + + +-- | Independently of the kind of type-level number, +-- construct an instance of `KnownDim` from it. +-- +-- Match against this pattern to bring `KnownDim` instance into scope +-- when you don't know the kind of the @Dim@ parameter. +pattern Dim :: forall (n :: k) . () => KnownDim n => Dim n +pattern Dim <- (dimEv -> E) + where + Dim = dim @_ @n + + +-- | Same as @Dim@ pattern, but constrained to @Nat@ kind. +pattern D :: forall (n :: Nat) . () => KnownDim n => Dim n +pattern D <- (dimEv -> E) + where + D = dim @_ @n + +-- | Statically known `XNat` +pattern Dn :: forall (xn :: XNat) . KnownXNatType xn + => forall (n :: Nat) . (KnownDim n, xn ~ 'N n) => Dim n -> Dim xn +pattern Dn k <- (dimXNEv (xNatType @xn) -> PatN k) + where + Dn k = unsafeCoerce# k + +-- | `XNat` that is unknown at compile time. +-- Same as `SomeNat`, but for a dimension: +-- Hide dimension size inside, but allow specifying its minimum possible value. +pattern Dx :: forall (xn :: XNat) . KnownXNatType xn + => forall (n :: Nat) (m :: Nat) + . (KnownDim n, MinDim m n, xn ~ 'XN m) => Dim n -> Dim xn +pattern Dx k <- (dimXNEv (xNatType @xn) -> PatXN k) + where + Dx k = unsafeCoerce# k + +-- | This class provides the `Dim` associated with a type-level natural. +class KnownDim (n :: k) where + -- | Get value of type-level dim at runtime. + -- + -- Note, this function is supposed to be used with @TypeApplications@, + -- and the @KnownDim@ class has varying kind of the parameter; + -- thus, the function has two type paremeters (kind and type of @n@). + -- For example, you can type: + -- + -- >>>:set -XTypeApplications + -- >>>:set -XDataKinds + -- >>>:t dim @Nat @3 + -- dim @Nat @3 :: Dim 3 + -- + -- >>>:set -XTypeOperators + -- >>>:t dim @_ @(13 - 6) + -- dim @_ @(13 - 6) :: Dim 7 + -- + -- + -- >>>:t dim @_ @(N 17) + -- dim @_ @(N 17) :: Dim (N 17) + -- + dim :: Dim n + + +-- | Find out the type of `XNat` constructor +class KnownXNatType (n :: XNat) where + -- | Pattern-match against this to out the type of `XNat` constructor + xNatType :: XNatType n + +instance KnownXNatType ('N n) where + xNatType = Nt + {-# INLINE xNatType #-} + +instance KnownXNatType ('XN n) where + xNatType = XNt + {-# INLINE xNatType #-} + + +-- | Similar to `natVal` from `GHC.TypeLits`, but returns `Word`. +dimVal :: Dim (x :: k) -> Word +dimVal = unsafeCoerce# +{-# INLINE dimVal #-} + +-- | Similar to `natVal` from `GHC.TypeLits`, but returns `Word`. +dimVal' :: forall n . KnownDim n => Word +dimVal' = unsafeCoerce# (dim @_ @n) +{-# INLINE dimVal' #-} + +-- | Friendly error message if `m <= n` constraint is not satisfied. +-- Use this type family instead of @(<=)@ if possible +-- or try `inferDimLE` function as the last resort. +type family MinDim (m :: Nat) (n :: Nat) :: Constraint where + MinDim m n = + If (CmpNat m n == 'GT) + (TypeError + ('Text "Minimum Dim size constraint (" + ':<>: 'ShowType m + ':<>: 'Text " <= " + ':<>: 'ShowType n + ':<>: 'Text ") is not satisfied." + ':$$: 'Text "Minimum Dim: " ':<>: 'ShowType m + ':$$: 'Text " Actual Dim: " ':<>: 'ShowType n + ) :: Constraint + ) + (m <= n) + +-- | Constraints given by an XNat type on possible values of a Nat hidden inside. +type family FixedDim (x :: XNat) (n :: Nat) :: Constraint where + FixedDim ('N a) b = a ~ b + FixedDim ('XN m) b = MinDim m b + +instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where + {-# INLINE dim #-} + dim = DimSing (fromInteger (natVal' (proxy# :: Proxy# n))) + +instance {-# OVERLAPPING #-} KnownDim 0 where + { {-# INLINE dim #-}; dim = DimSing 0 } +instance {-# OVERLAPPING #-} KnownDim 1 where + { {-# INLINE dim #-}; dim = DimSing 1 } +instance {-# OVERLAPPING #-} KnownDim 2 where + { {-# INLINE dim #-}; dim = DimSing 2 } +instance {-# OVERLAPPING #-} KnownDim 3 where + { {-# INLINE dim #-}; dim = DimSing 3 } +instance {-# OVERLAPPING #-} KnownDim 4 where + { {-# INLINE dim #-}; dim = DimSing 4 } +instance {-# OVERLAPPING #-} KnownDim 5 where + { {-# INLINE dim #-}; dim = DimSing 5 } +instance {-# OVERLAPPING #-} KnownDim 6 where + { {-# INLINE dim #-}; dim = DimSing 6 } +instance {-# OVERLAPPING #-} KnownDim 7 where + { {-# INLINE dim #-}; dim = DimSing 7 } +instance {-# OVERLAPPING #-} KnownDim 8 where + { {-# INLINE dim #-}; dim = DimSing 8 } +instance {-# OVERLAPPING #-} KnownDim 9 where + { {-# INLINE dim #-}; dim = DimSing 9 } +instance {-# OVERLAPPING #-} KnownDim 10 where + { {-# INLINE dim #-}; dim = DimSing 10 } +instance {-# OVERLAPPING #-} KnownDim 11 where + { {-# INLINE dim #-}; dim = DimSing 11 } +instance {-# OVERLAPPING #-} KnownDim 12 where + { {-# INLINE dim #-}; dim = DimSing 12 } +instance {-# OVERLAPPING #-} KnownDim 13 where + { {-# INLINE dim #-}; dim = DimSing 13 } +instance {-# OVERLAPPING #-} KnownDim 14 where + { {-# INLINE dim #-}; dim = DimSing 14 } +instance {-# OVERLAPPING #-} KnownDim 15 where + { {-# INLINE dim #-}; dim = DimSing 15 } +instance {-# OVERLAPPING #-} KnownDim 16 where + { {-# INLINE dim #-}; dim = DimSing 16 } +instance {-# OVERLAPPING #-} KnownDim 17 where + { {-# INLINE dim #-}; dim = DimSing 17 } +instance {-# OVERLAPPING #-} KnownDim 18 where + { {-# INLINE dim #-}; dim = DimSing 18 } +instance {-# OVERLAPPING #-} KnownDim 19 where + { {-# INLINE dim #-}; dim = DimSing 19 } +instance {-# OVERLAPPING #-} KnownDim 20 where + { {-# INLINE dim #-}; dim = DimSing 20 } + +instance KnownDim n => KnownDim ('N n) where + {-# INLINE dim #-} + dim = unsafeCoerce# (dim @Nat @n) + +-- | Similar to `someNatVal` from `GHC.TypeLits`. +someDimVal :: Word -> SomeDim +someDimVal = unsafeCoerce# +{-# INLINE someDimVal #-} + + +-- | Change the minimum allowed size of a @Dim (XN x)@, +-- while testing if the value inside satisfies it. +constrain :: forall (m :: Nat) x . KnownDim m + => Dim x -> Maybe (Dim (XN m)) +constrain (DimSing x) | dimVal' @m > x = Nothing + | otherwise = Just (unsafeCoerce# x) +{-# INLINE constrain #-} + +-- | `constrain` with explicitly-passed constraining @Dim@ +-- to avoid @AllowAmbiguousTypes@. +constrainBy :: forall m x . Dim m -> Dim x -> Maybe (Dim (XN m)) +constrainBy D = constrain @m +#if __GLASGOW_HASKELL__ < 802 +constrainBy _ = error "Dim: Impossible pattern." +#endif + +-- | Decrease minimum allowed size of a @Dim (XN x)@. +relax :: forall (m :: Nat) (n :: Nat) . (MinDim m n) => Dim (XN n) -> Dim (XN m) +relax = unsafeCoerce# +{-# INLINE relax #-} + + +-- | We either get evidence that this function +-- was instantiated with the same type-level numbers, or Nothing. +-- +-- Note, this function works on @Nat@-indexed dimensions only, +-- because @Dim (XN x)@ does not have runtime evidence to infer @x@ +-- and `KnownDim x` does not imply `KnownDim (XN x)`. +sameDim :: forall (x :: Nat) (y :: Nat) + . Dim x -> Dim y -> Maybe (Evidence (x ~ y)) +sameDim (DimSing a) (DimSing b) + | a == b = Just (unsafeCoerce# (E @(x ~ x))) + | otherwise = Nothing +{-# INLINE sameDim #-} + +-- | We either get evidence that this function +-- was instantiated with the same type-level numbers, or Nothing. +sameDim' :: forall (x :: Nat) (y :: Nat) p q + . (KnownDim x, KnownDim y) + => p x -> q y -> Maybe (Evidence (x ~ y)) +sameDim' _ _ = sameDim' (dim @Nat @x) (dim @Nat @y) +{-# INLINE sameDim' #-} + +-- | Ordering of dimension values. +compareDim :: Dim a -> Dim b -> Ordering +compareDim = unsafeCoerce# (compare :: Word -> Word -> Ordering) +{-# INLINE compareDim #-} + + +-- | Ordering of dimension values. +compareDim' :: forall a b p q + . (KnownDim a, KnownDim b) => p a -> q b -> Ordering +compareDim' _ _ = compareDim (dim @_ @a) (dim @_ @b) +{-# INLINE compareDim' #-} + + +instance Eq (Dim (n :: Nat)) where + _ == _ = True + {-# INLINE (==) #-} + +instance Eq (Dim (x :: XNat)) where + DimSing a == DimSing b = a == b + {-# INLINE (==) #-} + +instance Ord (Dim (n :: Nat)) where + compare _ _ = EQ + {-# INLINE compare #-} + +instance Ord (Dim (x :: XNat)) where + compare = compareDim + {-# INLINE compare #-} + +instance Show (Dim x) where + showsPrec p = showsPrec p . dimVal + {-# INLINE showsPrec #-} + +instance KnownDim m => Read (Dim ('XN m)) where + readsPrec p xs = do (a,ys) <- readsPrec p xs + case constrain (someDimVal a) of + Nothing -> [] + Just n -> [(n,ys)] + + + + +plusDim :: Dim n -> Dim m -> Dim (n + m) +plusDim (DimSing a) (DimSing b) = unsafeCoerce# (a + b) +{-# INLINE plusDim #-} + +minusDim :: MinDim m n => Dim n -> Dim m -> Dim (n - m) +minusDim (DimSing a) (DimSing b) = unsafeCoerce# (a - b) +{-# INLINE minusDim #-} + +minusDimM :: Dim n -> Dim m -> Maybe (Dim (n - m)) +minusDimM (DimSing a) (DimSing b) + | a >= b = Just (unsafeCoerce# (a - b)) + | otherwise = Nothing +{-# INLINE minusDimM #-} + +timesDim :: Dim n -> Dim m -> Dim ((*) n m) +timesDim (DimSing a) (DimSing b) = unsafeCoerce# (a * b) +{-# INLINE timesDim #-} + +powerDim :: Dim n -> Dim m -> Dim ((^) n m) +powerDim (DimSing a) (DimSing b) = unsafeCoerce# (a ^ b) +{-# INLINE powerDim #-} + + +-- | @MinDim@ implies @(<=)@, but this fact is not so clear to GHC. +-- This function assures the type system that the relation takes place. +inferDimLE :: forall m n . MinDim m n => Evidence (m <= n) +inferDimLE = unsafeCoerce# (E @(n <= n)) + + +-- | GADT to support `KnownDimKind` type class. +-- Match against its constructors to know if @k@ is @Nat@ or @XNat@ +data DimKind :: Type -> Type where + -- | Working on @Nat@. + DimNat :: DimKind Nat + -- | Working on @XNat@. + DimXNat :: DimKind XNat + +-- | Figure out whether the type-level dimension is `Nat` or `XNat`. +-- Useful for generalized inference functions. +class KnownDimKind k where + dimKind :: DimKind k + +instance KnownDimKind Nat where + dimKind = DimNat + +instance KnownDimKind XNat where + dimKind = DimXNat + +-------------------------------------------------------------------------------- + +-- | This function does GHC's magic to convert user-supplied `dim` function +-- to create an instance of `KnownDim` typeclass at runtime. +-- The trick is taken from Edward Kmett's reflection library explained +-- in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection +reifyDim :: forall r d . Dim d -> (KnownDim d => r) -> r +reifyDim d k = unsafeCoerce# (MagicDim k :: MagicDim d r) d +{-# INLINE reifyDim #-} +newtype MagicDim d r = MagicDim (KnownDim d => r) + +dimEv :: Dim d -> Evidence (KnownDim d) +dimEv d = reifyDim d E +{-# INLINE dimEv #-} + +data PatXDim (xn :: XNat) where + PatN :: KnownDim n => Dim n -> PatXDim ('N n) + PatXN :: (KnownDim n, MinDim m n) => Dim n -> PatXDim ('XN m) + +dimXNEv :: forall (xn :: XNat) . XNatType xn -> Dim xn -> PatXDim xn +dimXNEv Nt (DimSing k) = reifyDim dd (PatN dd) + where + dd = DimSing @Nat @_ k +dimXNEv XNt xn@(DimSing k) = reifyDim dd (f dd xn) + where + dd = DimSing @Nat @_ k + f :: forall (d :: Nat) (m :: Nat) + . KnownDim d => Dim d -> Dim ('XN m) -> PatXDim ('XN m) + f d _ = case ( unsafeCoerce# (E @((CmpNat m m == 'GT) ~ 'False, m <= m)) + :: Evidence ((CmpNat m d == 'GT) ~ 'False, m <= d) + ) of + E -> PatXN d +{-# INLINE dimXNEv #-} diff --git a/src/Numeric/Dimensions.hs b/src/Numeric/Dimensions.hs --- a/src/Numeric/Dimensions.hs +++ b/src/Numeric/Dimensions.hs @@ -7,7 +7,7 @@ -- Maintainer : chirkin@arch.ethz.ch -- -- Provides a set of data types to define and traverse through multiple dimensions. --- The core types are `Dim ds` and `Idx ds`, which fix dimension sizes at compile time. +-- The core types are `Dims ds` and `Idxs ds`, which fix dimension sizes at compile time. -- -- Lower indices go first, i.e. assumed enumeration -- is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1). @@ -16,13 +16,17 @@ ----------------------------------------------------------------------------- module Numeric.Dimensions - ( module Numeric.Dimensions.List - , module Numeric.Dimensions.Dim - , module Numeric.Dimensions.Idx - , Evidence (..), withEvidence, sumEvs, (+!+) + ( module Numeric.Dim + , module Numeric.Dimensions.Dims + , module Numeric.Dimensions.Idxs + , module Numeric.Dimensions.Fold + , module Numeric.Type.Evidence + , module Numeric.Type.List ) where -import Numeric.Dimensions.List -import Numeric.Dimensions.Dim -import Numeric.Dimensions.Idx -import Numeric.TypeLits +import Numeric.Dim +import Numeric.Dimensions.Dims +import Numeric.Dimensions.Idxs +import Numeric.Dimensions.Fold +import Numeric.Type.Evidence +import Numeric.Type.List diff --git a/src/Numeric/Dimensions/Dim.hs b/src/Numeric/Dimensions/Dim.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/Dim.hs +++ /dev/null @@ -1,582 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE RoleAnnotations #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeFamilyDependencies #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} ------------------------------------------------------------------------------ --- | --- Module : Numeric.Dimensions.Dim --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Maintainer : chirkin@arch.ethz.ch --- --- Provides a data type `Dim ds` to keep dimension sizes --- for multiple-dimensional data. --- Lower indices go first, i.e. assumed enumeration --- is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1). --- ------------------------------------------------------------------------------ - -module Numeric.Dimensions.Dim - ( -- * Dimension data types - Nat, XNat, XN, N, Dim (..), dimVal, totalDim, fromInt - , SomeDims (..), SomeDim (..), someDimVal, someDimsVal, sameDim, compareDim - , inSpaceOf, asSpaceOf - -- * Dimension constraints - , Dimensions (..), KnownDim (..), KnownDims - -- * Type-level programming - -- Provide type families to work with lists of dimensions (`[Nat]` or `[XNat]`) - , AsXDims, AsDims, WrapDims, UnwrapDims - , ConsDim, NatKind - , FixedDim, FixedXDim, WrapNat, type (:<), type (>:) - -- * Inference of dimension evidence - , inferDimensions, inferDimKnownDims, inferDimFiniteList - , inferTailDimensions, inferConcatDimensions - , inferPrefixDimensions, inferSuffixDimensions - , inferSnocDimensions, inferInitDimensions - , inferTakeNDimensions, inferDropNDimensions - , inferReverseDimensions, reifyDimensions - -- * Cons and Snoc inference - -- Very useful functions when you need some evidence for contraction ops. - , inferUnSnocDimensions, SnocDimensions - , inferUnConsDimensions, ConsDimensions - ) where - -import Data.Maybe (isJust) -import GHC.Exts (Constraint, unsafeCoerce#) -import Data.Type.Equality ((:~:)(..)) - -import Numeric.Dimensions.List -import Numeric.TypeLits - - --- | Type-level dimensionality -data Dim (ns :: k) where - -- | Zero-rank dimensionality - scalar - D :: Dim '[] - -- | List-like concatenation of dimensionality. - -- NatKind constraint is needed here to infer that - (:*) :: forall (n::l) (ns::[k]) . NatKind [k] l - => !(Dim n) -> !(Dim ns) -> Dim (ConsDim n ns) - -- | Proxy-like constructor - Dn :: forall (n :: Nat) . KnownDim n => Dim (n :: Nat) - -- | Nat known at runtime packed into existential constructor - Dx :: forall (n :: Nat) (m :: Nat) . n <= m - => !(Dim m) -> Dim (XN n) -infixr 5 :* - --- | Get runtime-known dim and make sure it is not smaller than the given Nat. -fromInt :: forall m . KnownDim m => Int -> Maybe (Dim (XN m)) -fromInt i | i < dimVal' @m = Nothing - | otherwise = do - SomeDim (dn :: Dim n) <- someDimVal i - return $ case unsafeEqEvidence @(m <=? n) @'True of - Evidence -> Dx dn -{-# INLINE fromInt #-} - - - --- | Same as SomeNat, but for Dimension: --- Hide all information about Dimension inside -data SomeDim = forall (n :: Nat) . SomeDim (Dim n) - --- | Same as SomeNat, but for Dimensions: --- Hide all information about Dimensions inside -data SomeDims = forall (ns :: [Nat]) . SomeDims (Dim ns) - --- | Get value of type-level dim at runtime. --- Gives a product of all dimensions if is a list. -dimVal :: Dim x -> Int -dimVal D = 1 -dimVal (d :* ds) = dimVal d * dimVal ds -dimVal (Dn :: Dim m) = dimVal' @m -dimVal (Dx (Dn :: Dim m)) = dimVal' @m -{-# INLINE dimVal #-} - --- | Product of all dimension sizes. -totalDim :: forall ds proxy . Dimensions ds => proxy ds -> Int -totalDim _ = dimVal (dim @ds) -{-# INLINE totalDim #-} - --- | Similar to `someNatVal`, but for a single dimension -someDimVal :: Int -> Maybe SomeDim -someDimVal x | 0 > x = Nothing - | otherwise = Just (reifyDim x f) - where - f :: forall (n :: Nat) . KnownDim n => Proxy# n -> SomeDim - f _ = SomeDim (Dn @n) -{-# INLINE someDimVal #-} - --- | Convert a list of ints into unknown type-level Dimensions list -someDimsVal :: [Int] -> Maybe SomeDims -someDimsVal [] = Just $ SomeDims D -someDimsVal (x:xs) | 0 > x = Nothing - | otherwise = do - SomeDim p <- someDimVal x - SomeDims ps <- someDimsVal xs - return $ SomeDims (p :* ps) -{-# INLINE someDimsVal #-} - -dimList :: Dim ds -> String -dimList D = "" -dimList d@Dn = show (dimVal d) -dimList (Dx d@Dn) = show (dimVal d) -dimList (d :* D) = show (dimVal d) -dimList (d :* ds) = show (dimVal d) ++ ' ':dimList ds - --- | We either get evidence that this function was instantiated with the --- same type-level Dimensions, or 'Nothing'. -sameDim :: Dim as -> Dim bs -> Maybe (Evidence (as ~ bs)) -sameDim D D = Just Evidence -sameDim (a :* as) (b :* bs) | dimVal a == dimVal b = (unsafeCoerce# (Evidence @())) <$ sameDim as bs - | otherwise = Nothing -sameDim _ _ = Nothing - - --- | Compare dimensions by their size in lexicorgaphic order --- from the last dimension to the first dimension --- (the last dimension is the most significant one). -compareDim :: Dim as -> Dim bs -> Ordering -compareDim D D = EQ -compareDim _ D = GT -compareDim D _ = LT -compareDim (a :* as) (b :* bs) = compareDim as bs `mappend` compare (dimVal a) (dimVal b) -compareDim a@Dn b@Dn = compare (dimVal a) (dimVal b) -compareDim (Dx a) (Dx b) = compare (dimVal a) (dimVal b) -compareDim a@Dn (Dx b) = compare (dimVal a) (dimVal b) -compareDim (Dx a) b@Dn = compare (dimVal a) (dimVal b) -compareDim a@Dn (b :* bs) = compareDim D bs `mappend` compare (dimVal a) (dimVal b) -compareDim (Dx a) (b :* bs) = compareDim D bs `mappend` compare (dimVal a) (dimVal b) -compareDim (a :* as) b@Dn = compareDim as D `mappend` compare (dimVal a) (dimVal b) -compareDim (a :* as) (Dx b) = compareDim as D `mappend` compare (dimVal a) (dimVal b) - - --- | Similar to `const` or `asProxyTypeOf`; --- to be used on such implicit functions as `dim`, `dimMax`, etc. -inSpaceOf :: a ds -> b ds -> a ds -inSpaceOf x _ = x -{-# INLINE inSpaceOf #-} - --- | Similar to `asProxyTypeOf`, --- Give a hint to type checker to fix the type of a function argument. -asSpaceOf :: a ds -> (b ds -> c) -> (b ds -> c) -asSpaceOf _ = id -{-# INLINE asSpaceOf #-} - - -instance Show (Dim ds) where - show D = "Dim Ø" - show ds = "Dim " ++ dimList ds - -instance Show SomeDims where - show (SomeDims p) = "Some" ++ show p - -instance Eq (Dim ds) where - a == b = isJust $ sameDim a b - -instance Eq SomeDims where - SomeDims as == SomeDims bs = isJust $ sameDim as bs - -instance Ord (Dim ds) where - compare = compareDim - -instance Ord SomeDims where - compare (SomeDims as) (SomeDims bs) = compareDim as bs - -class Dimensions (ds :: [Nat]) where - -- | Dimensionality of our space - dim :: Dim ds - -instance Dimensions '[] where - dim = D - {-# INLINE dim #-} - -instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds) where - dim = Dn :* dim - {-# INLINE dim #-} - -instance Dimensions ds => Bounded (Dim ds) where - maxBound = dim - {-# INLINE maxBound #-} - minBound = dim - {-# INLINE minBound #-} - - --------------------------------------------------------------------------------- --- * Type-level programming --------------------------------------------------------------------------------- - - --- | Map Dims onto XDims (injective) -type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where - AsXDims '[] = '[] - AsXDims (n ': ns) = N n ': AsXDims ns - --- | Map XDims onto Dims (injective) -type family AsDims (xns::[XNat]) = (ns :: [Nat]) | ns -> xns where - AsDims '[] = '[] - AsDims (N x ': xs) = x ': AsDims xs - --- | Treat Dims or XDims uniformly as XDims -type family WrapDims (x::[k]) :: [XNat] where - WrapDims ('[] :: [Nat]) = '[] - WrapDims ('[] :: [XNat]) = '[] - WrapDims (n ': ns :: [Nat]) = N n ': WrapDims ns - WrapDims (xns :: [XNat]) = xns - --- | Treat Dims or XDims uniformly as Dims -type family UnwrapDims (xns::[k]) :: [Nat] where - UnwrapDims ('[] :: [Nat]) = '[] - UnwrapDims ('[] :: [XNat]) = '[] - UnwrapDims (N x ': xs) = x ': UnwrapDims xs - UnwrapDims (XN _ ': _) = TypeError ( - 'Text "Cannot unwrap dimension XN into Nat" - ':$$: 'Text "(dimension is not known at compile time)" - ) - --- | Unify usage of XNat and Nat. --- This is useful in function and type definitions. --- Mainly used in the definition of Dim. -type family ConsDim (x :: l) (xs :: [k]) = (ys :: [k]) | ys -> x xs l where - ConsDim (x :: Nat) (xs :: [Nat]) = x ': xs - ConsDim (x :: Nat) (xs :: [XNat]) = N x ': xs - ConsDim (XN m) (xs :: [XNat]) = XN m ': xs - --- | Constraint on kinds; --- makes sure that the second argument kind is Nat if the first is a list of Nats. -type family NatKind ks k :: Constraint where - NatKind [Nat] l = l ~ Nat - NatKind [XNat] Nat = () - NatKind [XNat] XNat = () - NatKind ks k = ks ~ [k] - --- | FixedDim tries not to inspect content of `ns` and construct it --- based only on `xns` when it is possible. --- This means it does not check if `XN m <= n`. -type family FixedDim (xns :: [XNat]) (ns :: [Nat]) :: [Nat] where - FixedDim '[] _ = '[] - FixedDim (N n ': xs) ns = n ': FixedDim xs (Tail ns) - FixedDim (XN _ ': xs) ns = Head ns ': FixedDim xs (Tail ns) - --- | FixedXDim tries not to inspect content of `xns` and construct it --- based only on `ns` when it is possible. --- This means it does not check if `XN m <= n`. -type family FixedXDim (xns :: [XNat]) (ns :: [Nat]) :: [XNat] where - FixedXDim _ '[] = '[] - FixedXDim xs (n ': ns) = WrapNat (Head xs) n ': FixedXDim (Tail xs) ns - --- | WrapNat tries not to inspect content of `xn` and construct it --- based only on `n` when it is possible. --- This means it does not check if `XN m <= n`. -type family WrapNat (xn :: XNat) (n :: Nat) :: XNat where - WrapNat (XN m) n = XN m - WrapNat _ n = N n - --- | Synonym for (:+) that treats Nat values 0 and 1 in a special way: --- it preserves the property that all dimensions are greater than 1. -type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where - 0 :< _ = '[] - 1 :< ns = ns - n :< ns = n :+ ns -infixr 6 :< - --- | Synonym for (+:) that treats Nat values 0 and 1 in a special way: --- it preserves the property that all dimensions are greater than 1. -type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where - _ >: 0 = '[] - ns >: 1 = ns - ns >: n = ns +: n -infixl 6 >: - - - - --------------------------------------------------------------------------------- --- * Inference of evidence --------------------------------------------------------------------------------- - --- | Infer `Dimensions` given that the list is KnownDims and finite -inferDimensions :: forall (ds :: [Nat]) - . (KnownDims ds, FiniteList ds) - => Evidence (Dimensions ds) -inferDimensions = case tList @Nat @ds of - TLEmpty -> Evidence - TLCons _ (_ :: TypeList ds') -> case inferDimensions @ds' of - Evidence -> Evidence -{-# INLINE inferDimensions #-} - --- | `Dimensions` implies `KnownDims` -inferDimKnownDims :: forall (ds :: [Nat]) - . Dimensions ds - => Evidence (KnownDims ds) -inferDimKnownDims = inferDimKnownDims' (dim @ds) - where - inferDimKnownDims' :: forall (ns :: [Nat]) . Dim ns -> Evidence (KnownDims ns) - inferDimKnownDims' D = Evidence - inferDimKnownDims' (Dn :* ds) = case inferDimKnownDims' ds of Evidence -> Evidence -{-# INLINE inferDimKnownDims #-} - - --- | `Dimensions` implies `FiniteList` -inferDimFiniteList :: forall (ds :: [Nat]) - . Dimensions ds - => Evidence (FiniteList ds) -inferDimFiniteList = inferDimFiniteList' (dim @ds) - where - inferDimFiniteList' :: forall (ns :: [Nat]) . Dim ns -> Evidence (FiniteList ns) - inferDimFiniteList' D = Evidence - inferDimFiniteList' (Dn :* ds) = case inferDimFiniteList' ds of Evidence -> Evidence -{-# INLINE inferDimFiniteList #-} - - --- | Infer that tail list is also Dimensions -inferTailDimensions :: forall (ds :: [Nat]) - . Dimensions ds - => Maybe (Evidence (Dimensions (Tail ds))) -inferTailDimensions = case dim @ds of - D -> Nothing - Dn :* ds' -> Just $ reifyDimensions ds' -{-# INLINE inferTailDimensions #-} - - --- | Infer that concatenation is also Dimensions -inferConcatDimensions :: forall as bs - . (Dimensions as, Dimensions bs) - => Evidence (Dimensions (as ++ bs)) -inferConcatDimensions = reifyDimensions $ magic (dim @as) (unsafeCoerce# $ dim @bs) - where - magic :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim ys - magic D ys = ys - magic xs D = unsafeCoerce# xs - magic (x :* xs) ys = unsafeCoerce# $ x :* magic xs ys - {-# NOINLINE magic #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882 -{-# INLINE inferConcatDimensions #-} - - --- | Infer that prefix is also Dimensions -inferPrefixDimensions :: forall bs asbs - . (IsSuffix bs asbs ~ 'True, Dimensions bs, Dimensions asbs) - => Evidence (Dimensions (Prefix bs asbs)) -inferPrefixDimensions = reifyDimensions $ magic (len dasbs - len (dim @bs)) (unsafeCoerce# dasbs) - where - dasbs = dim @asbs - len :: forall (ns :: [Nat]) . Dim ns -> Int - len D = 0 - len (_ :* ds) = 1 + len ds - magic :: forall (ns :: [Nat]) . Int -> Dim ns -> Dim ns - magic _ D = D - magic 0 _ = unsafeCoerce# D - magic n (d :* ds) = d :* magic (n-1) ds - {-# NOINLINE magic #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882 -{-# INLINE inferPrefixDimensions #-} - --- | Infer that suffix is also Dimensions -inferSuffixDimensions :: forall as asbs - . (IsPrefix as asbs ~ 'True, Dimensions as, Dimensions asbs) - => Evidence (Dimensions (Suffix as asbs)) -inferSuffixDimensions = reifyDimensions $ magic (dim @as) (unsafeCoerce# $ dim @asbs) - where - magic :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim ys - magic D ys = ys - magic _ D = D - magic (_ :* xs) (_ :* ys) = unsafeCoerce# $ magic xs ys -{-# INLINE inferSuffixDimensions #-} - --- | Make snoc almost as good as cons -inferSnocDimensions :: forall xs z - . (KnownDim z, Dimensions xs) - => Evidence (Dimensions (xs +: z)) -inferSnocDimensions = reifyDimensions $ magic (dim @xs) - where - magic :: forall (ns :: [Nat]) . Dim ns -> Dim (ns +: z) - magic D = Dn :* D - magic (d :* ds) = unsafeCoerce# (d :* magic ds) -{-# INLINE inferSnocDimensions #-} - --- | Init of the dimension list is also Dimensions, --- and the last dimension is KnownDim. -inferUnSnocDimensions :: forall ds - . Dimensions ds - => Maybe (Evidence (SnocDimensions ds)) -inferUnSnocDimensions = case dim @ds of - D -> Nothing - ds -> Just $ case magic ds of - (ys, Dn) -> case unsafeSnocDims' @ds of - Evidence -> case reifyDimensions @(Init ds) (unsafeCoerce# ys) of - Evidence -> Evidence - where - magic :: forall (ns :: [Nat]) . Dim ns -> (Dim ns, Dim (Last ns)) - magic D = (D, undefined) - magic (d :* D) = (unsafeCoerce# D, d) - magic (d :* ds) = case magic ds of - (ds', z) -> (d :* ds', unsafeCoerce# z) -{-# INLINE inferUnSnocDimensions #-} - - --- | Tail of the dimension list is also Dimensions, --- and the head dimension is KnownDim. -inferUnConsDimensions :: forall ds - . Dimensions ds - => Maybe (Evidence (ConsDimensions ds)) -inferUnConsDimensions = case dim @ds of - D -> Nothing - Dn :* ds' -> Just $ case reifyDimensions ds' +!+ unsafeConsDims' @ds of - Evidence -> Evidence -{-# INLINE inferUnConsDimensions #-} - --- | Various evidence for the Snoc operation. -type SnocDimensions (xs :: [Nat]) = - ( xs ~ (Init xs +: Last xs) - , xs ~ (Init xs ++ '[Last xs]) - , IsPrefix (Init xs) xs ~ 'True - , IsSuffix '[Last xs] xs ~ 'True - , Suffix (Init xs) xs ~ '[Last xs] - , Prefix '[Last xs] xs ~ Init xs - , Dimensions (Init xs) - , KnownDim (Last xs) - ) - --- | Various evidence for the Snoc operation. -type ConsDimensions (xs :: [Nat]) = - ( xs ~ ( Head xs :+ Tail xs) - , xs ~ ('[Head xs] ++ Tail xs) - , IsPrefix '[Head xs] xs ~ 'True - , IsSuffix (Tail xs) xs ~ 'True - , Suffix '[Head xs] xs ~ Tail xs - , Prefix (Tail xs) xs ~ '[Head xs] - , Dimensions (Tail xs) - , KnownDim (Head xs) - ) - - -unsafeSnocDims' :: forall (xs :: [Nat]) . Evidence - ( xs ~ (Init xs +: Last xs) - , xs ~ (Init xs ++ '[Last xs]) - , IsPrefix (Init xs) xs ~ 'True - , IsSuffix '[Last xs] xs ~ 'True - , Suffix (Init xs) xs ~ '[Last xs] - , Prefix '[Last xs] xs ~ Init xs - ) -unsafeSnocDims' = case unsafeEqEvidence @xs @(Init xs +: Last xs) - +!+ unsafeEqEvidence @xs @(Init xs ++ '[Last xs]) - +!+ unsafeEqEvidence @(IsPrefix (Init xs) xs) @'True - +!+ unsafeEqEvidence @(IsSuffix '[Last xs] xs) @'True - +!+ unsafeEqEvidence @(Suffix (Init xs) xs) @'[Last xs] - +!+ unsafeEqEvidence @(Prefix '[Last xs] xs) @(Init xs) of - Evidence -> Evidence -{-# INLINE unsafeSnocDims' #-} - -unsafeConsDims' :: forall (xs :: [Nat]) . Evidence - ( xs ~ ( Head xs :+ Tail xs) - , xs ~ ('[Head xs] ++ Tail xs) - , IsPrefix '[Head xs] xs ~ 'True - , IsSuffix (Tail xs) xs ~ 'True - , Suffix '[Head xs] xs ~ Tail xs - , Prefix (Tail xs) xs ~ '[Head xs] - ) -unsafeConsDims' = case unsafeEqEvidence @xs @( Head xs :+ Tail xs) - +!+ unsafeEqEvidence @xs @('[Head xs] ++ Tail xs) - +!+ unsafeEqEvidence @(IsPrefix '[Head xs] xs) @'True - +!+ unsafeEqEvidence @(IsSuffix (Tail xs) xs) @'True - +!+ unsafeEqEvidence @(Suffix '[Head xs] xs) @(Tail xs) - +!+ unsafeEqEvidence @(Prefix (Tail xs) xs) @'[Head xs] of - Evidence -> Evidence -{-# INLINE unsafeConsDims' #-} - - --- | Init of the list is also Dimensions -inferInitDimensions :: forall xs - . Dimensions xs - => Maybe (Evidence (Dimensions (Init xs))) -inferInitDimensions = case dim @xs of - D -> Nothing - ds -> Just . reifyDimensions $ magic (unsafeCoerce# ds) - where - magic :: forall (ns :: [Nat]) . Dim ns -> Dim ns - magic D = D - magic (_ :* D) = unsafeCoerce# D - magic (d :* ds) = d :* magic ds -{-# INLINE inferInitDimensions #-} - --- | Take KnownDim of the list is also Dimensions -inferTakeNDimensions :: forall n xs - . (KnownDim n, Dimensions xs) - => Evidence (Dimensions (Take n xs)) -inferTakeNDimensions = reifyDimensions $ magic (dimVal' @n) (dim @xs) - where - magic :: forall (ns :: [Nat]) . Int -> Dim ns -> Dim (Take n ns) - magic _ D = D - magic 0 _ = unsafeCoerce# D - magic n (d :* ds) = unsafeCoerce# $ d :* (unsafeCoerce# $ magic (n-1) ds :: Dim (Tail ns)) - {-# NOINLINE magic #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882 -{-# INLINE inferTakeNDimensions #-} - --- | Drop KnownDim of the list is also Dimensions -inferDropNDimensions :: forall n xs - . (KnownDim n, Dimensions xs) - => Evidence (Dimensions (Drop n xs)) -inferDropNDimensions = reifyDimensions $ magic (dimVal' @n) (dim @xs) - where - magic :: forall (ns :: [Nat]) . Int -> Dim ns -> Dim (Drop n ns) - magic _ D = D - magic 0 ds = unsafeCoerce# ds - magic n (_ :* ds) = unsafeCoerce# $ magic (n-1) ds - {-# NOINLINE magic #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882 -{-# INLINE inferDropNDimensions #-} - --- | Reverse of the list is also Dimensions -inferReverseDimensions :: forall xs . Dimensions xs => Evidence (Dimensions (Reverse xs)) -inferReverseDimensions = reifyDimensions $ magic (dim @xs) (unsafeCoerce# D) - where - magic :: forall (ns :: [Nat]) . Dim ns -> Dim (Reverse ns) -> Dim (Reverse ns) - magic D xs = xs - magic (p:*sx) xs = magic (unsafeCoerce# sx :: Dim ns) - (unsafeCoerce# (p:*xs) :: Dim (Reverse ns)) -{-# INLINE inferReverseDimensions #-} - - - - - --------------------------------------------------------------------------------- --- * Utility functions --------------------------------------------------------------------------------- - - - --- | Use the given `Dim ds` to create an instance of `Dimensions ds` dynamically. -reifyDimensions :: forall (ds :: [Nat]) . Dim ds -> Evidence (Dimensions ds) -reifyDimensions ds = reifyDims ds Evidence -{-# INLINE reifyDimensions #-} - - --- | This function does GHC's magic to convert user-supplied `dimVal'` function --- to create an instance of KnownDim typeclass at runtime. --- The trick is taken from Edward Kmett's reflection library explained --- in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection -reifyDims :: forall r (ds :: [Nat]) . Dim ds -> ( Dimensions ds => r) -> r -reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds -{-# INLINE reifyDims #-} -newtype MagicDims ds r = MagicDims (Dimensions ds => r) - - -unsafeEqEvidence :: forall x y . Evidence (x ~ y) -unsafeEqEvidence = case (unsafeCoerce# Refl :: x :~: y) of Refl -> Evidence -{-# INLINE unsafeEqEvidence #-} diff --git a/src/Numeric/Dimensions/Dims.hs b/src/Numeric/Dimensions/Dims.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Dims.hs @@ -0,0 +1,405 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +----------------------------------------------------------------------------- +-- | +-- Module : Numeric.Dimensions.Dims +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- Provides a data type `Dims ds` to keep dimension sizes +-- for multiple-dimensional data. +-- Lower indices go first, i.e. assumed enumeration +-- is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1). +-- +----------------------------------------------------------------------------- + +module Numeric.Dimensions.Dims + ( Dims, SomeDims (..), Dimensions (..) + , TypedList ( Dims, XDims, AsXDims, KnownDims + , U, (:*), Empty, TypeList, Cons, Snoc, Reverse) + , listDims, someDimsVal, totalDim, totalDim' + , sameDims, sameDims' + , compareDims, compareDims' + , inSpaceOf, asSpaceOf + , xDims, xDims' + -- * Type-level programming + -- Provide type families to work with lists of dimensions (`[Nat]` or `[XNat]`) + , AsXDims, AsDims, FixedDims, KnownXNatTypes, type (:<), type (>:) + -- * Re-export type list + , RepresentableList (..), TypeList, types + , order, order' + -- * Re-export single dimension type and functions + , module Numeric.Dim + ) where + + + +import GHC.Exts (unsafeCoerce#, Constraint) +import qualified Text.Read as Read + +import Numeric.Dim +import Numeric.Type.Evidence +import Numeric.Type.List +import Numeric.TypedList (RepresentableList (..), TypeList, + TypedList (..), order, order', types) + + +-- | Type-level dimensionality O(1). +type Dims (xs :: [k]) = TypedList Dim xs + +-- Starting from GHC 8.2, compiler supports specifying lists of complete +-- pattern synonyms. +#if __GLASGOW_HASKELL__ >= 802 +{-# COMPLETE Dims #-} +{-# COMPLETE XDims #-} +{-# COMPLETE AsXDims #-} +{-# COMPLETE KnownDims #-} +#endif + +-- | @O(1)@ Pattern-matching against this constructor brings a `Dimensions` +-- instance into the scope. +-- Thus, you can do arbitrary operations on your dims and use this pattern +-- at any time to reconstruct the class instance at runtime. +pattern Dims :: forall ds . () => Dimensions ds => Dims ds +pattern Dims <- (dimsEv -> E) + where + Dims = dims @_ @ds + +-- | @O(Length ds)@ `Dimensions` and `KnownDim` for each individual dimension. +pattern KnownDims :: forall ds . () + => (All KnownDim ds, Dimensions ds) => Dims ds +pattern KnownDims <- (patKDims -> PatKDims) + where + KnownDims = dims @_ @ds + + +-- | Pattern-matching against this constructor reveals Nat-kinded list of dims, +-- pretending the dimensionality is known at compile time within the scope +-- of the pattern match. +-- This is the main recommended way to get `Dims` at runtime; +-- for example, reading a list of dimensions from a file. +-- +-- In order to use this pattern, one must know @XNat@ type constructors in +-- each dimension at compile time. +pattern XDims :: forall (xns :: [XNat]) . KnownXNatTypes xns + => forall (ns :: [Nat]) . (FixedDims xns ns, Dimensions ns) + => Dims ns -> Dims xns +pattern XDims ns <- (patXDims -> PatXDims ns) + where + XDims ns = unsafeCoerce# ns + +-- | An easy way to convert Nat-indexed dims into XNat-indexed dims. +pattern AsXDims :: forall (ns :: [Nat]) . () + => (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns)) + => Dims (AsXDims ns) -> Dims ns +pattern AsXDims xns <- (patAsXDims -> PatAsXDims xns) + where + AsXDims xns = unsafeCoerce# xns + +-- | Same as SomeNat, but for Dimensions: +-- Hide all information about Dimensions inside +data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns) + +class Dimensions (ds :: [k]) where + -- | Get dimensionality of a space at runtime, + -- represented as a list of `Dim`. + -- + -- Note, this function is supposed to be used with @TypeApplications@, + -- and the @Dimensions@ class has varying kind of the parameter; + -- thus, the function has two type paremeters (kind and type of @ds@). + -- For example, you can type: + -- + -- >>>:set -XTypeApplications + -- >>>:set -XDataKinds + -- >>>:t dims @_ @'[N 17, N 12] + -- dims @_ @'[N 17, N 12] :: Dims '[N 17, N 12] + -- + -- >>>:t dims @XNat @'[] + -- dims @XNat @'[] :: Dims '[] + -- + -- + -- >>>:t dims @_ @(Tail '[3,2,5,7]) + -- dims @_ @(Tail '[3,2,5,7]) :: Dims '[2, 5, 7] + -- + dims :: Dims ds + +instance Dimensions ('[] :: [k]) where + dims = U + {-# INLINE dims #-} + +instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds :: [k]) where + dims = dim :* dims + {-# INLINE dims #-} + + +-- | Convert `Dims xs` to a plain haskell list of dimension sizes @O(1)@. +listDims :: Dims xs -> [Word] +listDims = unsafeCoerce# +{-# INLINE listDims #-} + +-- | Convert a plain haskell list of dimension sizes into an unknown +-- type-level dimensionality @O(1)@. +someDimsVal :: [Word] -> SomeDims +someDimsVal = SomeDims . unsafeCoerce# +{-# INLINE someDimsVal #-} + +-- | Product of all dimension sizes @O(Length xs)@. +totalDim :: Dims xs -> Word +totalDim = product . listDims +{-# INLINE totalDim #-} + +-- | Product of all dimension sizes @O(Length xs)@. +totalDim' :: forall xs . Dimensions xs => Word +totalDim' = totalDim (dims @_ @xs) +{-# INLINE totalDim' #-} + +-- | Get XNat-indexed dims given their fixed counterpart. +xDims :: FixedDims xns ns => Dims ns -> Dims xns +xDims = unsafeCoerce# +{-# INLINE xDims #-} + +-- | Get XNat-indexed dims given their fixed counterpart. +xDims' :: forall xns ns . (FixedDims xns ns, Dimensions ns) => Dims xns +xDims' = xDims @xns (dims @Nat @ns) +{-# INLINE xDims' #-} + + +-- | We either get evidence that this function was instantiated with the +-- same type-level Dimensions, or 'Nothing' @O(Length xs)@. +-- +-- Note, this function works on @Nat@-indexed dimensions only, +-- because @Dims '[XN x]@ does not have runtime evidence to infer @x@ +-- and `KnownDim x` does not imply `KnownDim (XN x)`. +sameDims :: Dims (as :: [Nat]) -> Dims (bs :: [Nat]) -> Maybe (Evidence (as ~ bs)) +sameDims as bs + | listDims as == listDims bs + = Just (unsafeCoerce# (E @('[] ~ '[]))) + | otherwise = Nothing +{-# INLINE sameDims #-} + + +-- | We either get evidence that this function was instantiated with the +-- same type-level Dimensions, or 'Nothing' @O(Length xs)@. +sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) p q + . (Dimensions as, Dimensions bs) + => p as -> q bs -> Maybe (Evidence (as ~ bs)) +sameDims' _ _ = sameDims (dims @Nat @as) (dims @Nat @bs) +{-# INLINE sameDims' #-} + +-- | Compare dimensions by their size in lexicorgaphic order +-- from the last dimension to the first dimension +-- (the last dimension is the most significant one). +-- +-- Literally, +-- +-- > compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b) +compareDims :: Dims as -> Dims bs -> Ordering +compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b) +{-# INLINE compareDims #-} + +-- | Compare dimensions by their size in lexicorgaphic order +-- from the last dimension to the first dimension +-- (the last dimension is the most significant one) @O(Length xs)@. +-- +-- Literally, +-- +-- > compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b) +-- +-- This is the same @compare@ rule, as for `Idxs`. +compareDims' :: forall as bs p q + . (Dimensions as, Dimensions bs) + => p as -> q bs -> Ordering +compareDims' _ _ = compareDims (dims @_ @as) (dims @_ @bs) +{-# INLINE compareDims' #-} + + +-- | Similar to `const` or `asProxyTypeOf`; +-- to be used on such implicit functions as `dim`, `dimMax`, etc. +inSpaceOf :: a ds -> b ds -> a ds +inSpaceOf x _ = x +{-# INLINE inSpaceOf #-} + +-- | Similar to `asProxyTypeOf`, +-- Give a hint to type checker to fix the type of a function argument. +asSpaceOf :: a ds -> (b ds -> c) -> (b ds -> c) +asSpaceOf _ = id +{-# INLINE asSpaceOf #-} + + +instance Eq (Dims (ds :: [Nat])) where + (==) _ _ = True + +instance Eq (Dims (ds :: [XNat])) where + (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool) + +instance Eq SomeDims where + SomeDims as == SomeDims bs = listDims as == listDims bs + +instance Ord (Dims (ds :: [Nat])) where + compare _ _ = EQ + +instance Ord (Dims (ds :: [XNat])) where + compare = compareDims + +instance Ord SomeDims where + compare (SomeDims as) (SomeDims bs) = compareDims as bs + +instance Show (Dims xs) where + show ds = "Dims " ++ show (listDims ds) + showsPrec p ds + = showParen (p >= 10) + $ showString "Dims " . showsPrec p (listDims ds) + +instance Show SomeDims where + show (SomeDims ds) = "SomeDims " ++ show (listDims ds) + showsPrec p (SomeDims ds) + = showParen (p >= 10) + $ showString "SomeDims " . showsPrec p (listDims ds) + +instance Read SomeDims where + readPrec = Read.parens $ Read.prec 10 $ do + s <- Read.lexP + if s == Read.Ident "SomeDims" + then someDimsVal <$> Read.readPrec + else Read.pfail + +instance Dimensions ds => Bounded (Dims ds) where + maxBound = dims + {-# INLINE maxBound #-} + minBound = dims + {-# INLINE minBound #-} + + + +-- | Map Dims onto XDims (injective) +type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where + AsXDims '[] = '[] + AsXDims (n ': ns) = N n ': AsXDims ns + +-- | Map XDims onto Dims (injective) +type family AsDims (xns::[XNat]) = (ns :: [Nat]) | ns -> xns where + AsDims '[] = '[] + AsDims (N x ': xs) = x ': AsDims xs + +-- | Constrain @Nat@ dimensions hidden behind @XNat@s. +type family FixedDims (xns::[XNat]) (ns :: [Nat]) :: Constraint where + FixedDims '[] ns = (ns ~ '[]) + FixedDims (xn ': xns) ns + = ( ns ~ (Head ns ': Tail ns) + , FixedDim xn (Head ns) + , FixedDims xns (Tail ns)) + +-- | Know the structure of each dimension +type KnownXNatTypes xns = All KnownXNatType xns + + +-- | Synonym for (:+) that treats Nat values 0 and 1 in a special way: +-- it preserves the property that all dimensions are greater than 1. +type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where + 0 :< _ = '[] + 1 :< ns = ns + n :< ns = n :+ ns +infixr 6 :< + +-- | Synonym for (+:) that treats Nat values 0 and 1 in a special way: +-- it preserves the property that all dimensions are greater than 1. +type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where + _ >: 0 = '[] + ns >: 1 = ns + ns >: n = ns +: n +infixl 6 >: + + + + + + +-------------------------------------------------------------------------------- + +-- | This function does GHC's magic to convert user-supplied `dims` function +-- to create an instance of `Dimensions` typeclass at runtime. +-- The trick is taken from Edward Kmett's reflection library explained +-- in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection +reifyDims :: forall r ds . Dims ds -> ( Dimensions ds => r) -> r +reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds +{-# INLINE reifyDims #-} +newtype MagicDims ds r = MagicDims (Dimensions ds => r) + +dimsEv :: Dims ds -> Evidence (Dimensions ds) +dimsEv ds = reifyDims ds E +{-# INLINE dimsEv #-} + + +data PatXDims (xns :: [XNat]) + = forall (ns :: [Nat]) + . (FixedDims xns ns, Dimensions ns) => PatXDims (Dims ns) + + +patXDims :: All KnownXNatType xns => Dims xns -> PatXDims xns +patXDims U = PatXDims U +patXDims (Dn n :* xns) = case patXDims xns of + PatXDims ns -> PatXDims (n :* ns) +patXDims (Dx n :* xns) = case patXDims xns of + PatXDims ns -> PatXDims (n :* ns) +#if __GLASGOW_HASKELL__ >= 802 +#else +patXDims _ = error "XDims/patXDims: impossible argument" +#endif +{-# INLINE patXDims #-} + + +data PatAsXDims (ns :: [Nat]) + = (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns)) + => PatAsXDims (Dims (AsXDims ns)) + + +patAsXDims :: Dims ns -> PatAsXDims ns +patAsXDims U = PatAsXDims U +patAsXDims (n@D :* ns) = case patAsXDims ns of + PatAsXDims xns -> PatAsXDims (Dn n :* xns) +#if __GLASGOW_HASKELL__ >= 802 +#else +patAsXDims _ = error "AsXDims/patAsXDims: impossible argument" +#endif +{-# INLINE patAsXDims #-} + + + +data PatKDims (ns :: [k]) + = (All KnownDim ns, Dimensions ns) => PatKDims + + +patKDims :: Dims ns -> PatKDims ns +patKDims U = PatKDims +patKDims (Dim :* ns) = case patKDims ns of + PatKDims -> PatKDims +#if __GLASGOW_HASKELL__ >= 802 +#else +patKDims _ = error "Dims/patKDims: impossible argument" +#endif +{-# INLINE patKDims #-} diff --git a/src/Numeric/Dimensions/Fold.hs b/src/Numeric/Dimensions/Fold.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Fold.hs @@ -0,0 +1,334 @@ +{-# LANGUAGE PolyKinds #-} +-- Workaround weird behavior of GHC 8.4 +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} +----------------------------------------------------------------------------- +-- | +-- Module : Numeric.Dimensions.Fold +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- Fold a function over all dimensions provided dimension indices or offsets. +-- The main purpose of this module is to fold or traverse flat data arrays +-- following the shape of dimensions associated with them. +-- +----------------------------------------------------------------------------- +module Numeric.Dimensions.Fold + ( overDim, overDim_, overDimIdx, overDimIdx_ + , overDimOff, overDimOff_ + , overDimReverse, overDimReverseIdx + , foldDim, foldDimIdx, foldDimOff + , foldDimReverse, foldDimReverseIdx + , overDimPart, overDimPartIdx + ) where + + +import Control.Monad ((>=>)) +import Numeric.Dimensions.Idxs + +-- | Go over all dimensions keeping track of index and offset +overDim :: Monad m + => Dims ds -- ^ Shape of a space + -> (Idxs ds -> Int -> a -> m a) -- ^ Function to call on each dimension + -> Int -- ^ Initial offset + -> Int -- ^ Offset step + -> a -- ^ Initial value + -> m a +overDim U k offset _step = k U offset +overDim (d :* ds) k offset step = overDim ds k' offset (di * step) + where + dw = dimVal d + di = fromIntegral dw + k' is = go 1 + where + go i off + | i > dw = return + | otherwise = k (Idx i :* is) off >=> go (i+1) (off+step) +{-# INLINE overDim #-} + +-- | Go over all dimensions in reverse order keeping track of index and offset +overDimReverse :: Monad m + => Dims ds -- ^ Shape of a space + -> (Idxs ds -> Int -> a -> m a) -- ^ Function to call on each dimension + -> Int -- ^ Initial offset + -> Int -- ^ Offset step (substracted from initial offset) + -> a -- ^ Initial value + -> m a +overDimReverse U k offset _step = k U offset +overDimReverse (d :* ds) k offset step = overDimReverse ds k' offset (di * step) + where + dw = dimVal d + di = fromIntegral dw + k' is = go dw + where + go i off + | i <= 0 = return + | otherwise = k (Idx i :* is) off >=> go (i-1) (off-step) +{-# INLINE overDimReverse #-} + +-- | Go over all dimensions keeping track of index and offset +overDim_ :: Monad m + => Dims ds -- ^ Shape of a space + -> (Idxs ds -> Int -> m ()) -- ^ Function to call on each dimension + -> Int -- ^ Initial offset + -> Int -- ^ Offset step + -> m () +overDim_ U k offset _step = k U offset +overDim_ (d :* ds) k offset step = overDim_ ds k' offset (di * step) + where + dw = dimVal d + di = fromIntegral dw + k' is = go 1 + where + go i off + | i > dw = return () + | otherwise = k (Idx i :* is) off >> go (i+1) (off+step) +{-# INLINE overDim_ #-} + +-- | Go over all dimensions keeping track of index +overDimIdx :: Monad m + => Dims ds -- ^ Shape of a space + -> (Idxs ds -> a -> m a) -- ^ Function to call on each dimension + -> a -- ^ Initial value + -> m a +overDimIdx U k = k U +overDimIdx (d :* ds) k = overDimIdx ds k' + where + dw = dimVal d + k' is = go 1 + where + go i + | i > dw = return + | otherwise = k (Idx i :* is) >=> go (i+1) +{-# INLINE overDimIdx #-} + +-- | Go over all dimensions keeping track of index +overDimIdx_ :: Monad m + => Dims ds -- ^ Shape of a space + -> (Idxs ds -> m ()) -- ^ Function to call on each dimension + -> m () +overDimIdx_ U k = k U +overDimIdx_ (d :* ds) k = overDimIdx_ ds k' + where + dw = dimVal d + k' is = go 1 + where + go i + | i > dw = return () + | otherwise = k (Idx i :* is) >> go (i+1) +{-# INLINE overDimIdx_ #-} + + +-- | Go over all dimensions keeping track of total offset +overDimOff :: Monad m + => Dims ds -- ^ Shape of a space + -> (Int -> a -> m a) -- ^ Function to call with each offset value + -> Int -- ^ Initial offset + -> Int -- ^ Offset step + -> a -- ^ Initial value + -> m a +overDimOff ds k offset step = go (totalDim ds) offset + where + go i off + | i == 0 = return + | otherwise = k off >=> go (i-1) (off+step) +{-# INLINE overDimOff #-} + +-- | Go over all dimensions keeping track of total offset +overDimOff_ :: Monad m + => Dims ds -- ^ Shape of a space + -> (Int -> m ()) -- ^ Function to call with each offset value + -> Int -- ^ Initial offset + -> Int -- ^ Offset step + -> m () +overDimOff_ ds k offset step = go (totalDim ds) offset + where + go i off + | i == 0 = return () + | otherwise = k off >> go (i-1) (off+step) +{-# INLINE overDimOff_ #-} + + +-- | Go over all dimensions in reverse order keeping track of index +overDimReverseIdx :: Monad m + => Dims ds -- ^ Shape of a space + -> (Idxs ds -> a -> m a) -- ^ Function to call on each dimension + -> a -- ^ Initial value + -> m a +overDimReverseIdx U k = k U +overDimReverseIdx (d :* ds) k = overDimReverseIdx ds k' + where + dw = dimVal d + k' is = go dw + where + go i + | i <= 0 = return + | otherwise = k (Idx i :* is) >=> go (i-1) +{-# INLINE overDimReverseIdx #-} + + + +-- | Fold over all dimensions keeping track of index and offset +foldDim :: Dims ds -- ^ Shape of a space + -> (Idxs ds -> Int -> a -> a) -- ^ Function to call on each dimension + -> Int -- ^ Initial offset + -> Int -- ^ Offset step + -> a -- ^ Initial value + -> a +foldDim U k offset _step = k U offset +foldDim (d :* ds) k offset step = foldDim ds k' offset (di * step) + where + dw = dimVal d + di = fromIntegral dw + k' is = go 1 + where + go i off + | i > dw = id + | otherwise = go (i+1) (off+step) . k (Idx i :* is) off +{-# INLINE foldDim #-} + +-- | Fold over all dimensions in reverse order keeping track of index and offset +foldDimReverse :: Dims ds -- ^ Shape of a space + -> (Idxs ds -> Int -> a -> a) -- ^ Function to call on each dimension + -> Int -- ^ Initial offset + -> Int -- ^ Offset step (substracted from initial offset) + -> a -- ^ Initial value + -> a +foldDimReverse U k offset _step = k U offset +foldDimReverse (d :* ds) k offset step = foldDimReverse ds k' offset (di * step) + where + dw = dimVal d + di = fromIntegral dw + k' is = go dw + where + go i off + | i <= 0 = id + | otherwise = go (i-1) (off-step) . k (Idx i :* is) off +{-# INLINE foldDimReverse #-} + + + +-- | Fold over all dimensions keeping track of index +foldDimIdx :: Dims ds -- ^ Shape of a space + -> (Idxs ds -> a -> a) -- ^ Function to call on each dimension + -> a -- ^ Initial value + -> a +foldDimIdx U k = k U +foldDimIdx (d :* ds) k = foldDimIdx ds k' + where + dw = dimVal d + k' is = go 1 + where + go i + | i > dw = id + | otherwise = go (i+1) . k (Idx i :* is) +{-# INLINE foldDimIdx #-} + + +-- | Fold over all dimensions keeping track of total offset +foldDimOff :: Dims ds -- ^ Shape of a space + -> (Int -> a -> a) -- ^ Function to call on each dimension + -> Int -- ^ Initial offset + -> Int -- ^ Offset step + -> a -- ^ Initial value + -> a +foldDimOff ds k offset step = go (totalDim ds) offset + where + go i off + | i == 0 = id + | otherwise = go (i-1) (off+step) . k off +{-# INLINE foldDimOff #-} + + +-- | Fold over all dimensions in reverse order keeping track of index +foldDimReverseIdx :: Dims ds -- ^ Shape of a space + -> (Idxs ds -> a -> a) -- ^ Function to call on each dimension + -> a -- ^ Initial value + -> a +foldDimReverseIdx U k = k U +foldDimReverseIdx (d :* ds) k = foldDimReverseIdx ds k' + where + dw = dimVal d + k' is = go dw + where + go i + | i <= 0 = id + | otherwise = go (i-1) . k (Idx i :* is) +{-# INLINE foldDimReverseIdx #-} + + +-- | Traverse from the first index to the second index in each dimension. +-- You can combine positive and negative traversal directions +-- along different dimensions. +-- +-- Note, initial and final indices are included in the range; +-- the argument function is guaranteed to execute at least once. +overDimPart :: (Dimensions ds, Monad m) + => Idxs ds -- ^ Initial indices + -> Idxs ds -- ^ Final indices + -> (Idxs ds -> Int -> a -> m a) + -- ^ Function to call on each dimension + -> Int -- ^ Initial offset (at index @minBound :: Idxs ds@) + -- Note, this is not an offset value at initial indices. + -> Int -- ^ Offset step + -> a -- ^ initial value + -> m a +overDimPart imin imax f offset step = overDimPart' stepSizes imin imax f offset + where + stepSizes = createStepSizes (dims `inSpaceOf` imin) step + + createStepSizes :: Dims ns -> Int -> TypedList StepSize ns + createStepSizes U _ = U + createStepSizes (d :* ds) k + = StepSize k :* createStepSizes ds (k * fromIntegral (dimVal d)) + +overDimPart' :: Monad m + => TypedList StepSize ns + -> Idxs ds -> Idxs ds + -> (Idxs ds -> Int -> a -> m a) + -> Int + -> a -> m a +overDimPart' U U U k off0 = k U off0 +overDimPart' (siW :* iws) (Idx iStart :* starts) (Idx iEnd :* ends) k off0 + | iEnd >= iStart = overDimPart' iws starts ends (loop iStart) (off0 + headOff) + | otherwise = overDimPart' iws starts ends (looi iStart) (off0 + headOff) + where + StepSize iW = siW + headOff = iW * (fromIntegral iStart - 1) + loop i js off + | i > iEnd = return + | otherwise = k (Idx i :* js) off >=> loop (i+1) js (off + iW) + looi i js off + | i < iEnd = return + | otherwise = k (Idx i :* js) off >=> looi (i-1) js (off - iW) + + +newtype StepSize n = StepSize Int + +-- | Traverse from the first index to the second index in each dimension. +-- You can combine positive and negative traversal directions +-- along different dimensions. +-- +-- Note, initial and final indices are included in the range; +-- the argument function is guaranteed to execute at least once. +overDimPartIdx :: Monad m + => Idxs ds -- ^ Initial indices + -> Idxs ds -- ^ Final indices + -> (Idxs ds -> a -> m a) + -- ^ Function to call on each dimension + -> a -- ^ initial value + -> m a +overDimPartIdx U U k = k U +overDimPartIdx (start :* starts) (end :* ends) k + | iEnd >= iStart = overDimPartIdx starts ends (loop iStart) + | otherwise = overDimPartIdx starts ends (looi iStart) + where + Idx iStart = start + Idx iEnd = end + loop i is + | i > iEnd = return + | otherwise = k (Idx i :* is) >=> loop (i+1) is + looi i is + | i < iEnd = return + | otherwise = k (Idx i :* is) >=> looi (i-1) is diff --git a/src/Numeric/Dimensions/Idx.hs b/src/Numeric/Dimensions/Idx.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/Idx.hs +++ /dev/null @@ -1,209 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeFamilyDependencies #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} ------------------------------------------------------------------------------ --- | --- Module : Numeric.Dimensions.Idx --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Maintainer : chirkin@arch.ethz.ch --- --- Provides a data type Idx that enumerates through multiple dimensions. --- Lower indices go first, i.e. assumed enumeration --- is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1). --- This is also to encourage column-first matrix enumeration and array layout. --- ------------------------------------------------------------------------------ - -module Numeric.Dimensions.Idx - ( -- * Data types - Idx (..) - , appendIdx, splitIdx - ) where - - -import Control.Arrow (first) -import GHC.Exts (IsList (..)) -import Unsafe.Coerce (unsafeCoerce) - -import Numeric.Dimensions.Dim -import Numeric.Dimensions.List - - - --- | Type-level dimensional indexing with arbitrary Int values inside -data Idx (ds :: [Nat]) where - -- | Zero-rank dimensionality - scalar - Z :: Idx '[] - -- | List-like concatenation of indices - (:!) :: {-# UNPACK #-} !Int -> !(Idx ds) -> Idx (d ': ds) -infixr 5 :! - -idxToList :: Idx ds -> [Int] -idxToList Z = [] -idxToList (x :! xs) = x : idxToList xs - -idxFromList :: [Int] -> Idx ds -idxFromList [] = unsafeCoerce Z -idxFromList (x:xs) = unsafeCoerce $ x :! unsafeCoerce (idxFromList xs) - -succIdx :: Dim xs -> Idx xs -> Idx xs -succIdx _ Z = Z -succIdx ((Dn :: Dim d) :* ds) (i :! is) | i >= dimVal' @d = 1 :! succIdx ds is - | otherwise = succ i :! is -{-# INLINE succIdx #-} - -predIdx :: Dim xs -> Idx xs -> Idx xs -predIdx _ Z = Z -predIdx ((Dn :: Dim d) :* ds) (i :! is) | i <= 1 = dimVal' @d :! predIdx ds is - | otherwise = pred i :! is -{-# INLINE predIdx #-} - --- | Convert zero-based offset into Idx in a given space -toIdx :: Dim xs -> Int -> Idx xs -toIdx D _ = Z -toIdx ((Dn :: Dim d) :* ds) off = case divMod off (dimVal' @d) of - (off', i) -> i+1 :! toIdx ds off' -{-# NOINLINE toIdx #-} -- Prevent GHC panic https://ghc.haskell.org/trac/ghc/ticket/13882 - --- | Get zero-based offset of current index -fromIdx :: Dim xs -> Idx xs -> Int -fromIdx _ Z = 0 -fromIdx ((Dn :: Dim d) :* ds) (i :! is) = i - 1 + dimVal' @d * fromIdx ds is -{-# INLINE fromIdx #-} - --- | Offset difference of two indices (first idx - second idx) -diffIdx :: Dim xs -> Idx xs -> Idx xs -> Int -diffIdx _ Z _ = 0 -diffIdx ((Dn :: Dim d) :* ds) (i1:!is1) (i2:!is2) = i1 - i2 - + dimVal' @d * diffIdx ds is1 is2 -{-# INLINE diffIdx #-} - --- | Step dimension index by an Integer offset -stepIdx :: Dim ds -> Int -> Idx ds -> Idx ds -stepIdx _ _ Z = Z -stepIdx ((Dn :: Dim d) :* ds) di (i:!is) - = case divMod (di + i - 1) (dimVal' @d) of - (0 , i') -> i'+1 :! is - (di', i') -> i'+1 :! stepIdx ds di' is -{-# INLINE stepIdx #-} - --- | Append index dimension -appendIdx :: forall (as :: [Nat]) (b :: Nat) - . Idx as -> Int -> Idx (as +: b) -appendIdx Z i = i :! Z -appendIdx (j :! js) i = unsafeCoerce $ j :! (unsafeCoerce (appendIdx js i) :: Idx (Tail (as +: b))) -{-# INLINE appendIdx #-} - --- | Split index into prefix and suffix dimensioned indices -splitIdx :: forall (as :: [Nat]) (bs :: [Nat]) - . FiniteList as => Idx (as ++ bs) -> (Idx as, Idx bs) -splitIdx = splitN (order @_ @as) - where - splitN :: Int -> Idx (as ++ bs) -> (Idx as, Idx bs) - splitN 0 js = unsafeCoerce (Z, js) - splitN n (j :! js) = first (unsafeCoerce . (j :!)) - $ splitN (n-1) (unsafeCoerce js) - splitN _ Z = unsafeCoerce (Z, Z) -{-# INLINE splitIdx #-} - - -instance Show (Idx ds) where - show Z = "Idx Ø" - show xs = "Idx" ++ foldr (\i s -> " " ++ show i ++ s) "" (idxToList xs) - -instance Eq (Idx ds) where - Z == Z = True - (a:!as) == (b:!bs) = a == b && as == bs - Z /= Z = False - (a:!as) /= (b:!bs) = a /= b || as /= bs - - --- | With this instance we can slightly reduce indexing expressions --- e.g. x ! (1 :! 2 :! 4) == x ! (1 :! 2 :! 4 :! Z) -instance Num (Idx '[n]) where - (a:!Z) + (b:!Z) = (a+b) :! Z - (a:!Z) - (b:!Z) = (a-b) :! Z - (a:!Z) * (b:!Z) = (a*b) :! Z - signum (a:!Z) = signum a :! Z - abs (a:!Z) = abs a :! Z - fromInteger i = fromInteger i :! Z - - -instance Ord (Idx ds) where - compare Z Z = EQ - compare (a:!as) (b:!bs) = compare as bs `mappend` compare a b - -instance Dimensions ds => Bounded (Idx ds) where - maxBound = f (dim @ds) - where - f :: forall ns . Dim ns -> Idx ns - f D = Z - f ((Dn :: Dim n) :* ds) = dimVal' @n :! f ds - {-# INLINE maxBound #-} - minBound = f (dim @ds) - where - f :: forall (ns :: [Nat]) . Dim ns -> Idx ns - f D = Z - f (Dn :* ds) = 1 :! f ds - {-# INLINE minBound #-} - -instance IsList (Idx ds) where - type Item (Idx ds) = Int - -- | Very unsafe way to convert Haskell list into Idx. - -- If the length of a list is not equal to the length of type-level - -- dimensions, behavior is undefined (going to crash likely). - fromList = idxFromList - toList = idxToList - -instance Dimensions ds => Enum (Idx ds) where - succ = succIdx (dim @ds) - {-# INLINE succ #-} - pred = predIdx (dim @ds) - {-# INLINE pred #-} - toEnum = toIdx (dim @ds) - {-# INLINE toEnum #-} - fromEnum = fromIdx (dim @ds) - {-# INLINE fromEnum #-} - enumFrom x = take (diffIdx ds maxBound x + 1) $ iterate (succIdx ds) x - where - ds = dim @ds - {-# INLINE enumFrom #-} - enumFromTo x y | x >= y = take (diffIdx ds x y + 1) $ iterate (predIdx ds) x - | otherwise = take (diffIdx ds y x + 1) $ iterate (succIdx ds) x - where - ds = dim @ds - {-# INLINE enumFromTo #-} - enumFromThen x x' = take n $ iterate (stepIdx ds dn) x - where - ds = dim @ds - dn = diffIdx ds x' x - n = 1 + if dn == 0 then 0 - else if dn > 0 then diffIdx ds maxBound x `div` dn - else diffIdx ds x minBound `div` negate dn - {-# INLINE enumFromThen #-} - enumFromThenTo x x' y = take n $ iterate (stepIdx ds dn) x - where - ds = dim @ds - dn = diffIdx ds x' x - n = 1 + if dn == 0 then 0 - else diffIdx ds y x `div` dn - {-# INLINE enumFromThenTo #-} diff --git a/src/Numeric/Dimensions/Idxs.hs b/src/Numeric/Dimensions/Idxs.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Idxs.hs @@ -0,0 +1,427 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE Strict #-} +{-# LANGUAGE TypeApplications #-} +#if __GLASGOW_HASKELL__ >= 802 +#else +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} +#endif +----------------------------------------------------------------------------- +-- | +-- Module : Numeric.Dimensions.Idxs +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- Provides a data type Idx that enumerates through multiple dimensions. +-- Lower indices go first, i.e. assumed enumeration +-- is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1). +-- This is also to encourage column-first matrix enumeration and array layout. +-- +----------------------------------------------------------------------------- + +module Numeric.Dimensions.Idxs + ( -- * Data types + Idx (..), Idxs + , idxFromWord, unsafeIdxFromWord, idxToWord + , listIdxs, idxsFromWords + -- * Re-export dimensions types + , module Numeric.Dimensions.Dims + ) where + + +import Control.Arrow (first) +import Data.Data (Data) +import Foreign.Storable (Storable) +import GHC.Base +import GHC.Enum +import GHC.Generics (Generic, Generic1) + +import Numeric.Dimensions.Dims + + +-- | This type is used to index a single dimension; +-- the range of indices is from @1@ to @n@. +-- +-- Note, this type has a weird `Enum` instance: +-- +-- >>>fromEnum (Idx 7) +-- 6 +-- +-- The logic behind this is that the `Enum` class is used to transform +-- indices to offsets. That is, element of an array at index @k :: Idx n@ +-- is the element taken by an offset `k - 1 :: Int`. +newtype Idx n = Idx { unIdx :: Word } + deriving ( Data, Generic, Generic1, Integral, Real, Storable, Eq, Ord ) + +instance Read (Idx n) where + readsPrec d = fmap (first Idx) . readsPrec d + +instance Show (Idx n) where + showsPrec d = showsPrec d . unIdx + + +instance KnownDim n => Bounded (Idx n) where + minBound = 1 + {-# INLINE minBound #-} + maxBound = unsafeCoerce# (dim @_ @n) + {-# INLINE maxBound #-} + +-- This is a weird `Enum` instance: +-- +-- >>>fromEnum (Idx 7) +-- 6 +-- +-- The logic behind this is that the `Enum` class is used to transform +-- indices to offsets. That is, element of an array at index @k :: Idx n@ +-- is the element taken by an offset `k - 1 :: Int`. +instance KnownDim n => Enum (Idx n) where + +#ifdef UNSAFE_INDICES + succ = unsafeCoerce# ((+ 1) :: Word -> Word) +#else + succ x@(Idx i) + | x /= maxBound = Idx (i + 1) + | otherwise = succError $ "Idx " ++ show (dim @_ @n) +#endif + {-# INLINE succ #-} + +#ifdef UNSAFE_INDICES + pred = unsafeCoerce# ((+ (-1)) :: Word -> Word) +#else + pred x@(Idx i) + | x /= maxBound = Idx (i + 1) + | otherwise = predError $ "Idx " ++ show (dim @_ @n) +#endif + {-# INLINE pred #-} + +#ifdef UNSAFE_INDICES + toEnum (I# i#) = unsafeCoerce# (W# (int2Word# (i# +# 1#))) +#else + toEnum i@(I# i#) + | i >= 0 && i < dm = unsafeCoerce# (W# (int2Word# (i# +# 1#) )) + | otherwise = toEnumError ("Idx " ++ show d) i (0, dm) + where + d = unsafeCoerce# (dim @_ @n) :: Word + dm = fromIntegral d - 1 +#endif + {-# INLINE toEnum #-} + +#ifdef UNSAFE_INDICES + fromEnum (Idx (W# w#)) = I# (word2Int# w# -# 1#) +#else + fromEnum (Idx x@(W# w#)) + | x <= maxIntWord = I# (word2Int# w# -# 1#) + | otherwise = fromEnumError ("Idx " ++ show (dim @_ @n)) x + where + maxIntWord = W# (case maxInt of I# i -> int2Word# i) +#endif + {-# INLINE fromEnum #-} + + enumFrom (Idx n) + = unsafeCoerce# (enumFromTo n (unsafeCoerce# (dim @_ @n))) + {-# INLINE enumFrom #-} + enumFromThen (Idx n0) (Idx n1) + = case compare n0 n1 of + LT -> unsafeCoerce# (enumFromThenTo n0 n1 (unsafeCoerce# (dim @_ @n))) + EQ -> unsafeCoerce# (repeat n0) + GT -> unsafeCoerce# (enumFromThenTo n0 n1 1) + {-# INLINE enumFromThen #-} + enumFromTo + = unsafeCoerce# (enumFromTo :: Word -> Word -> [Word]) + {-# INLINE enumFromTo #-} + enumFromThenTo + = unsafeCoerce# (enumFromThenTo :: Word -> Word -> Word -> [Word]) + {-# INLINE enumFromThenTo #-} + +instance KnownDim n => Num (Idx n) where + +#ifdef UNSAFE_INDICES + (+) = unsafeCoerce# ((+) :: Word -> Word -> Word) +#else + (Idx a) + (Idx b) + | r > d || r < a || r < b + = errorWithoutStackTrace + $ "Num.(+){Idx " ++ show d ++ "}: sum of " + ++ show a ++ " and " ++ show b + ++ " is outside of index bounds." + | otherwise = Idx r + where + r = a + b + d = unsafeCoerce# (dim @_ @n) +#endif + {-# INLINE (+) #-} + +#ifdef UNSAFE_INDICES + (-) = unsafeCoerce# ((-) :: Word -> Word -> Word) +#else + (Idx a) - (Idx b) + | b >= a + = errorWithoutStackTrace + $ "Num.(-){Idx " ++ show (dim @_ @n) ++ "}: difference of " + ++ show a ++ " and " ++ show b + ++ " is not positive." + | otherwise = Idx (a - b) +#endif + {-# INLINE (-) #-} + +#ifdef UNSAFE_INDICES + (*) = unsafeCoerce# ((*) :: Word -> Word -> Word) +#else + (Idx a) * (Idx b) + | r > d || r < a || r < b + = errorWithoutStackTrace + $ "Num.(*){Idx " ++ show d ++ "}: product of " + ++ show a ++ " and " ++ show b + ++ " is outside of index bounds." + | otherwise = Idx r + where + r = a * b + d = unsafeCoerce# (dim @_ @n) +#endif + {-# INLINE (*) #-} + + negate = errorWithoutStackTrace + $ "Num.(*){Idx " ++ show (dim @_ @n) ++ "}: cannot negate index." + {-# INLINE negate #-} + abs = id + {-# INLINE abs #-} + signum _ = Idx 1 + {-# INLINE signum #-} + +#ifdef UNSAFE_INDICES + fromInteger = unsafeCoerce# (fromInteger :: Integer -> Word) +#else + fromInteger i + | i > 0 && i <= d = Idx $ fromInteger i + | otherwise = errorWithoutStackTrace + $ "Num.fromInteger{Idx " + ++ show d ++ "}: integer " + ++ show i ++ " is outside of index bounds." + where + d = toInteger (unsafeCoerce# (dim @_ @n) :: Word) +#endif + {-# INLINE fromInteger #-} + + +unsafeIdxFromWord :: forall d . KnownDim d => Word -> Idx d +#ifdef UNSAFE_INDICES +unsafeIdxFromWord = unsafeCoerce# +#else +unsafeIdxFromWord w + | w > 0 && w <= d = Idx w + | otherwise = errorWithoutStackTrace + $ "idxFromWord{Idx " + ++ show d ++ "}: word " + ++ show w ++ " is outside of index bounds." + where + d = unsafeCoerce# (dim @_ @d) +#endif +{-# INLINE unsafeIdxFromWord #-} + +idxFromWord :: forall d . KnownDim d => Word -> Maybe (Idx d) +idxFromWord w + | w > 0 && w <= unsafeCoerce# (dim @_ @d) = Just (Idx w) + | otherwise = Nothing +{-# INLINE idxFromWord #-} + + +idxToWord :: Idx d -> Word +idxToWord = unsafeCoerce# +{-# INLINE idxToWord #-} + +{-# RULES +"fromIntegral/idxToWord" + fromIntegral = idxToWord + #-} + + +-- | Type-level dimensional indexing with arbitrary Word values inside. +-- Most of the operations on it require `Dimensions` constraint, +-- because the @Idxs@ itself does not store info about dimension bounds. +-- +-- Note, this type has a special `Enum` instance: +-- `fromEnum` gives an offset of the index in a flat 1D array; +-- this is in line with a weird `Enum` instance of `Idx` type. +type Idxs (xs :: [k]) = TypedList Idx xs + + +listIdxs :: Idxs xs -> [Word] +listIdxs = unsafeCoerce# +{-# INLINE listIdxs #-} + + +idxsFromWords :: forall ds . Dimensions ds => [Word] -> Maybe (Idx ds) +idxsFromWords = unsafeCoerce# . go (listDims (dims @_ @ds)) + where + go [] [] = Just [] + go (d : ds) (i : is) + | i > 0 && i <= d = (i:) <$> go ds is + go _ _ = Nothing + + + +instance Eq (Idxs xs) where + (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool) + {-# INLINE (==) #-} + +-- | Compare indices by their importance in lexicorgaphic order +-- from the last dimension to the first dimension +-- (the last dimension is the most significant one) @O(Length xs)@. +-- +-- Literally, +-- +-- > compare a b = compare (reverse $ listIdxs a) (reverse $ listIdxs b) +-- +-- This is the same @compare@ rule, as for `Dims`. +-- Another reason to reverse the list of indices is to have a consistent +-- behavior when calculating index offsets: +-- +-- > sort == sortOn fromEnum +-- +instance Ord (Idxs xs) where + compare a b = compare (reverse $ listIdxs a) (reverse $ listIdxs b) + {-# INLINE compare #-} + + +instance Show (Idxs xs) where + show ds = "Idxs " ++ show (listIdxs ds) + showsPrec p ds + = showParen (p >= 10) + $ showString "Idxs " . showsPrec p (listIdxs ds) + +-- | With this instance we can slightly reduce indexing expressions, e.g. +-- +-- > x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U) +-- +instance KnownDim n => Num (Idxs '[n]) where + (a:*U) + (b:*U) = (a+b) :* U + {-# INLINE (+) #-} + (a:*U) - (b:*U) = (a-b) :* U + {-# INLINE (-) #-} + (a:*U) * (b:*U) = (a*b) :* U + {-# INLINE (*) #-} + signum (a:*U) = signum a :* U + {-# INLINE signum #-} + abs (a:*U) = abs a :* U + {-# INLINE abs #-} + fromInteger i = fromInteger i :* U + {-# INLINE fromInteger #-} + +instance Dimensions ds => Bounded (Idxs ds) where + maxBound = f (dims @_ @ds) + where + f :: forall ns . Dims ns -> Idxs ns + f U = U + f (d :* ds) = Idx (dimVal d) :* f ds + {-# INLINE maxBound #-} + minBound = f (dims @_ @ds) + where + f :: forall ns . Dims ns -> Idxs ns + f U = U + f (_ :* ds) = Idx 1 :* f ds + {-# INLINE minBound #-} + + +instance Dimensions ds => Enum (Idxs ds) where + + succ = go (dims @_ @ds) + where + go :: forall ns . Dims ns -> Idxs ns -> Idxs ns + go U U = succError $ "Idxs " ++ show (listDims $ dims @_ @ds) + go (d :* ds) (Idx i :* is) + | i == dimVal d = Idx 1 :* go ds is + | otherwise = Idx (i+1) :* is + {-# INLINE succ #-} + + pred = go (dims @_ @ds) + where + go :: forall ns . Dims ns -> Idxs ns -> Idxs ns + go U U = predError $ "Idxs " ++ show (listDims $ dims @_ @ds) + go (d :* ds) (Idx i :* is) + | i == 1 = Idx (dimVal d) :* go ds is + | otherwise = Idx (i-1) :* is + {-# INLINE pred #-} + + toEnum i = go dds $ fromIntegral i + where + dds = dims @_ @ds + go :: forall ns . Dims ns -> Word -> Idxs ns + go U 0 = U + go U _ = toEnumError ("Idxs " ++ show (listDims dds)) + i (0, totalDim dds - 1) + go (d :* ds) off = case divMod off (dimVal d) of + (off', j) -> Idx (j+1) :* go ds off' + {-# INLINE toEnum #-} + + fromEnum = fromIntegral . go 1 (dims @_ @ds) + where + go :: forall ns . Word -> Dims ns -> Idxs ns -> Word + go _ U U = 0 + go m (d :* ds) (Idx i :* is) = m * (i - 1) + go (m * dimVal d) ds is + {-# INLINE fromEnum #-} + + enumFrom x = take (diffIdx (dims @_ @ds) maxBound x + 1) $ iterate succ x + {-# INLINE enumFrom #-} + + enumFromTo x y | x >= y = take (diffIdx ds x y + 1) $ iterate pred x + | otherwise = take (diffIdx ds y x + 1) $ iterate succ x + where + ds = dims @_ @ds + {-# INLINE enumFromTo #-} + + enumFromThen x x' = take n $ iterate (stepIdx ds dn) x + where + ds = dims @_ @ds + dn = diffIdx ds x' x + n = 1 + if dn == 0 + then 0 + else if dn > 0 + then diffIdx ds maxBound x `div` dn + else diffIdx ds x minBound `div` negate dn + {-# INLINE enumFromThen #-} + + enumFromThenTo x x' y = take n $ iterate (stepIdx ds dn) x + where + ds = dims @_ @ds + dn = diffIdx ds x' x + n = 1 + if dn == 0 then 0 + else diffIdx ds y x `div` dn + {-# INLINE enumFromThenTo #-} + + + +-------------------------------------------------------------------------------- + + + +-- | Offset difference of two indices @idx1 - idx2@ +diffIdx :: Dims xs -> Idxs xs -> Idxs xs -> Int +diffIdx U U U = 0 +diffIdx (d :* ds) (Idx i1 :* is1) (Idx i2 :* is2) + = fromIntegral i1 - fromIntegral i2 + + fromIntegral (dimVal d) * diffIdx ds is1 is2 +{-# INLINE diffIdx #-} + +-- | Step dimension index by an Int offset +stepIdx :: Dims ds -> Int -> Idxs ds -> Idxs ds +stepIdx U _ U = U +stepIdx (d :* ds) di (Idx i :* is) + = case divMod (di + fromIntegral i - 1) (fromIntegral (dimVal d)) of + (0 , i') -> Idx (fromIntegral (i'+1)) :* is + (di', i') -> Idx (fromIntegral (i'+1)) :* stepIdx ds di' is +{-# INLINE stepIdx #-} diff --git a/src/Numeric/Dimensions/List.hs b/src/Numeric/Dimensions/List.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/List.hs +++ /dev/null @@ -1,436 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE RoleAnnotations #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeFamilyDependencies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE CPP #-} --------------------------------------------------------------------------------- --- | --- Module : Numeric.Dimensions.List --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Maintainer : chirkin@arch.ethz.ch --- --- Provides type-level operations on lists. --- --- * Note for GHC 8.0 --- Due to --- some complex type families could not be truly kind-polymorphic before GHC 8.2, --- thus I specialized them to work only on `[Nat]` and `[XNat]`. --- --------------------------------------------------------------------------------- - -module Numeric.Dimensions.List - ( -- * Basic operations - type (++), type (:+), type (+:) - , Empty, Cons, Snoc, Head - , Tail, Init, Last, Concat, Reverse, Take, Drop - -- * Working with concatenations - , Suffix, Prefix, IsPrefix, IsSuffix - -- * Term level functions - , ConcatList (..), FiniteList (..), TypeList (..) - -- * Term level inference of type-level functions - , inferConcat, inferSuffix, inferPrefix, ConcatEvidence, FiniteListEvidence - , inferKnownLength - , inferTailFiniteList, inferConcatFiniteList - , inferPrefixFiniteList, inferSuffixFiniteList - , inferSnocFiniteList, inferInitFiniteList - , inferTakeNFiniteList, inferDropNFiniteList, inferReverseFiniteList - ) where - -import Data.Proxy (Proxy (..)) -import Data.Type.Equality ((:~:)(..)) -import Numeric.TypeLits -import Unsafe.Coerce (unsafeCoerce) - --- | Synonym for a type-level cons --- (injective, since this is just a synonym for the list constructor) -type (a :: k) :+ (as :: [k]) = a ': as -infixr 5 :+ --- | Prefix-style synonym for cons -type Cons (n :: k) (ns :: [k]) = n :+ ns - --- | Synonym for a type-level snoc (injective!) -type (ns :: [k]) +: (n :: k) = Snoc ns n -infixl 5 +: --- | Prefix-style synonym for snoc -type Snoc (ns :: [k]) (n :: k) = GetSnoc (DoSnoc ns n) - - --- | List concatenation -type family (as :: [k]) ++ (bs :: [k]) :: [k] where - (++) '[] bs = bs - (++) as '[] = as - (++) (a :+ as) bs = a :+ (as ++ bs) -infixr 5 ++ - --- | Prefix-style synonym for concatenation -type Concat (as :: [k]) (bs :: [k]) = as ++ bs - - --- | Reverse a type-level list (injective!) -type Reverse (xs :: [k]) = Reversed (DoReverse xs) - - --- | Synonym for an empty type-level list -type Empty = '[] - - -type family Take (n::Nat) (xs :: [k]) :: [k] where - Take _ '[] = '[] - Take 0 xs = '[] - Take n (x :+ xs) = x :+ Take (n-1) xs - - -type family Drop (n::Nat) (xs :: [k]) :: [k] where - Drop _ '[] = '[] - Drop 0 xs = xs - Drop n (x :+ xs) = Drop (n-1) xs - -type family Suffix (as :: [k]) (asbs :: [k]) :: [k] where - Suffix '[] bs = bs - Suffix as as = '[] - Suffix (_ :+ as) (_ :+ asbs) = Suffix as asbs - -type family Prefix (bs :: [k]) (asbs :: [k]) :: [k] where - Prefix '[] as = as - Prefix bs bs = '[] - Prefix bs asbs = Take (Length asbs - Length bs) asbs - - -type family IsPrefix (as :: [k]) (asbs :: [k]) :: Bool where - IsPrefix '[] _ = 'True - IsPrefix (a :+ as) (a :+ asbs) = IsPrefix as asbs - IsPrefix as as = 'True - IsPrefix _ _= 'False - -type family IsSuffix (as :: [k]) (asbs :: [k]) :: Bool where - IsSuffix '[] _ = 'True - IsSuffix bs bs = 'True - IsSuffix bs (_ :+ sbs) = IsSuffix bs sbs - IsSuffix _ _ = 'False - - -type family Head (xs :: [k]) :: k where - Head (x :+ xs) = x - Head '[] = TypeError ( 'Text - "Head -- empty type-level list." - ) - -type family Tail (xs :: [k]) :: [k] where - Tail (x :+ xs) = xs - Tail '[] = TypeError ( 'Text - "Tail -- empty type-level list." - ) - -type family Init (xs :: [k]) :: [k] where - Init '[x] = '[] - Init (x :+ xs) = x :+ Init xs - Init '[] = TypeError ( 'Text - "Init -- empty type-level list." - ) - -type family Last (xs :: [k]) :: k where - Last '[x] = x - Last (x :+ xs) = Last xs - Last '[] = TypeError ( 'Text - "Last -- empty type-level list." - ) - - --- | Represent a triple of lists forming a relation `as ++ bs ~ asbs` -class ( asbs ~ Concat as bs - , as ~ Prefix bs asbs - , bs ~ Suffix as asbs - , IsSuffix bs asbs ~ 'True - , IsPrefix as asbs ~ 'True - ) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) - | as bs -> asbs - , as asbs -> bs - , bs asbs -> as where - tlPrefix :: ConcatEvidence as bs asbs -> Proxy as - tlSuffix :: ConcatEvidence as bs asbs -> Proxy bs - tlConcat :: ConcatEvidence as bs asbs -> Proxy asbs - -instance ( asbs ~ Concat as bs - , as ~ Prefix bs asbs - , bs ~ Suffix as asbs - , IsSuffix bs asbs ~ 'True - , IsPrefix as asbs ~ 'True - ) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) where - tlPrefix _ = Proxy - {-# INLINE tlPrefix #-} - tlSuffix _ = Proxy - {-# INLINE tlSuffix #-} - tlConcat _ = Proxy - {-# INLINE tlConcat #-} - - --- | Type level list, used together with FiniteList typeclass -data TypeList (xs :: [k]) where - TLEmpty :: TypeList '[] - TLCons :: FiniteList xs => !(Proxy# x) -> !(TypeList xs) -> TypeList (x :+ xs) - -instance Show (TypeList xs) where - show TLEmpty = "TLEmpty" - show (TLCons _ xs) = "TLCons " ++ show xs - --- | Type-level list that is known to be finite. --- Basically, provides means to get its length and term-level rep (via TypeList) -class FiniteList (xs :: [k]) where - -- | Length of a type-level list at type level - type Length xs :: Nat - -- | Length of a type-level list at term level - order :: Int - -- | Get type-level constructed list - tList :: TypeList xs - - - -instance FiniteList ('[] :: [k]) where - type Length '[] = 0 - order = 0 - {-# INLINE order #-} - tList = TLEmpty - {-# INLINE tList #-} - -instance FiniteList xs => FiniteList (x :+ xs :: [k]) where - type Length (x :+ xs) = Length xs + 1 - order = 1 + order @k @xs - {-# INLINE order #-} - tList = TLCons proxy# (tList @k @xs) - {-# INLINE tList #-} - - - -unsafeEqEvidence :: forall x y . Evidence (x ~ y) -unsafeEqEvidence = case (unsafeCoerce Refl :: x :~: y) of Refl -> Evidence -{-# INLINE unsafeEqEvidence #-} - --- | Length of a finite list is known and equal to `order` of the list -inferKnownLength :: forall xs . FiniteList xs => Evidence (KnownDim (Length xs)) -inferKnownLength = reifyDim (order @_ @xs) f - where - f :: forall n . KnownDim n => Proxy# n -> Evidence (KnownDim (Length xs)) - f _ = unsafeCoerce (Evidence @(KnownDim n)) -{-# INLINE inferKnownLength #-} - - --- | Tail of the list is also known list -inferTailFiniteList :: forall xs . FiniteList xs => Maybe (Evidence (FiniteList (Tail xs))) -inferTailFiniteList = case tList @_ @xs of - TLEmpty -> Nothing - TLCons _ _ -> Just Evidence -{-# INLINE inferTailFiniteList #-} - --- | Infer that concatenation is also finite -inferConcatFiniteList :: forall as bs - . (FiniteList as, FiniteList bs) - => Evidence (FiniteList (as ++ bs)) -inferConcatFiniteList = case tList @_ @as of - TLEmpty -> Evidence - TLCons _ (_ :: TypeList as') -> case inferConcatFiniteList @as' @bs of - Evidence -> case unsafeEqEvidence @(as ++ bs) @(Head as ': (as' ++ bs)) of - Evidence -> Evidence -{-# INLINE inferConcatFiniteList #-} - - --- | Infer that prefix is also finite -inferPrefixFiniteList :: forall bs asbs - . (IsSuffix bs asbs ~ 'True, FiniteList bs, FiniteList asbs) - => Evidence (FiniteList (Prefix bs asbs)) -inferPrefixFiniteList = reifyDim (order @_ @asbs - order @_ @bs) f - where - f :: forall n . KnownDim n => Proxy# n -> Evidence (FiniteList (Prefix bs asbs)) - f _ = unsafeCoerce (inferTakeNFiniteList @n @asbs) -{-# INLINE inferPrefixFiniteList #-} - --- | Infer that suffix is also finite -inferSuffixFiniteList :: forall as asbs - . (IsPrefix as asbs ~ 'True, FiniteList as, FiniteList asbs) - => Evidence (FiniteList (Suffix as asbs)) -inferSuffixFiniteList = case tList @_ @as of - TLEmpty -> Evidence - TLCons _ (_ :: TypeList as') -> case tList @_ @asbs of - TLCons _ (_ :: TypeList asbs') -> case unsafeEqEvidence @(IsPrefix as' asbs') @'True - `sumEvs` unsafeEqEvidence @(Suffix as' asbs') @(Suffix as asbs) of - Evidence -> inferSuffixFiniteList @as' @asbs' -{-# INLINE inferSuffixFiniteList #-} - --- | Make snoc almost as good as cons -inferSnocFiniteList :: forall xs z - . FiniteList xs - => Evidence (FiniteList (xs +: z)) -inferSnocFiniteList = case tList @_ @xs of - TLEmpty -> Evidence - TLCons _ (_ :: TypeList xs') -> case inferSnocFiniteList @xs' @z - `sumEvs` unsafeEqEvidence @(Head xs :+ (xs' +: z)) @(xs +: z) of - Evidence -> Evidence -{-# INLINE inferSnocFiniteList #-} - --- | Init of the list is also known list -inferInitFiniteList :: forall xs - . FiniteList xs - => Maybe (Evidence (FiniteList (Init xs))) -inferInitFiniteList = case tList @_ @xs of - TLEmpty -> Nothing - TLCons _ TLEmpty -> Just Evidence - TLCons _ (TLCons _ _ :: TypeList xs') -> case inferInitFiniteList @xs' of - Just Evidence -> Just Evidence - Nothing -> Nothing -{-# INLINE inferInitFiniteList #-} - --- | Take KnownDim of the list is also known list -inferTakeNFiniteList :: forall n xs - . (KnownDim n, FiniteList xs) - => Evidence (FiniteList (Take n xs)) -inferTakeNFiniteList = magic @n @xs (dimVal' @n) (tList @_ @xs) - where - magic :: forall m ns . Int -> TypeList ns -> Evidence (FiniteList (Take m ns)) - magic _ TLEmpty = Evidence - magic 0 _ = case unsafeEqEvidence @(Take m ns) @'[] of - Evidence -> Evidence - magic n (TLCons _ tl) = case unsafeEqEvidence @(Head ns ': Take (m-1) (Tail ns)) @(Take m ns) of - Evidence -> case magic @(m-1) @(Tail ns) (n-1) tl of - Evidence -> Evidence -{-# INLINE inferTakeNFiniteList #-} - --- | Drop KnownDim of the list is also known list -inferDropNFiniteList :: forall n xs - . (KnownDim n, FiniteList xs) - => Evidence (FiniteList (Drop n xs)) -inferDropNFiniteList = case magic (dimVal' @n) (tList @_ @xs) of - TLEmpty -> Evidence - TLCons _ _ -> Evidence - where - magic :: forall ns . Int -> TypeList ns -> TypeList (Drop n ns) - magic _ TLEmpty = TLEmpty - magic 0 tl = unsafeCoerce tl - magic n (TLCons _ tl) = unsafeCoerce $ magic (n-1) tl -{-# INLINE inferDropNFiniteList #-} - --- | Reverse of the list is also known list -inferReverseFiniteList :: forall xs . FiniteList xs => Evidence (FiniteList (Reverse xs)) -inferReverseFiniteList = case magic (tList @_ @xs) TLEmpty of - TLEmpty -> Evidence - TLCons _ _ -> Evidence - where - magic :: forall (ns :: [k]) (bs :: [k]) - . FiniteList bs - => TypeList ns -> TypeList bs -> TypeList (Reverse ns) - magic TLEmpty xs = unsafeCoerce xs - magic (TLCons p sx) xs = magic (unsafeCoerce sx :: TypeList ns) (TLCons p xs) -{-# INLINE inferReverseFiniteList #-} - - --------------------------------------------------------------------------------- ----- Constructing evidence for our constraints --------------------------------------------------------------------------------- - --- | Pattern-matching on the constructor of this type --- brings an evidence that `as ++ bs ~ asbs` -type ConcatEvidence (as :: [k]) (bs :: [k]) (asbs :: [k]) - = Evidence ( asbs ~ Concat as bs - , as ~ Prefix bs asbs - , bs ~ Suffix as asbs - , IsSuffix bs asbs ~ 'True - , IsPrefix as asbs ~ 'True - ) - --- | Pattern-matching on the constructor of this type --- brings an evidence that the type-level parameter list is finite -type FiniteListEvidence (xs :: [k]) - = Evidence (FiniteList xs) - - --- | Any two type-level lists can be concatenated, --- so we just fool the compiler by unsafeCoercing proxy-like data type. -inferConcat :: forall as bs . ConcatEvidence as bs (as ++ bs) -inferConcat = unsafeCoerce (Evidence :: ConcatEvidence ('[] :: [()]) ('[] :: [()]) ('[] :: [()])) -{-# INLINE inferConcat #-} - - --- | `as` being prefix of `asbs` is enough to infer some concatenation relations --- so we just fool the compiler by unsafeCoercing proxy-like data type. -inferSuffix :: forall as asbs - . IsPrefix as asbs ~ 'True - => ConcatEvidence as (Suffix as asbs) asbs -inferSuffix = unsafeCoerce (Evidence :: ConcatEvidence ('[] :: [()]) ('[] :: [()]) ('[] :: [()])) -{-# INLINE inferSuffix #-} - - --- | `bs` being suffix of `asbs` is enough to infer some concatenation relations --- so we just fool the compiler by unsafeCoercing proxy-like data type. -inferPrefix :: forall bs asbs - . IsSuffix bs asbs ~ 'True - => ConcatEvidence (Prefix bs asbs) bs asbs -inferPrefix = unsafeCoerce (Evidence :: ConcatEvidence ('[] :: [()]) ('[] :: [()]) ('[] :: [()])) -{-# INLINE inferPrefix #-} - - --------------------------------------------------------------------------------- ----- Tricks to make some type-level operations injective --------------------------------------------------------------------------------- - - --- | A special data type that can have either a single element, --- or more than two. --- This feature is not enforced in the type system - this is just a way to make injective Snoc. -data Snocing k = SSingle k | Snocing [k] - -type family DoSnoc (xs :: [k]) (z::k) = (ys :: Snocing k) | ys -> xs z where - DoSnoc '[] x = 'SSingle x -#if __GLASGOW_HASKELL__ >= 802 - DoSnoc (x :+ xs :: [k]) (y :: k) = ('Snocing (x :+ GetSnoc (DoSnoc xs y) :: [k]) :: Snocing k) -#else - DoSnoc (x :+ xs :: [Nat]) (y :: Nat) = ('Snocing (x :+ GetSnoc (DoSnoc xs y) :: [Nat]) :: Snocing Nat) - DoSnoc (x :+ xs :: [XNat]) (y :: XNat) = ('Snocing (x :+ GetSnoc (DoSnoc xs y) :: [XNat]) :: Snocing XNat) -#endif - -type family GetSnoc (xs :: Snocing k) = (ys :: [k]) | ys -> xs where - GetSnoc ('SSingle x) = '[x] -#if __GLASGOW_HASKELL__ >= 802 - GetSnoc ('Snocing (y :+ x :+ xs)) = y :+ x :+ xs -#else - GetSnoc ('Snocing (y :+ x :+ xs) :: Snocing Nat) = (y :+ x :+ xs :: [Nat]) - GetSnoc ('Snocing (y :+ x :+ xs) :: Snocing XNat) = (y :+ x :+ xs :: [XNat]) -#endif - --- | Another data type to make Reverse injective. -data Reversing k = REmpty | Reversing [k] - -type family Reversed (ts :: Reversing k) = (rs :: [k]) | rs -> ts where - Reversed 'REmpty = '[] -#if __GLASGOW_HASKELL__ >= 802 - Reversed ('Reversing (x :+ xs)) = x :+ xs -#else - Reversed ('Reversing (x :+ xs) :: Reversing Nat) = (x :+ xs :: [Nat]) - Reversed ('Reversing (x :+ xs) :: Reversing XNat) = (x :+ xs :: [XNat]) -#endif - - -type family DoReverse (as :: [k]) = (rs :: Reversing k) | rs -> as where - DoReverse '[] = 'REmpty -#if __GLASGOW_HASKELL__ >= 802 - DoReverse (a :+ as) = 'Reversing (Reversed (DoReverse as) +: a) -#else - DoReverse (a :+ as :: [Nat]) = ('Reversing (Reversed (DoReverse as) +: a :: [Nat]) :: Reversing Nat) - DoReverse (a :+ as :: [XNat]) = ('Reversing (Reversed (DoReverse as) +: a :: [XNat]) :: Reversing XNat) -#endif diff --git a/src/Numeric/Dimensions/Traverse.hs b/src/Numeric/Dimensions/Traverse.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/Traverse.hs +++ /dev/null @@ -1,289 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE UnboxedTuples #-} -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE Strict #-} ------------------------------------------------------------------------------ --- | --- Module : Numeric.Dimensions.Traverse --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Maintainer : chirkin@arch.ethz.ch --- --- Map a function over all dimensions provided dimension indices or offsets. --- ------------------------------------------------------------------------------ - -module Numeric.Dimensions.Traverse - ( overDim#, overDim_#, overDimIdx#, overDimIdx_#, overDimOff#, overDimOff_# - , overDimPart# - , foldDim, foldDimIdx, foldDimOff - , foldDimReverse, foldDimReverseIdx - ) where - - -import GHC.Exts - -import Numeric.Dimensions.Dim -import Numeric.Dimensions.Idx - - - --- | Traverse over all dimensions keeping track of index and offset -overDim# :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> State# s -> (# State# s, a #)) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a - -> State# s - -> (# State# s, a #) -overDim# ds f off0# step# a0 s0 = case overDim'# ds g off0# a0 s0 of - (# s1, _, a1 #) -> (# s1, a1 #) - where - g i off# a s = case f i off# a s of - (# t, b #) -> (# t, off# +# step#, b #) -{-# INLINE overDim# #-} - --- | Fold over all dimensions keeping track of index and offset -foldDim :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> a) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a -> a -foldDim ds f off0# step# a0 = case foldDim' ds g off0# a0 of - (# _, a1 #) -> a1 - where - g i off# a = (# off# +# step#, f i off# a #) -{-# INLINE foldDim #-} - --- | Fold over all dimensions in reverse order keeping track of index and offset -foldDimReverse :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> a) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step (substracted from initial offset) - -> a -> a -foldDimReverse ds f off0# step# a0 = case foldDimReverse' ds g (off0# +# n# *# step# -# step#) a0 of - (# _, a1 #) -> a1 - where - !(I# n#) = dimVal ds - g i off# a = (# off# -# step#, f i off# a #) -{-# INLINE foldDimReverse #-} - - - --- | Same as overDim#, but with no return value -overDim_# :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> State# s -> State# s) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> State# s - -> State# s -overDim_# ds f off0# step# s0 = case overDim_'# ds g off0# s0 of - (# s1, _ #) -> s1 - where - g i off# s = (# f i off# s, off# +# step# #) -{-# INLINE overDim_# #-} - --- | Traverse over all dimensions keeping track of indices -overDimIdx# :: Dim (ds :: [Nat]) - -> (Idx ds -> a -> State# s -> (# State# s, a #)) - -> a - -> State# s - -> (# State# s, a #) -overDimIdx# D f = f Z -overDimIdx# ((Dn :: Dim n) :* (!ds)) f = overDimIdx# ds (loop 1) - where - n = dimVal' @n - loop i js a s | i > n = (# s, a #) - | otherwise = case f (i:!js) a s of - (# s', b #) -> loop (i+1) js b s' - --- | Fold all dimensions keeping track of indices -foldDimIdx :: Dim (ds :: [Nat]) - -> (Idx ds -> a -> a) - -> a -> a -foldDimIdx D f = f Z -foldDimIdx ((Dn :: Dim n) :* (!ds)) f = foldDimIdx ds (loop 1) - where - n = dimVal' @n - loop i js a | i > n = a - | otherwise = loop (i+1) js $! f (i:!js) a - --- | Fold all dimensions in reverse order keeping track of indices -foldDimReverseIdx :: Dim (ds :: [Nat]) - -> (Idx ds -> a -> a) - -> a -> a -foldDimReverseIdx D f = f Z -foldDimReverseIdx ((Dn :: Dim n) :* (!ds)) f = foldDimReverseIdx ds (loop n) - where - n = dimVal' @n - loop i js a | i > n = a - | otherwise = loop (i-1) js $! f (i:!js) a - - - --- | Traverse over all dimensions keeping track of indices, with no return value -overDimIdx_# :: Dim (ds :: [Nat]) - -> (Idx ds -> State# s -> State# s) - -> State# s - -> State# s -overDimIdx_# D f = f Z -overDimIdx_# ((Dn :: Dim n) :* (!ds)) f = overDimIdx_# ds (loop 1) - where - n = dimVal' @n - loop i js s | i > n = s - | otherwise = loop (i+1) js (f (i:!js) s) - --- | Traverse over all dimensions keeping track of total offset -overDimOff# :: Dim (ds :: [Nat]) - -> (Int# -> a -> State# s -> (# State# s, a #)) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a -> State# s -> (# State# s, a #) -overDimOff# ds f off0# step# = loop off0# - where - off1# = case dimVal ds of I# n# -> n# *# step# +# off0# - cond# = if isTrue# (off1# >=# off0#) - then \off -> isTrue# (off >=# off1#) - else \off -> isTrue# (off <=# off1#) - loop off# a s | cond# off# = (# s, a #) - | otherwise = case f off# a s of - (# s', b #) -> loop (off# +# step#) b s' - --- | Fold over all dimensions keeping track of total offset -foldDimOff :: Dim (ds :: [Nat]) - -> (Int# -> a -> a) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a -> a -foldDimOff ds f off0# step# = loop off0# - where - off1# = case dimVal ds of I# n# -> n# *# step# +# off0# - cond# = if isTrue# (off1# >=# off0#) - then \off -> isTrue# (off >=# off1#) - else \off -> isTrue# (off <=# off1#) - loop off# a | cond# off# = a - | otherwise = loop (off# +# step#) $! f off# a - - --- | Traverse over all dimensions keeping track of total offset, with not return value -overDimOff_# :: Dim (ds :: [Nat]) - -> (Int# -> State# s -> State# s) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> State# s -> State# s -overDimOff_# ds f off0# step# = loop off0# - where - off1# = case dimVal ds of I# n# -> n# *# step# +# off0# - cond# = if isTrue# (off1# >=# off0#) - then \off -> isTrue# (off >=# off1#) - else \off -> isTrue# (off <=# off1#) - loop off# s | cond# off# = s - | otherwise = loop (off# +# step#) (f off# s) - --- | Traverse from the first index to the second index in each dimension. --- Indices must be within Dim range, which is not checked. --- You can combine positive and negative traversal directions along different dimensions. -overDimPart# :: forall (ds :: [Nat]) a s - . Dimensions ds - => Idx ds - -> Idx ds - -> (Idx ds -> Int# -> a -> State# s -> (# State# s, a #)) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a - -> State# s - -> (# State# s, a #) -overDimPart# imin imax f off0 step = overDimPart'# offs imin imax f off0 - where - offs = createOffsets (dim @ds) (I# step) - createOffsets :: forall (ns :: [Nat]) . Dim ns -> Int -> Idx ns - createOffsets D _ = Z - createOffsets ((Dn :: Dim n) :* (!ds)) k = k :! createOffsets ds (k * dimVal' @n) - - - - - - -overDim'# :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> State# s -> (# State# s, Int#, a #)) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> a - -> State# s - -> (# State# s, Int#, a #) -overDim'# D f = f Z -overDim'# ((Dn :: Dim n) :* (!ds)) f = overDim'# ds (loop 1) - where - n = dimVal' @n - loop i js off# a s | i > n = (# s , off# , a #) - | otherwise = case f (i:!js) off# a s of - (# s', off1#, b #) -> loop (i+1) js off1# b s' - - - -foldDim' :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> (# Int#, a #)) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> a -> (# Int#, a #) -foldDim' D f = f Z -foldDim' ((Dn :: Dim n) :* (!ds)) f = foldDim' ds (loop 1) - where - n = dimVal' @n - loop i js off# a | i > n = (# off#, a #) - | otherwise = case f (i:!js) off# a of - (# off1#, b #) -> loop (i+1) js off1# b - -foldDimReverse' :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> (# Int#, a #)) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> a -> (# Int#, a #) -foldDimReverse' D f = f Z -foldDimReverse' ((Dn :: Dim n) :* (!ds)) f = foldDimReverse' ds (loop n) - where - n = dimVal' @n - loop i js off# a | i <= 0 = (# off#, a #) - | otherwise = case f (i:!js) off# a of - (# off1#, b #) -> loop (i-1) js off1# b - - - -overDim_'# :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> State# s -> (# State# s, Int# #)) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> State# s - -> (# State# s, Int# #) -overDim_'# D f = f Z -overDim_'# ((Dn :: Dim n) :* (!ds)) f = overDim_'# ds (loop 1) - where - n = dimVal' @n - loop i js off# s | i > n = (# s , off# #) - | otherwise = case f (i:!js) off# s of - (# s', off1# #) -> loop (i+1) js off1# s' - - -overDimPart'# :: Idx (ds :: [Nat]) - -> Idx (ds :: [Nat]) - -> Idx (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> State# s -> (# State# s, a #)) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> a - -> State# s - -> (# State# s, a #) -overDimPart'# _ Z Z f off0# = f Z off0# -overDimPart'# (I# iW:!iws) (iMin:!mins) (iMax:!maxs) f off0# - | iMax >= iMin = overDimPart'# iws mins maxs (loop iMin) (off0# +# minOff#) - | otherwise = overDimPart'# iws mins maxs (looi iMin) (off0# +# minOff#) - where - minOff# = case iMin of I# i -> iW *# (i -# 1#) - loop i js off# a s | i > iMax = (# s, a #) - | otherwise = case f (i:!js) off# a s of - (# s', b #) -> loop (i+1) js (off# +# iW) b s' - looi i js off# a s | i < iMax = (# s, a #) - | otherwise = case f (i:!js) off# a s of - (# s', b #) -> looi (i-1) js (off# -# iW) b s' diff --git a/src/Numeric/Dimensions/Traverse/IO.hs b/src/Numeric/Dimensions/Traverse/IO.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/Traverse/IO.hs +++ /dev/null @@ -1,113 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UnboxedTuples #-} ------------------------------------------------------------------------------ --- | --- Module : Numeric.Dimensions.Traverse.IO --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Maintainer : chirkin@arch.ethz.ch --- --- Map a function over all dimensions provided dimension indices or offsets. --- This module provides a variant of traversal that lives in IO monad. --- ------------------------------------------------------------------------------ - -module Numeric.Dimensions.Traverse.IO - ( overDim, overDim_, overDimIdx, overDimIdx_, overDimOff, overDimOff_, overDimPart - , foldDim, foldDimIdx, foldDimOff - ) where - - -import GHC.Exts -import GHC.IO (IO (..)) - -import Numeric.Dimensions.Dim -import Numeric.Dimensions.Idx -import Numeric.Dimensions.Traverse - - - --- | Traverse over all dimensions keeping track of index and offset -overDim :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> IO a) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a -> IO a -overDim ds stf off0# step# = IO . overDim# ds (\i off# a -> case stf i off# a of - IO f -> f - ) off0# step# -{-# INLINE overDim #-} - --- | Traverse over all dimensions keeping track of indices -overDimIdx :: Dim (ds :: [Nat]) - -> (Idx ds -> a -> IO a) - -> a -> IO a -overDimIdx ds stf = IO . overDimIdx# ds (\i a -> case stf i a of IO f -> f) -{-# INLINE overDimIdx #-} - --- | Traverse over all dimensions keeping track of total offset -overDimOff :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> IO a) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a -> IO a -overDimOff ds stf off0# step# = IO . overDim# ds (\i off# a -> case stf i off# a of - IO f -> f - ) off0# step# -{-# INLINE overDimOff #-} - - - --- | Same as overDim#, but with no return value -overDim_ :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> IO ()) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> IO () -overDim_ ds stf off0# step# = fst'# $ overDim_# ds (\i off# -> fst# (stf i off#) - ) off0# step# -{-# INLINE overDim_ #-} - --- | Traverse over all dimensions keeping track of indices, with no return value -overDimIdx_ :: Dim (ds :: [Nat]) - -> (Idx ds -> IO ()) - -> IO () -overDimIdx_ ds stf = fst'# $ overDimIdx_# ds (\i -> fst# (stf i)) -{-# INLINE overDimIdx_ #-} - - --- | Traverse over all dimensions keeping track of total offset, with not return value -overDimOff_ :: Dim (ds :: [Nat]) - -> (Int# -> IO ()) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> IO () -overDimOff_ ds stf off0# step# = fst'# $ overDimOff_# ds (\off#-> fst# (stf off#) - ) off0# step# -{-# INLINE overDimOff_ #-} - -fst# :: IO () -> State# RealWorld -> State# RealWorld -fst# (IO f) s = case f s of (# t, _ #) -> t -{-# INLINE fst# #-} - -fst'# :: (State# RealWorld -> State# RealWorld) -> IO () -fst'# f = IO $ \s -> case f s of t -> (# t, () #) - --- | Traverse from the first index to the second index in each dimension. --- Indices must be within Dim range, which is not checked. --- You can combine positive and negative traversal directions along different dimensions. -overDimPart :: forall (ds :: [Nat]) a - . Dimensions ds - => Idx ds -> Idx ds - -> (Idx ds -> Int# -> a -> IO a) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a -> IO a -overDimPart iMin iMax stf off0# step# = IO . overDimPart# iMin iMax (\i off# a -> case stf i off# a of - IO f -> f - ) off0# step# -{-# INLINE overDimPart #-} diff --git a/src/Numeric/Dimensions/Traverse/ST.hs b/src/Numeric/Dimensions/Traverse/ST.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/Traverse/ST.hs +++ /dev/null @@ -1,113 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UnboxedTuples #-} ------------------------------------------------------------------------------ --- | --- Module : Numeric.Dimensions.Traverse.ST --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Maintainer : chirkin@arch.ethz.ch --- --- Map a function over all dimensions provided dimension indices or offsets. --- This module provides a variant of traversal that lives in ST monad. --- ------------------------------------------------------------------------------ - -module Numeric.Dimensions.Traverse.ST - ( overDim, overDim_, overDimIdx, overDimIdx_, overDimOff, overDimOff_, overDimPart - , foldDim, foldDimIdx, foldDimOff - ) where - - -import GHC.Exts -import GHC.ST (ST (..)) - -import Numeric.Dimensions.Dim -import Numeric.Dimensions.Idx -import Numeric.Dimensions.Traverse - - - --- | Traverse over all dimensions keeping track of index and offset -overDim :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> ST s a) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a -> ST s a -overDim ds stf off0# step# = ST . overDim# ds (\i off# a -> case stf i off# a of - ST f -> f - ) off0# step# -{-# INLINE overDim #-} - --- | Traverse over all dimensions keeping track of indices -overDimIdx :: Dim (ds :: [Nat]) - -> (Idx ds -> a -> ST s a) - -> a -> ST s a -overDimIdx ds stf = ST . overDimIdx# ds (\i a -> case stf i a of ST f -> f) -{-# INLINE overDimIdx #-} - --- | Traverse over all dimensions keeping track of total offset -overDimOff :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> a -> ST s a) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a -> ST s a -overDimOff ds stf off0# step# = ST . overDim# ds (\i off# a -> case stf i off# a of - ST f -> f - ) off0# step# -{-# INLINE overDimOff #-} - - - --- | Same as overDim#, but with no return value -overDim_ :: Dim (ds :: [Nat]) - -> (Idx ds -> Int# -> ST s ()) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> ST s () -overDim_ ds stf off0# step# = fst'# $ overDim_# ds (\i off# -> fst# (stf i off#) - ) off0# step# -{-# INLINE overDim_ #-} - --- | Traverse over all dimensions keeping track of indices, with no return value -overDimIdx_ :: Dim (ds :: [Nat]) - -> (Idx ds -> ST s ()) - -> ST s () -overDimIdx_ ds stf = fst'# $ overDimIdx_# ds (\i -> fst# (stf i)) -{-# INLINE overDimIdx_ #-} - - --- | Traverse over all dimensions keeping track of total offset, with not return value -overDimOff_ :: Dim (ds :: [Nat]) - -> (Int# -> ST s ()) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> ST s () -overDimOff_ ds stf off0# step# = fst'# $ overDimOff_# ds (\off#-> fst# (stf off#) - ) off0# step# -{-# INLINE overDimOff_ #-} - -fst# :: ST s () -> State# s -> State# s -fst# (ST f) s = case f s of (# t, _ #) -> t -{-# INLINE fst# #-} - -fst'# :: (State# s -> State# s) -> ST s () -fst'# f = ST $ \s -> case f s of t -> (# t, () #) - --- | Traverse from the first index to the second index in each dimension. --- Indices must be within Dim range, which is not checked. --- You can combine positive and negative traversal directions along different dimensions. -overDimPart :: forall (ds :: [Nat]) a s - . Dimensions ds - => Idx ds -> Idx ds - -> (Idx ds -> Int# -> a -> ST s a) -- ^ function to map over each dimension - -> Int# -- ^ Initial offset - -> Int# -- ^ offset step - -> a -> ST s a -overDimPart iMin iMax stf off0# step# = ST . overDimPart# iMin iMax (\i off# a -> case stf i off# a of - ST f -> f - ) off0# step# -{-# INLINE overDimPart #-} diff --git a/src/Numeric/Dimensions/XDim.hs b/src/Numeric/Dimensions/XDim.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/XDim.hs +++ /dev/null @@ -1,118 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE RoleAnnotations #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeFamilyDependencies #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} ------------------------------------------------------------------------------ --- | --- Module : Numeric.Dimensions.XDim --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Maintainer : chirkin@arch.ethz.ch --- --- Some dimensions in a type-level dimension list may by not known at compile time. --- ------------------------------------------------------------------------------ - -module Numeric.Dimensions.XDim - ( -- * Data types - XDim (..), xdim, xDimVal - -- * Constraints - , XDimensions (..) - ) where - - -import Data.Maybe (isJust) -import Data.Type.Equality ((:~:)(..)) -import GHC.Exts (unsafeCoerce#) - -import Numeric.Dimensions.Dim -import Numeric.TypeLits - - --- | Similar to SomeNat, hide some dimensions under an existential constructor. --- In contrast to SomeDim, it preserves the order of dimensions, --- and it can keep some of the dimensions in the list static --- while making other dimensions known only at runtime. -data XDim (xns :: [XNat]) - = forall ns . ( FixedDim xns ns ~ ns - , FixedXDim xns ns ~ xns - ) => XDim (Dim ns) - - -class XDimensions (xds :: [XNat]) where - wrapDim :: Dim (ds :: [Nat]) -> Maybe (Dim xds) - - -instance XDimensions '[] where - wrapDim D = Just D - wrapDim _ = Nothing - {-# INLINE wrapDim #-} - -instance (XDimensions xs, KnownDim m) => XDimensions (XN m ': xs) where - wrapDim D = Nothing - wrapDim ((d@Dn :: Dim d) :* ds) = - if dimVal d >= dimVal' @m - then case (wrapDim @xs ds, unsafeEqEvidence @(m <=? d) @'True) of - (Just xds, Evidence) -> Just (Dx d :* xds) - (Nothing, _) -> Nothing - else Nothing - -instance (XDimensions xs, KnownDim n) => XDimensions (N n ': xs) where - wrapDim D = Nothing - wrapDim ((Dn :: Dim d) :* ds) = - if dimVal' @d == dimVal' @n - then case (wrapDim @xs ds, unsafeEqEvidence @n @d) of - (Just xds, Evidence) -> Just (Dn @d :* xds) - (Nothing, _) -> Nothing - else Nothing - - --- | Loose compile-time information about dimensionalities -xdim :: forall (ds :: [Nat]) (xds :: [XNat]) - . ( Dimensions ds - , XDimensions xds) => Maybe (Dim xds) -xdim = wrapDim @xds @ds (dim @ds) -{-# INLINE xdim #-} - - - --- | Construct dimensionality at runtime -xDimVal :: Dim (xns :: [XNat]) -> XDim xns -xDimVal D = XDim D -xDimVal ((Dn :: Dim n) :* ds) = case xDimVal ds of - XDim ps -> XDim (Dn @n :* ps) -xDimVal (Dx d :* ds) = case xDimVal ds of - XDim ps -> XDim (d :* ps) - - -instance Show (XDim xns) where - show (XDim p) = 'X' : show p - -instance Eq (XDim xds) where - XDim as == XDim bs = isJust $ sameDim as bs - -instance Ord (XDim xds) where - compare (XDim as) (XDim bs) = compareDim as bs - - -unsafeEqEvidence :: forall x y . Evidence (x ~ y) -unsafeEqEvidence = case (unsafeCoerce# Refl :: x :~: y) of Refl -> Evidence -{-# INLINE unsafeEqEvidence #-} diff --git a/src/Numeric/Tuple.hs b/src/Numeric/Tuple.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Tuple.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +----------------------------------------------------------------------------- +-- | +-- Module : Numeric.Tuple +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- +----------------------------------------------------------------------------- +module Numeric.Tuple + ( module TS + , toStrict, fromStrict + ) where + +import Numeric.Tuple.Strict as TS +import qualified Numeric.Tuple.Lazy as TL +import Unsafe.Coerce (unsafeCoerce) + +toStrict :: TL.Tuple xs -> TS.Tuple xs +toStrict U = U +toStrict (TL.Id x :* xs) + = let !y = x `seq` TS.Id x + !ys = toStrict xs + in y :* ys +#if __GLASGOW_HASKELL__ >= 802 +#else +toStrict _ = error "Tuple.toStrict: impossible argument" +#endif + +fromStrict :: TS.Tuple xs -> TL.Tuple xs +fromStrict = unsafeCoerce +{-# INLINE fromStrict #-} diff --git a/src/Numeric/Tuple/Lazy.hs b/src/Numeric/Tuple/Lazy.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Tuple/Lazy.hs @@ -0,0 +1,320 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE IncoherentInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +----------------------------------------------------------------------------- +-- | +-- Module : Numeric.Tuple.Lazy +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- +----------------------------------------------------------------------------- +module Numeric.Tuple.Lazy + ( Id (..), Tuple + , TypedList (U, (:*), (:$), (:!), Empty, TypeList, Cons, Snoc, Reverse) + , (*$), ($*), (*!), (!*) + ) where + + +import Control.Arrow (first) +import Control.Monad.Fix +import Control.Monad.Zip +import Data.Bits (Bits, FiniteBits) +import Data.Coerce +import Data.Data (Data) +import Data.Foldable +import Data.Ix (Ix) +import Data.Monoid (Monoid (..)) +import Data.Semigroup (Semigroup (..)) +import Data.String (IsString) +import Foreign.Storable (Storable) +import GHC.Base (Type) +import GHC.Exts +import GHC.Generics (Generic, Generic1) +import qualified GHC.Read as Read +import qualified Text.Read as Read + +import Numeric.Type.List +import Numeric.TypedList + +-- | This is an almost complete copy of `Data.Functor.Identity` +-- by (c) Andy Gill 2001. +newtype Id a = Id { runId :: a } + deriving ( Bits, Bounded, Data, Enum, Eq, FiniteBits, Floating, Fractional + , Generic, Generic1, Integral, IsString, Ix, Monoid, Num, Ord + , Real, RealFrac, RealFloat , Semigroup, Storable, Traversable) + + +instance (Read a) => Read (Id a) where + readsPrec d = fmap (first Id) . readsPrec d + +instance (Show a) => Show (Id a) where + showsPrec d = showsPrec d . runId + +instance Foldable Id where + foldMap = coerce + elem = (. runId) #. (==) + foldl = coerce + foldl' = coerce + foldl1 _ = runId + foldr f z (Id x) = f x z + foldr' = foldr + foldr1 _ = runId + length _ = 1 + maximum = runId + minimum = runId + null _ = False + product = runId + sum = runId + toList (Id x) = [x] + +instance Functor Id where + fmap = coerce + +instance Applicative Id where + pure = Id + (<*>) = coerce + +instance Monad Id where + m >>= k = k (runId m) + +instance MonadFix Id where + mfix f = Id (fix (runId . f)) + +instance MonadZip Id where + mzipWith = coerce + munzip = coerce + + + + +-- | A tuple indexed by a list of types +type Tuple (xs :: [Type]) = TypedList Id xs + + +-- Starting from GHC 8.2, compiler supports specifying lists of complete +-- pattern synonyms. +#if __GLASGOW_HASKELL__ >= 802 +{-# COMPLETE U, (:$) #-} +{-# COMPLETE U, (:!) #-} +{-# COMPLETE Empty, (:$) #-} +{-# COMPLETE Empty, (:!) #-} +#endif + + +-- | Constructing a type-indexed list +pattern (:$) :: forall (xs :: [Type]) + . () + => forall (y :: Type) (ys :: [Type]) + . (xs ~ (y ': ys)) => y -> Tuple ys -> Tuple xs +pattern (:$) x xs <- (Id x :* xs) + where + (:$) = (*$) +infixr 5 :$ + +-- | Constructing a type-indexed list +pattern (:!) :: forall (xs :: [Type]) + . () + => forall (y :: Type) (ys :: [Type]) + . (xs ~ (y ': ys)) => y -> Tuple ys -> Tuple xs +pattern (:!) x xs <- (forceCons -> Id x :* xs) + where + (:!) = (*!) +infixr 5 :! + + +-- | Grow a tuple on the left O(1). +(*$) :: x -> Tuple xs -> Tuple (x :+ xs) +(*$) x xs = unsafeCoerce# (unsafeCoerce# x : unsafeCoerce# xs :: [Any]) +{-# INLINE (*$) #-} +infixr 5 *$ + +-- | Grow a tuple on the left while evaluating arguments to WHNF O(1). +(*!) :: x -> Tuple xs -> Tuple (x :+ xs) +(*!) !x !xs = let !r = unsafeCoerce# x : unsafeCoerce# xs :: [Any] + in unsafeCoerce# r +{-# INLINE (*!) #-} +infixr 5 *! + +-- | Grow a tuple on the right. +-- Note, it traverses an element list inside O(n). +($*) :: Tuple xs -> x -> Tuple (xs +: x) +($*) xs x = unsafeCoerce# (unsafeCoerce# xs ++ [unsafeCoerce# x] :: [Any]) +{-# INLINE ($*) #-} +infixl 5 $* + +-- | Grow a tuple on the right while evaluating arguments to WHNF. +-- Note, it traverses an element list inside O(n). +(!*) :: Tuple xs -> x -> Tuple (xs +: x) +(!*) !xs !x = let !r = go (unsafeCoerce# x) (unsafeCoerce# xs) :: [Any] + go :: Any -> [Any] -> [Any] + go z [] = z `seq` [z] + go z (y : ys) = y `seq` y : go z ys + in unsafeCoerce# r +{-# INLINE (!*) #-} +infixl 5 !* + + +instance (All Semigroup xs) => Semigroup (Tuple xs) where + U <> U = U + (x :$ xs) <> (y :$ ys) + = (x <> y) *$ ( xs <> ys) +#if __GLASGOW_HASKELL__ >= 802 +#else + _ <> _ = error "(<>): impossible combination of arguments" +#endif + +instance ( Semigroup (Tuple xs) + , RepresentableList xs + , All Monoid xs) => Monoid (Tuple xs) where + mempty = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Monoid ys => TypeList ys -> Tuple ys + go U = U + go (_ :* xs) = mempty *$ go xs +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ = error "mempty/go: impossible combination of arguments" +#endif + mappend = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Monoid ys + => TypeList ys + -> Tuple ys + -> Tuple ys + -> Tuple ys + go U _ _ = U + go (_ :* ts) (x :$ xs) (y :$ ys) = mappend x y *$ go ts xs ys +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ _ _ = error "mappend/go: impossible combination of arguments" +#endif + + +instance (RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) where + minBound = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Bounded ys => TypeList ys -> Tuple ys + go U = U + go (_ :* xs) = minBound *$ go xs +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ = error "minBound/go: impossible combination of arguments" +#endif + maxBound = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Bounded ys => TypeList ys -> Tuple ys + go U = U + go (_ :* xs) = maxBound *$ go xs +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ = error "maxBound/go: impossible combination of arguments" +#endif + +instance All Eq xs => Eq (Tuple xs) where + (==) U U = True + (==) (x :* tx) (y :* ty) = x == y && tx == ty +#if __GLASGOW_HASKELL__ >= 802 +#else + (==) _ _ = error "(==): impossible combination of arguments" +#endif + (/=) U U = False + (/=) (x :* tx) (y :* ty) = x /= y || tx /= ty +#if __GLASGOW_HASKELL__ >= 802 +#else + (/=) _ _ = error "(/=): impossible combination of arguments" +#endif + +-- | Ord instance of the Tuple implements inverse lexicorgaphic ordering. +-- That is, the last element in the tuple is the most significant one. +-- +-- Note, this will never work on infinite-dimensional tuples! +instance (All Eq xs, All Ord xs) => Ord (Tuple xs) where + compare U U = EQ + compare (x :* tx) (y :* ty) = compare tx ty <> compare x y +#if __GLASGOW_HASKELL__ >= 802 +#else + compare _ _ = error "compare: impossible combination of arguments" +#endif + +instance All Show xs => Show (Tuple xs) where + show U = "U" + show (x :* xs) = show x ++ " :* " ++ show xs +#if __GLASGOW_HASKELL__ >= 802 +#else + show _ = error "show: impossible combination of arguments" +#endif + showsPrec _ U = showString "U" + showsPrec p (x :* xs) = showParen (p >= 5) + $ showsPrec 5 x + . showString " :* " + . showsPrec 5 xs +#if __GLASGOW_HASKELL__ >= 802 +#else + showsPrec _ _ = error "showsPrec: impossible combination of arguments" +#endif + +instance (RepresentableList xs, All Read xs) => Read (Tuple xs) where + readPrec = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Read ys => TypeList ys -> Read.ReadPrec (Tuple ys) + go U = U <$ Read.expectP (Read.Symbol "U") + go (_ :* ts) = Read.parens $ Read.prec 5 $ do + x <- Read.step Read.readPrec + Read.expectP (Read.Symbol ":*") + xs <- Read.step $ go ts + return (x :* xs) +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ = error "readPrec/go: impossible combination of arguments" +#endif + + + +-------------------------------------------------------------------------------- +-- internal +-------------------------------------------------------------------------------- + + +-- | Internal (non-exported) 'Coercible' helper for 'elem' +-- +-- See Note [Function coercion] in "Data.Foldable" for more details. +(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c +(#.) _f = coerce + +forceCons :: Tuple xs -> Tuple xs +forceCons U = U +forceCons (Id x :* xs) = x `seq` xs `seq` (Id x :* xs) +#if __GLASGOW_HASKELL__ >= 802 +#else +forceCons _ = error "forceCons: impossible combination of arguments" +#endif diff --git a/src/Numeric/Tuple/Strict.hs b/src/Numeric/Tuple/Strict.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Tuple/Strict.hs @@ -0,0 +1,320 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE IncoherentInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +----------------------------------------------------------------------------- +-- | +-- Module : Numeric.Tuple.Strict +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- +----------------------------------------------------------------------------- +module Numeric.Tuple.Strict + ( Id (..), Tuple + , TypedList (U, (:*), (:$), (:!), Empty, TypeList, Cons, Snoc, Reverse) + , (*$), ($*), (*!), (!*) + ) where + + +import Control.Arrow (first) +import Control.Monad.Fix +import Control.Monad.Zip +import Data.Bits (Bits, FiniteBits) +import Data.Coerce +import Data.Data (Data) +import Data.Foldable +import Data.Ix (Ix) +import Data.Monoid (Monoid (..)) +import Data.Semigroup (Semigroup (..)) +import Data.String (IsString) +import Foreign.Storable (Storable) +import GHC.Base (Type) +import GHC.Exts +import GHC.Generics (Generic, Generic1) +import qualified GHC.Read as Read +import qualified Text.Read as Read + +import Numeric.Type.List +import Numeric.TypedList + +-- | This is an almost complete copy of `Data.Functor.Identity` +-- by (c) Andy Gill 2001. +newtype Id a = Id { runId :: a } + deriving ( Bits, Bounded, Data, Enum, Eq, FiniteBits, Floating, Fractional + , Generic, Generic1, Integral, IsString, Ix, Monoid, Num, Ord + , Real, RealFrac, RealFloat , Semigroup, Storable, Traversable) + + +instance (Read a) => Read (Id a) where + readsPrec d = fmap (first Id) . readsPrec d + +instance (Show a) => Show (Id a) where + showsPrec d = showsPrec d . runId + +instance Foldable Id where + foldMap = coerce + elem = (. runId) #. (==) + foldl = coerce + foldl' = coerce + foldl1 _ = runId + foldr f z (Id x) = f x z + foldr' = foldr + foldr1 _ = runId + length _ = 1 + maximum = runId + minimum = runId + null _ = False + product = runId + sum = runId + toList (Id x) = [x] + +instance Functor Id where + fmap = coerce + +instance Applicative Id where + pure = Id + (<*>) = coerce + +instance Monad Id where + m >>= k = k (runId m) + +instance MonadFix Id where + mfix f = Id (fix (runId . f)) + +instance MonadZip Id where + mzipWith = coerce + munzip = coerce + + + + +-- | A tuple indexed by a list of types +type Tuple (xs :: [Type]) = TypedList Id xs + + +-- Starting from GHC 8.2, compiler supports specifying lists of complete +-- pattern synonyms. +#if __GLASGOW_HASKELL__ >= 802 +{-# COMPLETE U, (:$) #-} +{-# COMPLETE U, (:!) #-} +{-# COMPLETE Empty, (:$) #-} +{-# COMPLETE Empty, (:!) #-} +#endif + + +-- | Constructing a type-indexed list +pattern (:$) :: forall (xs :: [Type]) + . () + => forall (y :: Type) (ys :: [Type]) + . (xs ~ (y ': ys)) => y -> Tuple ys -> Tuple xs +pattern (:$) x xs <- (Id x :* xs) + where + (:$) = (*$) +infixr 5 :$ + +-- | Constructing a type-indexed list +pattern (:!) :: forall (xs :: [Type]) + . () + => forall (y :: Type) (ys :: [Type]) + . (xs ~ (y ': ys)) => y -> Tuple ys -> Tuple xs +pattern (:!) x xs <- (forceCons -> Id x :* xs) + where + (:!) = (*!) +infixr 5 :! + + +-- | Grow a tuple on the left O(1). +(*$) :: x -> Tuple xs -> Tuple (x :+ xs) +(*$) x xs = unsafeCoerce# (unsafeCoerce# x : unsafeCoerce# xs :: [Any]) +{-# INLINE (*$) #-} +infixr 5 *$ + +-- | Grow a tuple on the left while evaluating arguments to WHNF O(1). +(*!) :: x -> Tuple xs -> Tuple (x :+ xs) +(*!) !x !xs = let !r = unsafeCoerce# x : unsafeCoerce# xs :: [Any] + in unsafeCoerce# r +{-# INLINE (*!) #-} +infixr 5 *! + +-- | Grow a tuple on the right. +-- Note, it traverses an element list inside O(n). +($*) :: Tuple xs -> x -> Tuple (xs +: x) +($*) xs x = unsafeCoerce# (unsafeCoerce# xs ++ [unsafeCoerce# x] :: [Any]) +{-# INLINE ($*) #-} +infixl 5 $* + +-- | Grow a tuple on the right while evaluating arguments to WHNF. +-- Note, it traverses an element list inside O(n). +(!*) :: Tuple xs -> x -> Tuple (xs +: x) +(!*) !xs !x = let !r = go (unsafeCoerce# x) (unsafeCoerce# xs) :: [Any] + go :: Any -> [Any] -> [Any] + go z [] = z `seq` [z] + go z (y : ys) = y `seq` y : go z ys + in unsafeCoerce# r +{-# INLINE (!*) #-} +infixl 5 !* + + +instance (All Semigroup xs) => Semigroup (Tuple xs) where + U <> U = U + (x :! xs) <> (y :! ys) + = (x <> y) *! ( xs <> ys) +#if __GLASGOW_HASKELL__ >= 802 +#else + _ <> _ = error "(<>): impossible combination of arguments" +#endif + +instance ( Semigroup (Tuple xs) + , RepresentableList xs + , All Monoid xs) => Monoid (Tuple xs) where + mempty = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Monoid ys => TypeList ys -> Tuple ys + go U = U + go (_ :* xs) = mempty *! go xs +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ = error "mempty/go: impossible combination of arguments" +#endif + mappend = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Monoid ys + => TypeList ys + -> Tuple ys + -> Tuple ys + -> Tuple ys + go U _ _ = U + go (_ :* ts) (x :! xs) (y :! ys) = mappend x y *! go ts xs ys +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ _ _ = error "mappend/go: impossible combination of arguments" +#endif + + +instance (RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) where + minBound = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Bounded ys => TypeList ys -> Tuple ys + go U = U + go (_ :* xs) = minBound *! go xs +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ = error "minBound/go: impossible combination of arguments" +#endif + maxBound = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Bounded ys => TypeList ys -> Tuple ys + go U = U + go (_ :* xs) = maxBound *! go xs +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ = error "maxBound/go: impossible combination of arguments" +#endif + +instance All Eq xs => Eq (Tuple xs) where + (==) U U = True + (==) (x :* tx) (y :* ty) = x == y && tx == ty +#if __GLASGOW_HASKELL__ >= 802 +#else + (==) _ _ = error "(==): impossible combination of arguments" +#endif + (/=) U U = False + (/=) (x :* tx) (y :* ty) = x /= y || tx /= ty +#if __GLASGOW_HASKELL__ >= 802 +#else + (/=) _ _ = error "(/=): impossible combination of arguments" +#endif + +-- | Ord instance of the Tuple implements inverse lexicorgaphic ordering. +-- That is, the last element in the tuple is the most significant one. +-- +-- Note, this will never work on infinite-dimensional tuples! +instance (All Eq xs, All Ord xs) => Ord (Tuple xs) where + compare U U = EQ + compare (x :* tx) (y :* ty) = compare tx ty <> compare x y +#if __GLASGOW_HASKELL__ >= 802 +#else + compare _ _ = error "compare: impossible combination of arguments" +#endif + +instance All Show xs => Show (Tuple xs) where + show U = "U" + show (x :* xs) = show x ++ " :* " ++ show xs +#if __GLASGOW_HASKELL__ >= 802 +#else + show _ = error "show: impossible combination of arguments" +#endif + showsPrec _ U = showString "U" + showsPrec p (x :* xs) = showParen (p >= 5) + $ showsPrec 5 x + . showString " :* " + . showsPrec 5 xs +#if __GLASGOW_HASKELL__ >= 802 +#else + showsPrec _ _ = error "showsPrec: impossible combination of arguments" +#endif + +instance (RepresentableList xs, All Read xs) => Read (Tuple xs) where + readPrec = go (tList @Type @xs) + where + go :: forall (ys :: [Type]) + . All Read ys => TypeList ys -> Read.ReadPrec (Tuple ys) + go U = U <$ Read.expectP (Read.Symbol "U") + go (_ :* ts) = Read.parens $ Read.prec 5 $ do + x <- Read.step Read.readPrec + Read.expectP (Read.Symbol ":*") + xs <- Read.step $ go ts + return (x :* xs) +#if __GLASGOW_HASKELL__ >= 802 +#else + go _ = error "readPrec/go: impossible combination of arguments" +#endif + + + +-------------------------------------------------------------------------------- +-- internal +-------------------------------------------------------------------------------- + + +-- | Internal (non-exported) 'Coercible' helper for 'elem' +-- +-- See Note [Function coercion] in "Data.Foldable" for more details. +(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c +(#.) _f = coerce + +forceCons :: Tuple xs -> Tuple xs +forceCons U = U +forceCons (Id x :* xs) = x `seq` xs `seq` (Id x :* xs) +#if __GLASGOW_HASKELL__ >= 802 +#else +forceCons _ = error "forceCons: impossible combination of arguments" +#endif diff --git a/src/Numeric/Type/Evidence.hs b/src/Numeric/Type/Evidence.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Type/Evidence.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE PolyKinds #-} +----------------------------------------------------------------------------- +-- | +-- Module : Numeric.Type.Evidence +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- Construct type-level evidence at runtime +-- +----------------------------------------------------------------------------- +module Numeric.Type.Evidence + ( Evidence (..), withEvidence, sumEvs, (+!+) + , Evidence' (..), toEvidence, toEvidence' + ) where + + +import GHC.Base (Type) +import GHC.Exts (Constraint) + + +-- | Bring an instance of certain class or constaint satisfaction evidence into scope. +data Evidence :: Constraint -> Type where + E :: a => Evidence a + +-- | Combine evidence +sumEvs :: Evidence a -> Evidence b -> Evidence (a,b) +sumEvs E E = E +{-# INLINE sumEvs #-} + +infixl 4 +!+ +-- | Combine evidence +(+!+) :: Evidence a -> Evidence b -> Evidence (a,b) +(+!+) = sumEvs +{-# INLINE (+!+) #-} + +-- | Pattern match agains evidence to get constraints info +withEvidence :: Evidence a -> (a => r) -> r +withEvidence d r = case d of E -> r +{-# INLINE withEvidence #-} + +-- | Same as @Evidence@, but allows to separate constraint function from +-- the type it is applied to. +data Evidence' :: (k -> Constraint) -> k -> Type where + E' :: c a => Evidence' c a + +toEvidence :: Evidence' c a -> Evidence (c a) +toEvidence E' = E +{-# INLINE toEvidence #-} + +toEvidence' :: Evidence (c a) -> Evidence' c a +toEvidence' E = E' +{-# INLINE toEvidence' #-} diff --git a/src/Numeric/Type/List.hs b/src/Numeric/Type/List.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Type/List.hs @@ -0,0 +1,222 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +-------------------------------------------------------------------------------- +-- | +-- Module : Numeric.Type.List +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- Provides type-level operations on lists. +-- +-- +-------------------------------------------------------------------------------- + +module Numeric.Type.List + ( -- * Basic operations + type (++), type (+:), type (:+) + , Empty, Cons, Snoc, Head + , Tail, Init, Last, Concat, Reverse, Take, Drop, Length + , All, Map + -- * Working with concatenations + , Suffix, Prefix, IsPrefix, IsSuffix + -- * Term level functions + , ConcatList + ) where + +import GHC.Exts +import GHC.TypeLits + + +-- | Synonym for a type-level cons +-- (injective, since this is just a synonym for the list constructor) +type (a :: k) :+ (as :: [k]) = a ': as +infixr 5 :+ +-- | Prefix-style synonym for cons +type Cons (n :: k) (ns :: [k]) = n :+ ns + +-- | Synonym for a type-level snoc (injective!) +type (ns :: [k]) +: (n :: k) = Snoc ns n +infixl 5 +: +-- | Prefix-style synonym for snoc +type Snoc (ns :: [k]) (n :: k) = GetSnoc k (DoSnoc k ns n) + + +-- | List concatenation +type family (as :: [k]) ++ (bs :: [k]) :: [k] where + (++) '[] bs = bs + (++) as '[] = as + (++) (a :+ as) bs = a :+ (as ++ bs) +infixr 5 ++ + +-- | Prefix-style synonym for concatenation +type Concat (as :: [k]) (bs :: [k]) = as ++ bs + + +-- | Reverse a type-level list (injective!) +type Reverse (xs :: [k]) = Reversed k (DoReverse k xs) + + +-- | Synonym for an empty type-level list +type Empty = '[] + + +type family Take (n::Nat) (xs :: [k]) :: [k] where + Take _ '[] = '[] + Take 0 xs = '[] + Take n (x :+ xs) = x :+ Take (n-1) xs + + +type family Drop (n::Nat) (xs :: [k]) :: [k] where + Drop _ '[] = '[] + Drop 0 xs = xs + Drop n (x :+ xs) = Drop (n-1) xs + +type family Suffix (as :: [k]) (asbs :: [k]) :: [k] where + Suffix '[] bs = bs + Suffix as as = '[] + Suffix (_ :+ as) (_ :+ asbs) = Suffix as asbs + +type family Prefix (bs :: [k]) (asbs :: [k]) :: [k] where + Prefix '[] as = as + Prefix bs bs = '[] + Prefix bs asbs = Take (Length asbs - Length bs) asbs + + +type family IsPrefix (as :: [k]) (asbs :: [k]) :: Bool where + IsPrefix '[] _ = 'True + IsPrefix (a :+ as) (a :+ asbs) = IsPrefix as asbs + IsPrefix as as = 'True + IsPrefix _ _= 'False + +type family IsSuffix (as :: [k]) (asbs :: [k]) :: Bool where + IsSuffix '[] _ = 'True + IsSuffix bs bs = 'True + IsSuffix bs (_ :+ sbs) = IsSuffix bs sbs + IsSuffix _ _ = 'False + + +type family Head (xs :: [k]) :: k where + Head (x :+ xs) = x + Head (KEmpty k) = TypeError ( 'Text + "Head: empty type-level list." + ':$$: FamErrMsg k + ) + +type family Tail (xs :: [k]) :: [k] where + Tail (x :+ xs) = xs + Tail (KEmpty k) = TypeError ( 'Text + "Tail: empty type-level list." + ':$$: FamErrMsg k + ) + +type family Init (xs :: [k]) :: [k] where + Init '[x] = '[] + Init (x :+ xs) = x :+ Init xs + Init (KEmpty k) = TypeError ( 'Text + "Init: empty type-level list." + ':$$: FamErrMsg k + ) + +type family Last (xs :: [k]) :: k where + Last '[x] = x + Last (x :+ xs) = Last xs + Last (KEmpty k) = TypeError ( 'Text + "Last: empty type-level list." + ':$$: FamErrMsg k + ) + +type family Length (xs :: [k]) :: Nat where + Length '[] = 0 + Length (_ ': xs) = 1 + Length xs + + +type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where + All _ '[] = () + All f (x ': xs) = (f x, All f xs) + +type family Map (f :: a -> b) (xs :: [a]) :: [b] where + Map f '[] = '[] + Map f (x ': xs) = f x ': Map f xs + + +-- | Represent a triple of lists forming a relation `as ++ bs ~ asbs` +class ( asbs ~ Concat as bs + , as ~ Prefix bs asbs + , bs ~ Suffix as asbs + , IsSuffix bs asbs ~ 'True + , IsPrefix as asbs ~ 'True + ) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) + | as bs -> asbs + , as asbs -> bs + , bs asbs -> as + +instance ( asbs ~ Concat as bs + , as ~ Prefix bs asbs + , bs ~ Suffix as asbs + , IsSuffix bs asbs ~ 'True + , IsPrefix as asbs ~ 'True + ) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) + + + +type FamErrMsg k + = 'Text "Type-level error occured when operating on a list of kind " + ':<>: 'ShowType [k] ':<>: 'Text "." + +-------------------------------------------------------------------------------- +---- Tricks to make some type-level operations injective +-------------------------------------------------------------------------------- + + + +-- | A special data type that can have either a single element, +-- or more than two. +-- This feature is not enforced in the type system - this is just a way to make injective Snoc. +data Snocing k = SSingle k | SCons [k] +type SSingle k x = 'SSingle (x :: k) +type SCons k xs = 'SCons (xs :: [k]) +type KCons k x xs = (x :: k) ': (xs :: [k]) +type KEmpty k = ('[] :: [k]) +type KSingle k x = ('[x] :: [k]) + +type family DoSnoc k (xs :: [k]) (z::k) = (ys :: Snocing k) | ys -> xs z where + DoSnoc k '[] x = SSingle k x + DoSnoc k (KCons k x xs) y = + (SCons k (KCons k x (GetSnoc k (DoSnoc k xs y)) :: [k]) :: Snocing k) + + +type family GetSnoc k (xs :: Snocing k) = (ys :: [k]) | ys -> xs where + GetSnoc k (SSingle k x) = KSingle k x + GetSnoc k (SCons k (KCons k y (KCons k x xs))) = + KCons k y (KCons k x xs) + +-- | Another data type to make Reverse injective. +data Reversing k = REmpty | RReverse [k] +type REmpty k = 'REmpty +type RReverse k xs = 'RReverse (xs :: [k]) + + + +type family Reversed k (ts :: Reversing k) = (rs :: [k]) | rs -> ts where + Reversed k (REmpty k) = KEmpty k + Reversed k (RReverse k (KCons k x xs)) = KCons k x xs + + +type family DoReverse k (as :: [k]) = (rs :: Reversing k) | rs -> as where + DoReverse k '[] = REmpty k + DoReverse k (KCons k a as) = + RReverse k (GetSnoc k (DoSnoc k (Reversed k (DoReverse k as)) a)) diff --git a/src/Numeric/TypeLits.hs b/src/Numeric/TypeLits.hs deleted file mode 100644 --- a/src/Numeric/TypeLits.hs +++ /dev/null @@ -1,192 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE RoleAnnotations #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} ------------------------------------------------------------------------------ --- | --- Module : Numeric.TypeLits --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Maintainer : chirkin@arch.ethz.ch --- --- This modules is based on `GHC.TypeLits` and re-exports its functionality. --- It provides `KnownDim` class that is similar to `KnownNat`, but keeps --- `Int`s instead of `Integer`s. --- A set of utility functions provide inference functionality, so --- that `KnownDim` can be preserved over some type-level operations. --- ------------------------------------------------------------------------------ - -module Numeric.TypeLits - ( XNat (..), XN, N - -- * Nats backed by Int - , SomeIntNat (..), someIntNatVal, intNatVal, reifyDim - , KnownDim (..), KnownDims, dimVal#, Proxy#, proxy# - -- * Dynamically constructing evidence - , Evidence (..), withEvidence, sumEvs, (+!+) - , inferPlusKnownDim, inferMinusKnownDim, inferMinusKnownDimM - , inferTimesKnownDim - -- * Re-export original GHC TypeLits - , module GHC.TypeLits - , Proxy (..) - ) where - - -import Data.Proxy (Proxy(..)) -import GHC.Exts (Constraint, Proxy#, proxy#) -import GHC.TypeLits -import GHC.Types (Type) -import Unsafe.Coerce (unsafeCoerce) - - - --- | Either known or unknown at compile-time natural number -data XNat = XN Nat | N Nat --- | Unknown natural number, known to be not smaller than the given Nat -type XN (n::Nat) = 'XN n --- | Known natural number -type N (n::Nat) = 'N n - - - --- | Same as SomeNat, but for Dimensions: --- Hide all information about Dimensions inside -data SomeIntNat = forall (n :: Nat) . KnownDim n => SomeIntNat (Proxy n) - - - --- | This class gives the int associated with a type-level natural. --- Valid known dim must be not less than 0. -class KnownDim (n :: Nat) where - -- | Get value of type-level dim at runtime - dimVal' :: Int - --- | A constraint family that makes sure all subdimensions are known. -type family KnownDims (ns :: [Nat]) :: Constraint where - KnownDims '[] = () - KnownDims (x ': xs) = ( KnownDim x, KnownDims xs ) - --- | A variant of `dimVal'` that gets `Proxy#` as an argument. -dimVal# :: forall (n :: Nat) . KnownDim n => Proxy# n -> Int -dimVal# _ = dimVal' @n -{-# INLINE dimVal# #-} - --- | Similar to `natVal` from `GHC.TypeLits`, but returns `Int`. -intNatVal :: forall n proxy . KnownDim n => proxy n -> Int -intNatVal _ = dimVal' @n - -instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where - {-# INLINE dimVal' #-} - dimVal' = fromInteger (natVal' (proxy# :: Proxy# n)) - -instance {-# OVERLAPPING #-} KnownDim 0 where { {-# INLINE dimVal' #-}; dimVal' = 0 } -instance {-# OVERLAPPING #-} KnownDim 1 where { {-# INLINE dimVal' #-}; dimVal' = 1 } -instance {-# OVERLAPPING #-} KnownDim 2 where { {-# INLINE dimVal' #-}; dimVal' = 2 } -instance {-# OVERLAPPING #-} KnownDim 3 where { {-# INLINE dimVal' #-}; dimVal' = 3 } -instance {-# OVERLAPPING #-} KnownDim 4 where { {-# INLINE dimVal' #-}; dimVal' = 4 } -instance {-# OVERLAPPING #-} KnownDim 5 where { {-# INLINE dimVal' #-}; dimVal' = 5 } -instance {-# OVERLAPPING #-} KnownDim 6 where { {-# INLINE dimVal' #-}; dimVal' = 6 } -instance {-# OVERLAPPING #-} KnownDim 7 where { {-# INLINE dimVal' #-}; dimVal' = 7 } -instance {-# OVERLAPPING #-} KnownDim 8 where { {-# INLINE dimVal' #-}; dimVal' = 8 } -instance {-# OVERLAPPING #-} KnownDim 9 where { {-# INLINE dimVal' #-}; dimVal' = 9 } -instance {-# OVERLAPPING #-} KnownDim 10 where { {-# INLINE dimVal' #-}; dimVal' = 10 } -instance {-# OVERLAPPING #-} KnownDim 11 where { {-# INLINE dimVal' #-}; dimVal' = 11 } -instance {-# OVERLAPPING #-} KnownDim 12 where { {-# INLINE dimVal' #-}; dimVal' = 12 } -instance {-# OVERLAPPING #-} KnownDim 13 where { {-# INLINE dimVal' #-}; dimVal' = 13 } -instance {-# OVERLAPPING #-} KnownDim 14 where { {-# INLINE dimVal' #-}; dimVal' = 14 } -instance {-# OVERLAPPING #-} KnownDim 15 where { {-# INLINE dimVal' #-}; dimVal' = 15 } -instance {-# OVERLAPPING #-} KnownDim 16 where { {-# INLINE dimVal' #-}; dimVal' = 16 } -instance {-# OVERLAPPING #-} KnownDim 17 where { {-# INLINE dimVal' #-}; dimVal' = 17 } -instance {-# OVERLAPPING #-} KnownDim 18 where { {-# INLINE dimVal' #-}; dimVal' = 18 } -instance {-# OVERLAPPING #-} KnownDim 19 where { {-# INLINE dimVal' #-}; dimVal' = 19 } -instance {-# OVERLAPPING #-} KnownDim 20 where { {-# INLINE dimVal' #-}; dimVal' = 20 } - - --- | Similar to `someNatVal`, but for a single dimension -someIntNatVal :: Int -> Maybe SomeIntNat -someIntNatVal x | 0 > x = Nothing - | otherwise = Just (reifyDim x f) - where - f :: forall (n :: Nat) . KnownDim n => Proxy# n -> SomeIntNat - f _ = SomeIntNat (Proxy @n) -{-# INLINE someIntNatVal #-} - - --- | This function does GHC's magic to convert user-supplied `dimVal'` function --- to create an instance of KnownDim typeclass at runtime. --- The trick is taken from Edward Kmett's reflection library explained --- in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection -reifyDim :: forall r . Int -> (forall (n :: Nat) . KnownDim n => Proxy# n -> r) -> r -reifyDim n k = unsafeCoerce (MagicDim k :: MagicDim r) n proxy# -{-# INLINE reifyDim #-} -newtype MagicDim r = MagicDim (forall (n :: Nat) . KnownDim n => Proxy# n -> r) - - -instance Eq SomeIntNat where - SomeIntNat x == SomeIntNat y = intNatVal x == intNatVal y - -instance Ord SomeIntNat where - compare (SomeIntNat x) (SomeIntNat y) = compare (intNatVal x) (intNatVal y) - -instance Show SomeIntNat where - showsPrec p (SomeIntNat x) = showsPrec p (intNatVal x) - -instance Read SomeIntNat where - readsPrec p xs = do (a,ys) <- readsPrec p xs - case someIntNatVal a of - Nothing -> [] - Just n -> [(n,ys)] - - --- | Bring an instance of certain class or constaint satisfaction evidence into scope. -data Evidence :: Constraint -> Type where - Evidence :: a => Evidence a - -sumEvs :: Evidence a -> Evidence b -> Evidence (a,b) -sumEvs Evidence Evidence = Evidence -{-# INLINE sumEvs #-} - -infixl 4 +!+ -(+!+) :: Evidence a -> Evidence b -> Evidence (a,b) -(+!+) = sumEvs -{-# INLINE (+!+) #-} - - -withEvidence :: Evidence a -> (a => r) -> r -withEvidence d r = case d of Evidence -> r -{-# INLINE withEvidence #-} - -mkKDEv :: forall (m :: Nat) (n :: Nat) . KnownDim n => Proxy# n -> Evidence (KnownDim m) -mkKDEv _ = unsafeCoerce $ Evidence @(KnownDim n) -{-# INLINE mkKDEv #-} - -inferPlusKnownDim :: forall n m . (KnownDim n, KnownDim m) => Evidence (KnownDim (n + m)) -inferPlusKnownDim = reifyDim (dimVal' @n + dimVal' @m) (mkKDEv @(n + m)) -{-# INLINE inferPlusKnownDim #-} - -inferMinusKnownDim :: forall n m . (KnownDim n, KnownDim m, m <= n) => Evidence (KnownDim (n - m)) -inferMinusKnownDim = reifyDim (dimVal' @n - dimVal' @m) (mkKDEv @(n - m)) -{-# INLINE inferMinusKnownDim #-} - -inferMinusKnownDimM :: forall n m . (KnownDim n, KnownDim m) => Maybe (Evidence (KnownDim (n - m))) -inferMinusKnownDimM = if v >= 0 then Just $ reifyDim v (mkKDEv @(n - m)) - else Nothing - where - v = dimVal' @n - dimVal' @m -{-# INLINE inferMinusKnownDimM #-} - -inferTimesKnownDim :: forall n m . (KnownDim n, KnownDim m) => Evidence (KnownDim (n * m)) -inferTimesKnownDim = reifyDim (dimVal' @n * dimVal' @m) (mkKDEv @(n * m)) -{-# INLINE inferTimesKnownDim #-} diff --git a/src/Numeric/TypedList.hs b/src/Numeric/TypedList.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/TypedList.hs @@ -0,0 +1,343 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +----------------------------------------------------------------------------- +-- | +-- Module : Numeric.TypedList +-- Copyright : (c) Artem Chirkin +-- License : BSD3 +-- +-- Maintainer : chirkin@arch.ethz.ch +-- +-- +-- Provide a type-indexed heterogeneous list type @TypedList@. +-- Behind the facade, @TypedList@ is just a plain list of haskell pointers. +-- It is used to represent dimension lists, indices, and just flexible tuples. +-- +-- Most of type-level functionality is implemented using GADT-like pattern synonyms. +-- Import this module qualified to use list-like functionality. +-- +----------------------------------------------------------------------------- +module Numeric.TypedList + ( TypedList (U, (:*), Empty, TypeList, EvList, Cons, Snoc, Reverse) + , RepresentableList (..) + , TypeList, types, order, order' + , cons, snoc + , Numeric.TypedList.reverse + , Numeric.TypedList.take + , Numeric.TypedList.drop + , Numeric.TypedList.head + , Numeric.TypedList.tail + , Numeric.TypedList.last + , Numeric.TypedList.init + , Numeric.TypedList.splitAt + , Numeric.TypedList.concat + , Numeric.TypedList.length + , Numeric.TypedList.map + , module Numeric.Type.List + ) where + +import Control.Arrow (first) +import Data.Proxy +import GHC.Base (Type) +import GHC.Exts + +import Numeric.Dim +import Numeric.Type.Evidence +import Numeric.Type.List + + +-- | Type-indexed list +newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any] + + +-- Starting from GHC 8.2, compiler supports specifying lists of complete +-- pattern synonyms. +#if __GLASGOW_HASKELL__ >= 802 +{-# COMPLETE TypeList #-} +{-# COMPLETE EvList #-} +{-# COMPLETE U, (:*) #-} +{-# COMPLETE U, Cons #-} +{-# COMPLETE U, Snoc #-} +{-# COMPLETE Empty, (:*) #-} +{-# COMPLETE Empty, Cons #-} +{-# COMPLETE Empty, Snoc #-} +{-# COMPLETE Reverse #-} +#endif + +-- | A list of type proxies +type TypeList (xs :: [k]) = TypedList Proxy xs + + +-- | A list of evidence for constraints +type EvidenceList (c :: k -> Constraint) (xs :: [k]) + = TypedList (Evidence' c) xs + + +-- | Pattern matching against this causes `RepresentableList` instance +-- come into scope. +-- Also it allows constructing a term-level list out of a constraint. +pattern TypeList :: forall (xs :: [k]) + . () => RepresentableList xs => TypeList xs +pattern TypeList <- (mkRTL -> E) + where + TypeList = tList @k @xs + +-- | Pattern matching against this allows manipulating lists of constraints. +-- Useful when creating functions that change the shape of dimensions. +pattern EvList :: forall (c :: k -> Constraint) (xs :: [k]) + . () => (All c xs, RepresentableList xs) => EvidenceList c xs +pattern EvList <- (mkEVL -> E) + where + EvList = _evList (tList @k @xs) + +-- | Zero-length type list +pattern U :: forall (f :: k -> Type) (xs :: [k]) + . () => (xs ~ '[]) => TypedList f xs +pattern U <- (patTL @f @xs -> PatCNil) + where + U = unsafeCoerce# [] + +-- | Zero-length type list; synonym to `U`. +pattern Empty :: forall (f :: k -> Type) (xs :: [k]) + . () => (xs ~ '[]) => TypedList f xs +pattern Empty = U + +-- | Constructing a type-indexed list +pattern (:*) :: forall (f :: k -> Type) (xs :: [k]) + . () + => forall (y :: k) (ys :: [k]) + . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs +pattern (:*) x xs = Cons x xs +infixr 5 :* + +-- | Constructing a type-indexed list in the canonical way +pattern Cons :: forall (f :: k -> Type) (xs :: [k]) + . () + => forall (y :: k) (ys :: [k]) + . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs +pattern Cons x xs <- (patTL @f @xs -> PatCons x xs) + where + Cons = Numeric.TypedList.cons + +-- | Constructing a type-indexed list from the other end +pattern Snoc :: forall (f :: k -> Type) (xs :: [k]) + . () + => forall (sy :: [k]) (y :: k) + . (xs ~ (sy +: y)) => TypedList f sy -> f y -> TypedList f xs +pattern Snoc sx x <- (unsnocTL @f @xs -> PatSnoc sx x) + where + Snoc = Numeric.TypedList.snoc + +-- | Reverse a typed list +pattern Reverse :: forall (f :: k -> Type) (xs :: [k]) + . () + => forall (sx :: [k]) + . (xs ~ Reverse sx, sx ~ Reverse xs) + => TypedList f sx -> TypedList f xs +pattern Reverse sx <- (unreverseTL @f @xs -> PatReverse sx) + where + Reverse = Numeric.TypedList.reverse + +cons :: f x -> TypedList f xs -> TypedList f (x :+ xs) +cons x xs = TypedList (unsafeCoerce# x : unsafeCoerce# xs) +{-# INLINE cons #-} + +snoc :: TypedList f xs -> f x -> TypedList f (xs +: x) +snoc xs x = TypedList (unsafeCoerce# xs ++ [unsafeCoerce# x]) +{-# INLINE snoc #-} + +reverse :: TypedList f xs -> TypedList f (Reverse xs) +reverse (TypedList sx) = unsafeCoerce# (Prelude.reverse sx) +{-# INLINE reverse #-} + +take :: Dim n -> TypedList f xs -> TypedList f (Take n xs) +take d (TypedList xs) = unsafeCoerce# (Prelude.take (intD d) xs) +{-# INLINE take #-} + +drop :: Dim n -> TypedList f xs -> TypedList f (Drop n xs) +drop d (TypedList xs) = unsafeCoerce# (Prelude.drop (intD d) xs) +{-# INLINE drop #-} + +head :: TypedList f xs -> f (Head xs) +head (TypedList xs) = unsafeCoerce# (Prelude.head xs) +{-# INLINE head #-} + +tail :: TypedList f xs -> TypedList f (Tail xs) +tail (TypedList xs) = unsafeCoerce# (Prelude.tail xs) +{-# INLINE tail #-} + +init :: TypedList f xs -> TypedList f (Init xs) +init (TypedList xs) = unsafeCoerce# (Prelude.init xs) +{-# INLINE init #-} + +last :: TypedList f xs -> f (Last xs) +last (TypedList xs) = unsafeCoerce# (Prelude.last xs) +{-# INLINE last #-} + +length :: TypedList f xs -> Dim (Length xs) +length = order +{-# INLINE length #-} + +splitAt :: Dim n + -> TypedList f xs + -> (TypedList f (Take n xs), TypedList f (Drop n xs)) +splitAt d (TypedList xs) = unsafeCoerce# (Prelude.splitAt (intD d) xs) +{-# INLINE splitAt #-} + +concat :: TypedList f xs + -> TypedList f ys + -> TypedList f (xs ++ ys) +concat (TypedList xs) (TypedList ys) = unsafeCoerce# (xs ++ ys) +{-# INLINE concat #-} + +-- | Map a function over contents of a typed list +map :: (forall a . f a -> g a) + -> TypedList f xs + -> TypedList g xs +map k (TypedList xs) = unsafeCoerce# (Prelude.map k' xs) + where + k' :: Any -> Any + k' = unsafeCoerce# . k . unsafeCoerce# +{-# INLINE map #-} + +-- | Get a constructible `TypeList` from any other `TypedList`; +-- Pattern matching agains the result brings `RepresentableList` constraint +-- into the scope: +-- +-- > case types ts of TypeList -> ... +-- +types :: TypedList f xs -> TypeList xs +types (TypedList xs) = unsafeCoerce# (Prelude.map (const Proxy) xs) +{-# INLINE types #-} + +-- | Representable type lists. +-- Allows getting type information about list structure at runtime. +class RepresentableList (xs :: [k]) where + -- | Get type-level constructed list + tList :: TypeList xs + +instance RepresentableList ('[] :: [k]) where + tList = U + +instance RepresentableList xs => RepresentableList (x ': xs :: [k]) where + tList = Proxy @x :* tList @k @xs + + +order' :: forall xs . RepresentableList xs => Dim (Length xs) +order' = order (tList @_ @xs) +{-# INLINE order' #-} + +order :: TypedList f xs -> Dim (Length xs) +order (TypedList xs) = unsafeCoerce# (fromIntegral (Prelude.length xs) :: Word) +{-# INLINE order #-} + + + + +-------------------------------------------------------------------------------- +-- internal +-------------------------------------------------------------------------------- + + +-- | This function does GHC's magic to convert user-supplied `tList` function +-- to create an instance of `RepresentableList` typeclass at runtime. +-- The trick is taken from Edward Kmett's reflection library explained +-- in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection +reifyRepList :: forall xs r + . TypeList xs + -> (RepresentableList xs => r) + -> r +reifyRepList tl k = unsafeCoerce# (MagicRepList k :: MagicRepList xs r) tl +{-# INLINE reifyRepList #-} +newtype MagicRepList xs r = MagicRepList (RepresentableList xs => r) + +data PatReverse f xs + = forall (sx :: [k]) . (xs ~ Reverse sx, sx ~ Reverse xs) + => PatReverse (TypedList f sx) + +unreverseTL :: forall f xs . TypedList f xs -> PatReverse f xs +unreverseTL (TypedList xs) + = case (unsafeCoerce# (E @(xs ~ xs, xs ~ xs)) + :: Evidence (xs ~ Reverse sx, sx ~ Reverse xs) + ) of + E -> PatReverse (unsafeCoerce# (Prelude.reverse xs)) +{-# INLINE unreverseTL #-} + + +mkRTL :: forall (xs :: [k]) + . TypeList xs + -> Evidence (RepresentableList xs) +mkRTL xs = reifyRepList xs E +{-# INLINE mkRTL #-} + + +data PatSnoc f xs where + PatSNil :: PatSnoc f '[] + PatSnoc :: TypedList f ys -> f y -> PatSnoc f (ys +: y) + +unsnocTL :: forall f xs . TypedList f xs -> PatSnoc f xs +unsnocTL (TypedList []) + = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ '[])) of + E -> PatSNil +unsnocTL (TypedList (x:xs)) + = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ (Init xs +: Last xs))) of + E -> PatSnoc (unsafeCoerce# sy) (unsafeCoerce# y) + where + (sy, y) = unsnoc x xs + unsnoc t [] = ([], t) + unsnoc t (z:zs) = first (t:) (unsnoc z zs) +{-# INLINE unsnocTL #-} + + +data PatCons f xs where + PatCNil :: PatCons f '[] + PatCons :: f y -> TypedList f ys -> PatCons f (y ': ys) + +patTL :: forall f xs . TypedList f xs -> PatCons f xs +patTL (TypedList []) + = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ '[])) of + E -> PatCNil +patTL (TypedList (x : xs)) + = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ (Head xs ': Tail xs))) of + E -> PatCons (unsafeCoerce# x) (unsafeCoerce# xs) +{-# INLINE patTL #-} + +intD :: Dim n -> Int +intD = (fromIntegral :: Word -> Int) . unsafeCoerce# + + +mkEVL :: forall (c :: k -> Constraint) (xs :: [k]) + . EvidenceList c xs -> Evidence (All c xs, RepresentableList xs) +mkEVL U = E +mkEVL (E' :* evs) = case mkEVL evs of E -> E +#if __GLASGOW_HASKELL__ >= 802 +#else +mkEVL _ = error "EvList/mkEVL: impossible argument" +#endif + + +_evList :: forall (c :: k -> Constraint) (xs :: [k]) + . All c xs => TypeList xs -> EvidenceList c xs +_evList U = U +_evList (_ :* xs) = case _evList xs of evs -> E' :* evs +#if __GLASGOW_HASKELL__ >= 802 +#else +_evList _ = error "EvList/_evList: impossible argument" +#endif diff --git a/test/Numeric/DimTest.hs b/test/Numeric/DimTest.hs new file mode 100644 --- /dev/null +++ b/test/Numeric/DimTest.hs @@ -0,0 +1,86 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +-- | Some GHC versions show incorrect warnings here: +-- +-- GHC 8.2 says "Pattern match has inaccessible right hand side" +-- if our GADT-like patterns are matched nested: +-- https://ghc.haskell.org/trac/ghc/ticket/14253 +-- +-- GHC 8.0 says "Pattern match(es) are non-exhaustive" +-- because it does not support COMPLETE pragmas yet. +-- +module Numeric.DimTest (runTests) where + +import Test.QuickCheck (quickCheckAll) + +import Numeric.Dim +import Numeric.Type.Evidence + + +-- | Try inference of type-level natural values via term-level binary functions. +testBinaryOp :: forall (a :: Nat) (b :: Nat) (c :: Nat) + . (Word -> Word -> Word) + -> (Dim a -> Dim b -> Dim c) + -> Dim a -> Dim b -> Bool +testBinaryOp fTerm fType da db + | a <- dimVal da + , b <- dimVal db + , Dx dr <- someDimVal (fTerm a b) + -- pattern-match against @SomeDim@ to extract a type-level natural Dim. + , True <- fTerm a b == dimVal (fType da db) + -- compare the term-level function and the type-level function results + -- as regular word values. + , Just E <- sameDim dr (fType da db) + -- now the type system knows that @c ~ fType a b@ and + -- we can use ordinary equality function (which is @const True@). + = dr == fType da db +testBinaryOp _ _ _ _ = False + + + +prop_plusDim :: Word -> Word -> Bool +prop_plusDim a b = case (someDimVal a, someDimVal b) of + (Dx da, Dx db) -> testBinaryOp (+) plusDim da db + + +prop_timesDim :: Word -> Word -> Bool +prop_timesDim a b = case (someDimVal a, someDimVal b) of + (Dx da, Dx db) -> testBinaryOp (*) timesDim da db + + +prop_powerDim :: Word -> Word -> Bool +prop_powerDim a b = case ( someDimVal a + , someDimVal b + ) of + (Dx da, Dx db) -> testBinaryOp (^) powerDim da db + +prop_minusDim :: Word -> Word -> Bool +prop_minusDim a' b' + | a <- max a' b' + , b <- min a' b' + , xda <- someDimVal a -- this is an unknown (Dim (XN 0)) + , Dx db <- someDimVal b + , Just (Dx da) <- constrainBy db xda -- here da >= db + = a - b == dimVal (minusDim da db) +prop_minusDim _ _ = False + + + + + + +return [] +runTests :: IO Bool +runTests = $quickCheckAll diff --git a/test/Numeric/Dimensions/DimsTest.hs b/test/Numeric/Dimensions/DimsTest.hs new file mode 100644 --- /dev/null +++ b/test/Numeric/Dimensions/DimsTest.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + + + +module Numeric.Dimensions.DimsTest (runTests) where + +import Test.QuickCheck (quickCheckAll) + +import Numeric.Dim +import Numeric.Dimensions.Dims +import qualified Numeric.TypedList as TL + + +-- | Matching against @Reverse@ pattern lets GHC know the reversion relation +-- at the type level. +-- That means the type system knows that reverse of reverse is the same list! +prop_reverseDims :: [Word] -> Bool +prop_reverseDims xs + | SomeDims ds <- someDimsVal xs + = case ds of + Reverse rds -> case rds of + Reverse rrds -> ds == rrds + + +prop_concatDims :: [Word] -> [Word] -> Bool +prop_concatDims xs ys + | SomeDims dxs <- someDimsVal xs + , SomeDims dys <- someDimsVal ys + = case TL.concat dxs dys of + dxsys -> listDims dxsys == xs ++ ys + + +-- | TODO: bring more evidence about list equality +prop_splitDims :: Word -> [Word] -> Bool +prop_splitDims n xsys + | SomeDims dxsys <- someDimsVal xsys + , Dx dn <- someDimVal n -- TODO: why this causes non-exhaustive patterns in GHC 8.2? + , (xs, ys) <- splitAt (fromIntegral n) xsys + = case TL.splitAt dn dxsys of + (dxs, dys) -> and + [ listDims dxs == xs + , listDims dys == ys + -- , dxsys == TL.concat dxs dys + ] + + + + + + + + +return [] +runTests :: IO Bool +runTests = $quickCheckAll diff --git a/test/Numeric/Dimensions/ListTest.hs b/test/Numeric/Dimensions/ListTest.hs deleted file mode 100644 --- a/test/Numeric/Dimensions/ListTest.hs +++ /dev/null @@ -1,124 +0,0 @@ -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE MagicHash #-} ------------------------------------------------------------------------------ --- | --- Module : Numeric.Dimensions.ListTest --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Maintainer : chirkin@arch.ethz.ch --- --- Testing type-level Lists and the inference plugin --- ------------------------------------------------------------------------------ - - -module Numeric.Dimensions.ListTest (runTests) where - -import Test.QuickCheck (quickCheckAll) - -import Numeric.TypeLits -import Numeric.Dimensions - --- * Test simple binary nat ops - -natSum :: Dim a -> Dim b -> Proxy (a+b) -natSum _ _ = Proxy -natMul :: Dim a -> Dim b -> Proxy (a*b) -natMul _ _ = Proxy -natRem :: Dim a -> Dim b -> Proxy (a-b) -natRem _ _ = Proxy -natSucc :: Dim a -> Proxy (a + 1) -natSucc _ = Proxy -natPred :: Dim a -> Proxy (a - 1) -natPred _ = Proxy - -prop_KnownNats :: Int -> Int -> Bool -prop_KnownNats a b - | x <- max (abs a) (abs b) - , y <- min (abs a) (abs b) - , z <- y `mod` 50 - , Just (SomeDim (px@Dn :: Dim x)) <- someDimVal x - , Just (SomeDim (py@Dn :: Dim y)) <- someDimVal y - , Just (SomeDim (px1@Dn :: Dim x1)) <- someDimVal (x+1) - , Just (SomeDim (Dn :: Dim z)) <- someDimVal z - , Just Evidence <- (\e1 e2 e3 -> e1 `sumEvs` e2 `sumEvs` e3) - <$> inferMinusKnownDimM @x @y - <*> inferMinusKnownDimM @x1 @1 - <*> Just ( inferPlusKnownDim @x @y - `sumEvs` inferTimesKnownDim @x @y - `sumEvs` inferPlusKnownDim @y @1 - ) - = and - [ x + y == intNatVal (natSum px py) - , x * y == intNatVal (natMul px py) - , x - y == intNatVal (natRem px py) - , x == intNatVal (natPred px1) - , y + 1 == intNatVal (natSucc py) - ] -prop_KnownNats _ _ = True - - - --- * Test props on a single type-level list - -prop_FiniteList :: Int -> [Int] -> Bool -prop_FiniteList a xs' - | n <- (abs a) - , xs <- (2+) . abs <$> xs' - , Just (SomeDim (Dn :: Dim n)) <- someDimVal n - , Just (SomeDims (pxs :: Dim xs)) <- someDimsVal xs - , Evidence <- reifyDimensions pxs - , Evidence <- inferDimFiniteList @xs - = and [ order @_ @xs == length xs - , case inferTakeNFiniteList @n @xs of - Evidence -> order @_ @(Take n xs) == length (take n xs) - , case inferDropNFiniteList @n @xs of - Evidence -> order @_ @(Drop n xs) == length (drop n xs) - , case inferReverseFiniteList @xs of - Evidence -> order @_ @(Reverse xs) == length (reverse xs) - ] -prop_FiniteList _ _ = False - - - - --- * Inference properties - -prop_ListInference :: [Int] -> [Int] -> Bool -prop_ListInference xs' ys' - | xs <- (2+) . abs <$> xs' - , ys <- (2+) . abs <$> ys' - , Just (SomeDims (dxs :: Dim xs)) <- someDimsVal xs - , Just (SomeDims (dys :: Dim ys)) <- someDimsVal ys - , Evidence <- reifyDimensions dxs - , Evidence <- reifyDimensions dys - , Evidence <- inferDimFiniteList @xs - `sumEvs` inferDimFiniteList @ys - = and [ case inferConcatFiniteList @xs @ys of - Evidence -> order @_ @(xs ++ ys) == length xs + length ys - , case inferConcat @xs @ys `sumEvs` - inferConcatFiniteList @xs @ys of - Evidence -> case inferPrefixFiniteList @ys @(xs ++ ys) of - Evidence -> order @_ @(Prefix ys (xs ++ ys)) == length xs - , case inferConcat @xs @ys `sumEvs` - inferConcatFiniteList @xs @ys of - Evidence -> case inferSuffixFiniteList @xs @(xs ++ ys) of - Evidence -> order @_ @(Suffix xs (xs ++ ys)) == length ys - ] -prop_ListInference _ _ = False - -return [] -runTests :: IO Bool -runTests = $quickCheckAll diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -3,13 +3,15 @@ import System.Exit import Distribution.TestSuite -import qualified Numeric.Dimensions.ListTest +import qualified Numeric.DimTest +import qualified Numeric.Dimensions.DimsTest -- | Collection of tests in detailed-0.9 format tests :: IO [Test] tests = return - [ test "Dimensions.List" Numeric.Dimensions.ListTest.runTests + [ test "Dim" Numeric.DimTest.runTests + , test "Dims" Numeric.Dimensions.DimsTest.runTests ]