diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,32 @@ +{- +Disable some errors and warnings during the haddock pass + (caused by compiler plugins and hs-boot) + -} +{-# OPTIONS_GHC -Wall #-} +module Main (main) where + import Distribution.Simple -main = defaultMain +import Distribution.Simple.Setup + +main :: IO () +main = defaultMainWithHooks simpleUserHooks + { confHook = \a -> confHook simpleUserHooks a . tweakFlags } + +tweakFlags :: ConfigFlags -> ConfigFlags +tweakFlags flags = flags + { configProgramArgs = addHaddockArgs (configProgramArgs flags) } + +addHaddockArgs :: [(String, [String])] -> [(String, [String])] +addHaddockArgs [] + = [("haddock", newHaddockGhcArgs)] +addHaddockArgs (("haddock", args):otherProgsArgs) + = ("haddock", args ++ newHaddockGhcArgs) : otherProgsArgs +addHaddockArgs (progArgs:otherProgsArgs) + = progArgs : addHaddockArgs otherProgsArgs + +newHaddockGhcArgs :: [String] +newHaddockGhcArgs = + [ "--optghc=-fdefer-type-errors" + , "--optghc=-fno-warn-deferred-type-errors" + , "--optghc=-fno-warn-missing-home-modules" + ] diff --git a/dimensions.cabal b/dimensions.cabal --- a/dimensions.cabal +++ b/dimensions.cabal @@ -1,13 +1,13 @@ -cabal-version: 1.12 +cabal-version: 1.24 -- This file has been generated from package.yaml by hpack version 0.31.1. -- -- see: https://github.com/sol/hpack -- --- hash: 982b8bf6393fdd487b646f7c7a3b258acba9501a6d106861757a3b4a49f3de82 +-- hash: 02a12f73c300d1f3b4ea569d86f2222327243c0918b00236786ba647754dd7f2 name: dimensions -version: 2.0.0.0 +version: 2.1.0.0 synopsis: Safe type-level dimensionality for multidimensional data. description: Safe type-level dimensionality for multidimensional data. Please see the README on GitHub at category: math, geometry @@ -18,13 +18,18 @@ copyright: Copyright: (c) 2019 Artem Chirkin license: BSD3 license-file: LICENSE -build-type: Simple +build-type: Custom source-repository head type: git location: https://github.com/achirkin/easytensor subdir: dimensions +custom-setup + setup-depends: + Cabal + , base + flag unsafeindices description: Disable bound checks on Idx and Idxs types. manual: True @@ -42,15 +47,15 @@ Numeric.Tuple.Strict Numeric.TypedList other-modules: - Data.Type.List.InjectiveSnoc + Data.Type.List.Families + Data.Type.List.Classes Data.Type.List.Internal hs-source-dirs: src ghc-options: -Wall -Wcompat -Wtabs -Wmissing-local-signatures -Wmissing-home-modules -Widentities build-depends: base >=4.10 && <5 - , constraints-deriving >=1 && <2 - , ghc + , constraints-deriving >=1.1.1.0 && <2 if flag(unsafeindices) cpp-options: -DUNSAFE_INDICES default-language: Haskell2010 @@ -59,6 +64,7 @@ type: exitcode-stdio-1.0 main-is: Spec.hs other-modules: + Data.Type.ListTest Numeric.Dimensions.DimTest Numeric.Dimensions.IdxTest Paths_dimensions @@ -69,6 +75,6 @@ Cabal , QuickCheck , base - , constraints-deriving >=1 && <2 + , constraints-deriving >=1.1.1.0 && <2 , dimensions default-language: Haskell2010 diff --git a/src/Data/Type/List.hs b/src/Data/Type/List.hs --- a/src/Data/Type/List.hs +++ b/src/Data/Type/List.hs @@ -1,15 +1,15 @@ -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilyDependencies #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + -------------------------------------------------------------------------------- -- | -- Module : Data.Type.List @@ -29,48 +29,25 @@ , StripPrefix, StripSuffix , Reverse, Take, Drop, Length -- * Operations on elements - , All, Map, Elem - -- * Concatenation and its evidence - , ConcatList, evStripSuffix, evStripPrefix, evConcat + , All, Map, UnMap, Elem + -- * Classes that simplify inference of type equalities + , SnocList, ReverseList, ConcatList + , inferStripSuffix, inferStripPrefix, inferConcat -- * Data.Typeable , inferTypeableCons ) where -import Data.Constraint ((:-) (..), Constraint, Dict (..)) -import Data.Type.List.Internal (Snoc) +import Data.Constraint (Constraint, Dict (..)) +import Data.Type.List.Classes +import Data.Type.List.Families import Data.Type.Lits -import GHC.Base (Type) import Type.Reflection -import Unsafe.Coerce (unsafeCoerce) -- | Empty list, same as @'[]@. -type Empty = '[] +type Empty = ('[] :: [k]) -- | Appending a list, represents an @Op@ counterpart of @(':)@. -type Cons (a :: k) (as :: [k]) - = a ': as - --- | Extract the first element of a list, which must be non-empty. -type family Head (xs :: [k]) :: k where - Head ('[] :: [k]) = TypeError ( ListError k "Head: empty type-level list." ) - Head (x ': _) = x - --- | Extract the elements after the head of a list, which must be non-empty. -type family Tail (xs :: [k]) :: [k] where - Tail ('[] :: [k]) = TypeError ( ListError k "Tail: empty type-level list." ) - Tail (_ ': xs) = xs - --- | Extract the last element of a list, which must be non-empty. -type family Last (xs :: [k]) :: k where - Last ('[] :: [k]) = TypeError ( ListError k "Last: empty type-level list." ) - Last '[x] = x - Last (_ ': xs) = Last xs - --- | Extract all but last elements of a list, which must be non-empty. -type family Init (xs :: [k]) :: [k] where - Init ('[] :: [k]) = TypeError ( ListError k "Init: empty type-level list." ) - Init '[x] = '[] - Init (x ': xs) = x ': Init xs +type Cons (a :: k) (as :: [k]) = a ': as -- | @Take n xs@ returns the prefix of a list of length @max n (length xs)@. type family Take (n :: Nat) (xs :: [k]) :: [k] where @@ -84,64 +61,6 @@ Drop n (_ ': xs) = Drop (n - 1) xs Drop _ '[] = '[] --- | Append two lists. -type family Concat (as :: [k]) (bs :: [k]) :: [k] where - Concat '[] bs = bs - Concat as '[] = as - Concat (a ': as) bs = a ': Concat as bs - --- | Remove prefix @as@ from a list @asbs@ if @as@ is a prefix; fail otherwise. -type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where - StripPrefix as as = '[] - StripPrefix '[] asbs = asbs - StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs - StripPrefix (a ': as) (b ': asbs) - = TypeError - ( 'Text "StripPrefix: the first argument is not a prefix of the second." - ':$$: - 'Text "Failed prefix: " ':<>: 'ShowType (a ': as) - ':$$: - 'Text "Second argument: " ':<>: 'ShowType (b ': asbs) - ) - StripPrefix (a ': as) '[] - = TypeError - ( 'Text "StripPrefix: the first argument is longer than the second." - ':$$: - 'Text "Failed prefix: " ':<>: 'ShowType (a ': as) - ':$$: - 'Text "The reduced second argument is empty." - ) - --- | Remove suffix @bs@ from a list @asbs@ if @bs@ is a suffix; fail otherwise. -type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where - StripSuffix bs bs = '[] - StripSuffix '[] asbs = asbs - StripSuffix (a ': bs) (b ': bs) - = TypeError - ( 'Text "StripSuffix: the first argument is not a suffix of the second." - ':$$: - 'Text "Failed match: " - ':<>: 'ShowType ((a ': bs) ~ (b ': bs)) - ) - StripSuffix (b ': bs) '[] - = TypeError - ( 'Text "StripSuffix: the first argument is longer than the second." - ':$$: - 'Text "Failed suffix: " ':<>: 'ShowType (b ': bs) - ':$$: - 'Text "The reduced second argument is empty." - ) - StripSuffix bs (a ': asbs) = a ': StripSuffix bs asbs - --- | Returns the elements of a list in reverse order. -type family Reverse (xs :: [k]) :: [k] where - -- Note: the goal is not to write a fast implementation, - -- but make it easier for the type checker to simplify things. - -- This is only going to be executed during compile time, - -- so there is no real performance impact. - Reverse '[] = '[] - Reverse (x ': xs) = Snoc (Reverse xs) x - -- | Number of elements in a list. type family Length (xs :: [k]) :: Nat where Length '[] = 0 @@ -169,59 +88,18 @@ Map f '[] = '[] Map f (x ': xs) = f x ': Map f xs +-- | Unmap a functor over the elements of a type list. +type family UnMap (f :: a -> b) (xs :: [b]) :: [a] where + UnMap f '[] = '[] + UnMap f (f x ': ys) = x ': UnMap f ys + -- | Check if an item is a member of a list. type family Elem (x :: k) (xs :: [k]) :: Constraint where Elem x (x ': xs) = () Elem x (_ ': xs) = Elem x xs -type ListError k t - = 'Text t ':$$: - ( 'Text "Type-level error occured when operating on a list of kind " - ':<>: 'ShowType [k] ':<>: 'Text "." - ) - --- | Represent a triple of lists forming a relation @(as ++ bs) ~ asbs@ -type ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) = - ( asbs ~ Concat as bs - , as ~ StripSuffix bs asbs - , bs ~ StripPrefix as asbs - ) - --- | Derive @ConcatList@ given @Concat@ -evConcat :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) - . (asbs ~ Concat as bs) :- ConcatList as bs asbs -evConcat = Sub $ unsafeCoerce - ( Dict :: Dict - ( asbs ~ Concat as bs - , as ~ as - , bs ~ bs - ) - ) - --- | Derive @ConcatList@ given @StripSuffix@ -evStripSuffix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) - . (as ~ StripSuffix bs asbs) :- ConcatList as bs asbs -evStripSuffix = Sub $ unsafeCoerce - ( Dict :: Dict - ( asbs ~ asbs - , as ~ StripSuffix bs asbs - , bs ~ bs - ) - ) - --- | Derive @ConcatList@ given @StripPrefix@ -evStripPrefix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) - . (bs ~ StripPrefix as asbs) :- ConcatList as bs asbs -evStripPrefix = Sub $ unsafeCoerce - ( Dict :: Dict - ( asbs ~ asbs - , as ~ as - , bs ~ StripPrefix as asbs - ) - ) - -- | Given a @Typeable@ list, infer this constraint for its parts. -inferTypeableCons :: forall (k :: Type) (ys :: [k]) (x :: k) (xs :: [k]) +inferTypeableCons :: forall ys x xs . (Typeable ys, ys ~ (x ': xs)) => Dict (Typeable x, Typeable xs) inferTypeableCons = case typeRep @ys of diff --git a/src/Data/Type/List/Classes.hs b/src/Data/Type/List/Classes.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/List/Classes.hs @@ -0,0 +1,489 @@ +{-# OPTIONS_HADDOCK hide, prune #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-} +module Data.Type.List.Classes + ( -- * Classes that simplify inference of type equalities + SnocList, ReverseList, ConcatList + , inferStripSuffix, inferStripPrefix, inferConcat + -- auto-generating instances + , nilInstSnocList, consInstSnocList, incohInstSnocList + , consInstReverseList, incohInstReverseList + , nilInstConcatList, consInstConcatList, incohInstConcatList + ) where + +import Data.Constraint (Dict (..)) +import Data.Constraint.Bare +import Data.Constraint.Deriving +import Data.Kind +import Data.Type.Equality +import Unsafe.Coerce (unsafeCoerce) + +import Data.Type.List.Families +import Data.Type.List.Internal + + +-- | Represent a decomposition of a list by appending an element to its end. +class + ( bs ~ Snoc as a, as ~ Init bs, a ~ Last bs + , SnocListCtx as a bs, ConcatList as '[a] bs) + => SnocList (as :: [k]) (a :: k) (bs :: [k]) + | as a -> bs, bs -> as a, as -> k, a -> a, bs -> k where + +-- | Represent two lists that are `Reverse` of each other +class + ( as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as + , ReverseListCtx as bs) + => ReverseList (as :: [k]) (bs :: [k]) + | as -> bs, bs -> as, as -> k, bs -> k + +-- | Represent a triple of lists forming a relation @(as ++ bs) ~ asbs@ +-- +-- NB: functional dependency @bs asbs -> as@ does not seem to be possible, +-- because dependency checking happens before constraints checking +-- and does not take constraints into account. +class + ( asbs ~ Concat as bs + , as ~ StripSuffix bs asbs + , bs ~ StripPrefix as asbs + , ConcatListCtx1 as bs asbs + , ConcatListCtx2 as bs asbs (bs == asbs) + ) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) + | as bs -> asbs, as asbs -> bs --, bs asbs -> as + , as -> k, bs -> k, asbs -> k + + + + +{- Type-dependent constraints - XxxCtx type familes + +Extra "given" constraints provided by class instances via superclass mechanics + (the constraints that depend on the expansion of the type variables) + + +These type families give very handy evidence when you know the structure of +the type variables (e.g. as ~ '[] or as ~ (a' ': 'as)). + +A huge problem with this approach is that sometimes I need to provide these +constraints for incoherent instances when I don't know how the type variables expand. +To workaround this, I need to provide such constraint families that: + + 1. Their runtime representation is the same for all parameter values + 2. If a constraint does not make sense for a given parameter expansion, + replace it with a useless but harmless alternative + 3. XxxCtx must not be in loop with Xxx + (otherwise, typechecker stack overflow occurs at the call site) + + -} + + +type family SnocListCtx (as :: [k]) (a :: k) (bs :: [k]) :: Constraint where + SnocListCtx '[] z bs = + ( Head bs ~ z + , Tail bs ~ '[] + , bs ~ '[z] + , UnreachableConstraint (SnocList (Tail '[]) (Head '[]) (Tail bs)) + "SnocListCtx '[] z bs -- SnocList (Tail '[]) (Head '[]) (Tail bs)" + ) + SnocListCtx (a ': as) z bs = + ( Head bs ~ a + , Tail bs ~ Snoc as z + , bs ~ (Head bs ': Head (Tail bs) ': Tail (Tail bs)) + , SnocList as z (Tail bs) + ) + +type family ReverseListCtx (as :: [k]) (bs :: [k]) :: Constraint where + ReverseListCtx '[] bs = + ( bs ~ '[] + , UnreachableConstraint (ReverseList (Tail '[]) (Init bs)) + "ReverseListCtx '[] bs -- ReverseList (Tail '[]) (Init bs)" + , UnreachableConstraint (SnocList (Init bs) (Head '[]) bs) + "ReverseListCtx '[] bs -- SnocList (Init bs) (Head '[]) bs" + ) + ReverseListCtx (a ': as) bs = + ( bs ~ (Head bs ': Tail bs) + , ReverseList as (Init bs) + , SnocList (Init bs) a bs + ) + +-- | Extra evidence provided by `ConcatList` in various cases +type family ConcatListCtx1 (as :: [k]) (bs :: [k]) (asbs :: [k]) :: Constraint where + ConcatListCtx1 '[] bs asbs = + ( asbs ~ bs + , (bs == asbs) ~ 'True + , UnreachableConstraint (Head '[] ~ Head asbs) + "ConcatListCtx1 '[] bs asbs -- (Head '[] ~ Head asbs)" + , UnreachableConstraint (ConcatList (Tail '[]) bs (Tail asbs)) + "ConcatListCtx1 '[] bs asbs -- ConcatList (Tail '[]) bs (Tail asbs)" + , UnreachableConstraint (ConcatList (Init '[]) (Last '[] ': bs) asbs) + "ConcatListCtx1 '[] bs asbs -- ConcatList (Init '[]) (Last '[] ': bs) asbs" + ) + ConcatListCtx1 (a ': as) bs asbs = + ( asbs ~ (a ': Tail asbs) + , (bs == asbs) ~ 'False + , a ~ Head asbs + , ConcatList as bs (Tail asbs) + , ConcatList (Init (a ': as)) (Last (a ': as) ': bs) asbs + ) +-- | Extra evidence provided by `ConcatList` in various cases +type family ConcatListCtx2 (as :: [k]) (bs :: [k]) (asbs :: [k]) (bsEq :: Bool) :: Constraint where + ConcatListCtx2 as bs asbs 'True = + ( as ~ '[] + , bs ~ asbs + , UnreachableConstraint (ConcatList (Tail as) bs (Tail asbs)) + "ConcatListCtx2 as bs asbs 'True -- ConcatList (Tail as) bs (Tail asbs)" + ) + ConcatListCtx2 as bs (a ': asbs) 'False = + ( as ~ (a ': Tail as) + , a ~ Head as + , ConcatList (Tail as) bs asbs + ) + ConcatListCtx2 as bs '[] _ = + ( as ~ '[] + , bs ~ '[] + , UnreachableConstraint (ConcatList (Tail as) bs (Tail '[])) + "ConcatListCtx2 as bs '[] _ -- ConcatList (Tail as) bs (Tail '[])" + ) + +{- Lookup class data constructors. + +I use my plugin called ClassDict from constraints-deriving package. +It takes a data constructor for a given class and wraps it in Dict. + +The signatures of the functions below are fully determined by the structure +of the corresponding type classes. +But as a user of the ClassDict API, I have to write these signatures by hand + (otherwise the plugin displays a compile-time error with the correct signatures). + + -} + +{-# ANN defineSnocList ClassDict #-} +defineSnocList :: forall (k :: Type) (as :: [k]) (a :: k) (bs :: [k]) + . ( bs ~ Snoc as a, as ~ Init bs, a ~ Last bs + , SnocListCtx as a bs + , ConcatList as '[a] bs + ) + => Dict (SnocList as a bs) +defineSnocList = defineSnocList + +{-# ANN defineReverseList ClassDict #-} +defineReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k]) + . (as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as, ReverseListCtx as bs) + => Dict (ReverseList as bs) +defineReverseList = defineReverseList + +{-# ANN defineConcatList ClassDict #-} +defineConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) + . ( asbs ~ Concat as bs + , as ~ StripSuffix bs asbs + , bs ~ StripPrefix as asbs + , ConcatListCtx1 as bs asbs + , ConcatListCtx2 as bs asbs (bs == asbs) + ) + => Dict (ConcatList as bs asbs) +defineConcatList = defineConcatList + + +{- Creating instances + +The constraints defined about have a lot of recursive references to each other. +This makes defining instances using the standard syntax virtually impossible. + +That is why I create most of the instances manually via the ClassDict+toInstance plugins. + +Even on this way, there are some problems with passing dictionaries recursively; +if I just used `Dict` all the time and pattern match against it, I would get +a lot of <> or "unreachable instances" errors. +Instead, I use the `BareConstraint` abstract data type and pass it to `defineXxx` +functions as if constraints were vanilla values. + +The functions below are helpers that break reference loops. +They also unsafely create all type equality constraints; + it is very easy to introduce a bug here, because I bypass most of the typechecker. + -} + + + +unsafeBareSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k]) + . BareConstraint (SnocListCtx as z bs) + -> BareConstraint (SnocList as z bs) +unsafeBareSnocList = runMagic m + where + m :: SnocListCtx as z bs =-> BareConstraint (SnocList as z bs) + m | Dict <- unsafeEqTypes @bs @(Snoc as z) + , Dict <- unsafeEqTypes @as @(Init bs) + , Dict <- unsafeEqTypes @z @(Last bs) + , Dict <- unsafeEqTypes @bs @(Concat as '[z]) + , Dict <- inferConcat @as @'[z] @bs + = Magic (dictToBare $ defineSnocList @k @as @z @bs) + +unsafeBareReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k]) + . BareConstraint (ReverseList bs as) + -> BareConstraint (ReverseListCtx as bs) + -> BareConstraint (ReverseList as bs) +unsafeBareReverseList = runMagic . runMagic m + where + m :: ReverseList bs as + =-> ReverseListCtx as bs + =-> BareConstraint (ReverseList as bs) + m | Dict <- unsafeEqTypes @as @(Reverse bs) + , Dict <- unsafeEqTypes @bs @(Reverse as) + = Magic (Magic (dictToBare $ defineReverseList @k @as @bs)) + +unsafeBareConcatList :: + forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) + . BareConstraint (ConcatListCtx1 as bs asbs) + -> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs)) + -> BareConstraint (ConcatList as bs asbs) +unsafeBareConcatList = runMagic . runMagic m + where + m :: ConcatListCtx1 as bs asbs + =-> ConcatListCtx2 as bs asbs (bs == asbs) + =-> BareConstraint (ConcatList as bs asbs) + m | Dict <- unsafeEqTypes @as @(StripSuffix bs asbs) + , Dict <- unsafeEqTypes @bs @(StripPrefix as asbs) + , Dict <- unsafeEqTypes @asbs @(Concat as bs) + = Magic (Magic (dictToBare $ defineConcatList @k @as @bs @asbs)) + + +unsafeBareSnocListCtx :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k]) + . BareConstraint (SnocList (Tail as) z (Tail bs)) + -> BareConstraint (SnocListCtx as z bs) +unsafeBareSnocListCtx = runMagic m + where + m :: SnocList (Tail as) z (Tail bs) =-> BareConstraint (SnocListCtx as z bs) + m = Magic (dictToBare d) + d :: SnocList (Tail as) z (Tail bs) => Dict (SnocListCtx as z bs) + d = unsafeCoerce $ Dict + @(Head as ~ Head as, Tail bs ~ Tail bs, bs ~ bs, SnocList (Tail as) z (Tail bs)) + +unsafeBareReverseListCtx :: forall (k :: Type) (as :: [k]) (bs :: [k]) + . BareConstraint (ReverseList (Tail as) (Init bs)) + -> BareConstraint (ReverseListCtx as bs) +unsafeBareReverseListCtx + = runMagic (runMagic m unsafeIncohBareSnocList) + where + m :: SnocList (Init bs) (Head as) bs + =-> ReverseList (Tail as) (Init bs) + =-> BareConstraint (ReverseListCtx as bs) + m = Magic (Magic (dictToBare f)) + f :: ( SnocList (Init bs) (Last bs) bs + , ReverseList (Tail as) (Init bs) + ) + => Dict (ReverseListCtx as bs) + f | Dict <- unsafeEqTypes @(Head as) @(Last bs) + = unsafeCoerce ( + Dict @( bs ~ bs + , ReverseList (Tail as) (Init bs) + , SnocList (Init bs) (Head as) bs) + ) + +unsafeBareConcatListCtx1 :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) + . BareConstraint (ConcatList (Tail as) bs (Tail asbs)) + -> BareConstraint (ConcatList (Init as) (Last as ': bs) asbs) + -> BareConstraint (ConcatListCtx1 as bs asbs) +unsafeBareConcatListCtx1 = runMagic . runMagic m + where + m :: ConcatList (Tail as) bs (Tail asbs) + =-> ConcatList (Init as) (Last as ': bs) asbs + =-> BareConstraint (ConcatListCtx1 as bs asbs) + m = Magic (Magic (dictToBare d)) + d :: ( ConcatList (Tail as) bs (Tail asbs) + , ConcatList (Init as) (Last as ': bs) asbs) + => Dict (ConcatListCtx1 as bs asbs) + d = unsafeCoerce $ Dict + @( asbs ~ asbs, (bs == asbs) ~ (bs == asbs) + , Head asbs ~ Head asbs + , ConcatList (Tail as) bs (Tail asbs) + , ConcatList (Init as) (Last as ': bs) asbs + ) + +unsafeBareConcatListCtx2 :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) + . BareConstraint (ConcatList (Tail as) bs (Tail asbs)) + -> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs)) +unsafeBareConcatListCtx2 = runMagic m + where + m :: ConcatList (Tail as) bs (Tail asbs) + =-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs)) + m = Magic (dictToBare d) + d :: ConcatList (Tail as) bs (Tail asbs) + => Dict (ConcatListCtx2 as bs asbs (bs == asbs)) + d = unsafeCoerce $ Dict + @(as ~ as, Head as ~ Head as, ConcatList (Tail as) bs (Tail asbs)) + + +{- Recursive bindings for generic incoherent instances + +Since all three classes consist solely of some combination of equality constraints +(nested inside algebraic class constructors and constraint tuples), +one can construct instances "from nothing". +These are the three functions below. + + -} + +unsafeIncohBareSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k]) + . BareConstraint (SnocList as z bs) +unsafeIncohBareSnocList = unsafeBareSnocList $ + unsafeBareSnocListCtx @k @as @z @bs unsafeIncohBareSnocList + +unsafeIncohBareReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k]) + . BareConstraint (ReverseList as bs) +unsafeIncohBareReverseList = unsafeBareReverseList @k @as @bs + unsafeIncohBareReverseList + (unsafeBareReverseListCtx @k @as @bs unsafeIncohBareReverseList) + +unsafeIncohBareConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) + . BareConstraint (ConcatList as bs asbs) +unsafeIncohBareConcatList = unsafeBareConcatList @k @as @bs @asbs + (unsafeBareConcatListCtx1 @k @as @bs @asbs unsafeIncohBareConcatList unsafeIncohBareConcatList) + (unsafeBareConcatListCtx2 @k @as @bs @asbs unsafeIncohBareConcatList) + + + + +{- Declaring instances + +The simplest instances can be created using the vanilla syntax; +the rest is derived via the three recursive definitions above. + -} + +-- instance SnocList '[] a '[a] where +{-# ANN nilInstSnocList (ToInstance NoOverlap) #-} +nilInstSnocList :: forall (k :: Type) (a :: k) + . Dict (SnocList '[] a '[a]) +nilInstSnocList + | Dict <- nilInstConcatList @k @'[a] + = defineSnocList @k @'[] @a @'[a] + +-- instance SnocList as z bs => SnocList (a ': as) z (a ': bs) +{-# ANN consInstSnocList (ToInstance NoOverlap) #-} +consInstSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k]) (a :: k) (b :: k) + . SnocList as z (b ': bs) + => Dict (SnocList (a ': as) z (a ': b ': bs)) +consInstSnocList + | Dict <- unsafeEqTypes @(a ': b ': bs) @(Snoc (a ': as) z) + , Dict <- unsafeEqTypes @(a ': as) @(Init (a ': b ': bs)) + , Dict <- unsafeEqTypes @z @(Last (a ': b ': bs)) + , Dict <- consInstConcatList @_ @as @'[z] @(b ': bs) @a + = defineSnocList @k @(a ': as) @z @(a ': b ': bs) + + +-- instance {-# INCOHERENT #-} SnocList as z bs +{-# ANN incohInstSnocList (ToInstance Incoherent) #-} +incohInstSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k]) + . bs ~ Snoc as z + => Dict (SnocList as z bs) +incohInstSnocList = bareToDict $ unsafeIncohBareSnocList @k @as @z @bs + + +instance ReverseList ('[] :: [k]) ('[] :: [k]) + +-- instance (ReverseList as bs', SnocList bs' a (b ': bs)) +-- => ReverseList (a ': as) (b ': bs) +{-# ANN consInstReverseList (ToInstance NoOverlap) #-} +consInstReverseList :: forall (k :: Type) + (a :: k) (as :: [k]) (b :: k) (bs :: [k]) + . (ReverseList as (Init (b ': bs)), SnocList (Init (b ': bs)) a (b ': bs)) + => Dict (ReverseList (a ': as) (b ': bs)) +consInstReverseList = bareToDict d + where + d = runMagic m (rev d) + + m :: ReverseList (b ': bs) (a ': as) + =-> BareConstraint (ReverseList (a ': as) (b ': bs)) + m = Magic f + f :: ReverseList (b ': bs) (a ': as) + => BareConstraint (ReverseList (a ': as) (b ': bs)) + f | Dict <- unsafeEqTypes @(a ': as) @(Reverse (b ': bs)) + , Dict <- unsafeEqTypes @(b ': bs) @(Reverse (a ': as)) + = dictToBare $ defineReverseList + + {- Since both classes, ReverseList and SnocList actually bear no runtime references + to their parameters, the only thing that matters is the length of the list + (the only parameter that affects the content of an instance). + Thus, I can cast the class instances between the lists of the same lengths. + -} + rev :: BareConstraint (ReverseList (a ': as) (b ': bs)) + -> BareConstraint (ReverseList (b ': bs) (a ': as)) + rev = unsafeCoerce + + +{-# ANN incohInstReverseList (ToInstance Incoherent) #-} +incohInstReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k]) + . bs ~ Reverse as + => Dict (ReverseList as bs) +incohInstReverseList = bareToDict $ unsafeIncohBareReverseList @k @as @bs + + + + +-- instance {-# INCOHERENT #-} ConcatList as '[] as +{-# ANN incohInstConcatList (ToInstance Incoherent) #-} +incohInstConcatList :: forall (k :: Type) (as :: [k]) + . Dict (ConcatList as ('[] :: [k]) as) +incohInstConcatList = bareToDict $ unsafeIncohBareConcatList @k @as @'[] @as + +-- instance ConcatList '[] bs bs +{-# ANN nilInstConcatList (ToInstance NoOverlap) #-} +nilInstConcatList :: forall (k :: Type) (bs :: [k]) + . Dict (ConcatList '[] bs bs) +nilInstConcatList + | Dict <- unsafeEqTypes @(bs == bs) @'True + = defineConcatList @k @'[] @bs @bs + +-- instance ConcatList as bs asbs => ConcatList (a ': as) bs (a ': asbs) +{-# ANN consInstConcatList (ToInstance NoOverlap) #-} +consInstConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) (a :: k) + . ConcatList as bs asbs + => Dict (ConcatList (a ': as) bs (a ': asbs)) +consInstConcatList + | Dict <- unsafeEqTypes @(bs == (a ': asbs)) @'False + , Dict <- unsafeEqTypes @(a ': as) @(StripSuffix bs (a ': asbs)) + , Dict <- unsafeEqTypes @bs @(StripPrefix (a ': as) (a ': asbs)) + , Dict <- unsafeEqTypes @(a ': asbs) @(Concat (a ': as) bs) + = let x :: ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs) + => Dict (ConcatList (a ': as) bs (a ': asbs)) + x = defineConcatList @k @(a ': as) @bs @(a ': asbs) + m :: ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs) + =-> BareConstraint (ConcatList (a ': as) bs (a ': asbs)) + m = Magic (dictToBare x) + + shiftedCL :: BareConstraint + (ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs)) + shiftedCL = unsafeIncohBareConcatList + in bareToDict $ runMagic m shiftedCL + + + + +-- | Derive @ConcatList@ given @Concat@ +inferConcat :: forall as bs asbs + . asbs ~ Concat as bs + => Dict (ConcatList as bs asbs) +inferConcat = bareToDict $ unsafeIncohBareConcatList @_ @as @bs @asbs + +-- | Derive @ConcatList@ given @StripSuffix@ +inferStripSuffix :: forall as bs asbs + . as ~ StripSuffix bs asbs + => Dict (ConcatList as bs asbs) +inferStripSuffix = bareToDict $ unsafeIncohBareConcatList @_ @as @bs @asbs + +-- | Derive @ConcatList@ given @StripPrefix@ +inferStripPrefix :: forall as bs asbs + . bs ~ StripPrefix as asbs + => Dict (ConcatList as bs asbs) +inferStripPrefix = bareToDict $ unsafeIncohBareConcatList @_ @as @bs @asbs diff --git a/src/Data/Type/List/Families.hs b/src/Data/Type/List/Families.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/List/Families.hs @@ -0,0 +1,84 @@ +{-# OPTIONS_HADDOCK hide, prune #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Type.List.Families + ( Head, Tail + , Snoc, Init, Last, Reverse + , StripSuffix, StripPrefix, Concat + -- * Internals + , List (..), RunList, Snoc', Reverse' + ) where + + +-- | Extract the first element of a list, which must be non-empty. +type family Head (xs :: [k]) :: k where + Head (x ': _) = x + +-- | Extract the elements after the head of a list, which must be non-empty. +type family Tail (xs :: [k]) :: [k] where + Tail (_ ': xs) = xs + +-- | Extract the last element of a list, which must be non-empty. +type family Last (xs :: [k]) :: k where + Last '[x] = x + Last (_ ': xs) = Last xs + +-- | Extract all but last elements of a list, which must be non-empty. +type family Init (xs :: [k]) = (ys :: [k]) | ys -> k where + Init ('[x] :: [k]) = ('[] :: [k]) + Init (x ': xs) = x ': Init xs + +-- | Appending a list on the other side (injective). +type Snoc (xs :: [k]) (x :: k) = (RunList (Snoc' xs x :: List k) :: [k]) + +-- | Reverse elements of a list (injective). +type Reverse (xs :: [k]) = (RunList (Reverse' xs :: List k) :: [k]) + +-- | A helper data type that makes possible injective `Snoc` and `Reverse` families. +-- +-- It assures GHC type checker that the `Snoc` operation on a non-empty list +-- yields a list that contains at least two elements. +data List k + = Empty + | Single k + | TwoOrMore [k] + -- ^ An important invariant: the argument list contains at least two elements. + +type family RunList (xs :: List k) = (ys :: [k]) | ys -> k xs where + RunList ('Empty :: List k) = ('[] :: [k]) + RunList ('Single x) = '[x] + RunList ('TwoOrMore (x ': y ': xs)) = x ': y ': xs + +type family Snoc' (xs :: [k]) (x :: k) = (ys :: List k) | ys -> k xs x where + Snoc' '[] y = 'Single y + Snoc' (x ': xs) y = 'TwoOrMore (x ': RunList (Snoc' xs y)) + +type family Reverse' (xs :: [k]) = (ys :: List k) | ys -> k xs where + Reverse' ('[] :: [k]) = ('Empty :: List k) + Reverse' '[x] = 'Single x + Reverse' (y ': x ': xs) = 'TwoOrMore (Snoc (RunList (Reverse' (x ': xs))) y) + + +-- | Append two lists. +type family Concat (as :: [k]) (bs :: [k]) :: [k] where + Concat as '[] = as -- "incoherent instance" + Concat '[] bs = bs + Concat (a ': as) bs = a ': Concat as bs + +-- | Remove prefix @as@ from a list @asbs@ if @as@ is a prefix; fail otherwise. +type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where + StripPrefix as as = '[] -- "incoherent instance" + StripPrefix '[] bs = bs + StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs + +-- | Remove suffix @bs@ from a list @asbs@ if @bs@ is a suffix; fail otherwise. +type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where + StripSuffix '[] as = as -- "incoherent instance" + StripSuffix bs bs = '[] + StripSuffix bs (a ': asbs) = a ': StripSuffix bs asbs diff --git a/src/Data/Type/List/InjectiveSnoc.hs b/src/Data/Type/List/InjectiveSnoc.hs deleted file mode 100644 --- a/src/Data/Type/List/InjectiveSnoc.hs +++ /dev/null @@ -1,67 +0,0 @@ -{-# OPTIONS_GHC -fobject-code #-} -{-# OPTIONS_HADDOCK hide, prune #-} --------------------------------------------------------------------------------- --- | --- Module : Data.Type.List.InjectiveSnoc --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- A small core plugin to make GHC think that @Snoc@ is injective --- --- --------------------------------------------------------------------------------- -module Data.Type.List.InjectiveSnoc ( plugin ) where - - -import CoAxiom (CoAxBranch (..), CoAxiom (..), mapAccumBranches) -import Data.Maybe (fromMaybe) -import GhcPlugins - --- NB: check out --- https://github.com/ghc/ghc/blob/bf73419518ca550e85188616f860961c7e2a336b/compiler/typecheck/TcTypeNats.hs --- for further ideas. --- Maybe, I can use BuiltInSynFamily to do a lot of super cool stuff! - --- | A small core plugin to make GHC think that @Snoc@ is injective -plugin :: Plugin -plugin = defaultPlugin - { installCoreToDos = - const $ pure . (CoreDoPluginPass "InjectiveSnoc" injectiveSnocPass :) - } - -injectiveSnocPass :: ModGuts -> CoreM ModGuts -injectiveSnocPass = pure . modSnocFam updateSnocFam - -modSnocFam :: (TyCon -> TyCon) -> ModGuts -> ModGuts -modSnocFam f guts = guts {mg_tcs = map g (mg_tcs guts)} - where - g tc - | nameOccName (tyConName tc) == mkTcOcc "Snoc" = f tc - | otherwise = tc - -updateSnocFam :: TyCon -> TyCon -updateSnocFam tc = fromMaybe tc $ do - axiom <- isClosedSynFamilyTyConWithAxiom_maybe tc - let newAxiom = axiom - { co_ax_tc = newTc - , co_ax_branches = mapAccumBranches f (co_ax_branches axiom) - } - f _ b = b { cab_rhs = repTc (cab_rhs b) } - repTc t = case splitTyConApp_maybe t of - Just (c, ts) - | nameOccName (tyConName c) == mkTcOcc "Snoc" - -> mkTyConApp newTc $ map repTc ts - | otherwise - -> mkTyConApp c $ map repTc ts - Nothing - -> t - newTc = mkFamilyTyCon - (tyConName tc) -- Name - (tyConBinders tc) -- [TyConBinder] - (tyConResKind tc) -- Kind - (famTcResVar tc) -- Maybe Name - (ClosedSynFamilyTyCon (Just newAxiom)) -- FamTyConFlav - (tyConAssoc_maybe tc) -- Maybe Class - -- Injectivity copied from a dummy injective TF with the same head - (Injective [True, True, True]) -- Injectivity - return newTc diff --git a/src/Data/Type/List/Internal.hs b/src/Data/Type/List/Internal.hs --- a/src/Data/Type/List/Internal.hs +++ b/src/Data/Type/List/Internal.hs @@ -1,27 +1,58 @@ -{-# OPTIONS_GHC -fobject-code #-} -{-# OPTIONS_GHC -fplugin Data.Type.List.InjectiveSnoc #-} {-# OPTIONS_HADDOCK hide, prune #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE TypeFamilyDependencies #-} -{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableSuperClasses #-} +module Data.Type.List.Internal + ( UnreachableConstraint (..) + , type (=->) (..), runMagic, unsafeEqTypes + ) where -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE UndecidableInstances #-} --------------------------------------------------------------------------------- --- | --- Module : Data.Type.List.Internal --- Copyright : (c) Artem Chirkin --- License : BSD3 --- --- Thanks to @Data.Type.List.InjectiveSnoc@, @Snoc@ appears to be injective --- for an oustide viewer. --- --- --------------------------------------------------------------------------------- -module Data.Type.List.Internal ( Snoc ) where +import Data.Constraint (Dict (..)) +import Data.Constraint.Bare +import Data.Kind +import Data.Proxy +import GHC.TypeLits +import Unsafe.Coerce (unsafeCoerce) --- | Appending a list on the other side. -type family Snoc (xs :: [k]) (x :: k) = (ys :: [k]) where - Snoc (x ': xs) y = x ': Snoc xs y - Snoc '[] y = '[y] + +{- | +This class should have the same runtime representation as its parameter ctx. +The point is to make sure GHC won't segfault if it mixes up `UnreachableConstraint ctx` +with `ctx` itself: + + If GHC mistakenly recognizes `UnreachableConstraint ctx` dictionary as + `ctx` dictionary, a call to this dictionary should return an error + as defined by `unreachable` function rather than the panic. + +Note, I must not put `ctx` in the superclass position to prevent GHC from +trying to use it. + -} +class UnreachableConstraint (ctx :: Constraint) (msg :: Symbol) where + unreachable :: BareConstraint ctx + +instance KnownSymbol msg + => UnreachableConstraint ctx msg where + unreachable = error $ "Unreachable constraint:: " ++ symbolVal (Proxy @msg) + + +newtype c =-> r = Magic (c => r) +infixr 0 =-> + +runMagic :: (c =-> r) -> BareConstraint c -> r +runMagic = unsafeCoerce +{-# NOINLINE runMagic #-} + + +unsafeEqTypes :: forall a b + . Dict (a ~ b) +unsafeEqTypes = unsafeCoerce (Dict :: Dict (a ~ a)) diff --git a/src/Data/Type/Lits.hs b/src/Data/Type/Lits.hs --- a/src/Data/Type/Lits.hs +++ b/src/Data/Type/Lits.hs @@ -1,17 +1,19 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ExplicitForAll #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} #if __GLASGOW_HASKELL__ >= 806 -{-# LANGUAGE NoStarIsType #-} +{-# LANGUAGE NoStarIsType #-} #endif -{-# LANGUAGE FlexibleContexts #-} -------------------------------------------------------------------------------- -- | -- Module : Data.Type.List @@ -26,6 +28,7 @@ module Data.Type.Lits ( -- * Kinds TN.Nat, TL.Symbol + , KindOf, KindOfEl -- * Linking type and value level , TN.KnownNat, TN.natVal, TN.natVal' , TL.KnownSymbol, TL.symbolVal, TL.symbolVal' @@ -35,6 +38,7 @@ -- * Functions on type literals , type (+), type (*), type (^), type (-) , type TN.Div, type TN.Mod, type TN.Log2 + , type Min, type Max , TL.AppendSymbol, ShowNat , TN.CmpNat, TL.CmpSymbol, type (<=) , SOrdering (..), cmpNat, cmpSymbol @@ -101,15 +105,45 @@ GT -> unsafeCoerce SGT {-# INLINE cmpSymbol #-} +-- | Miminum among two type-level naturals. +type Min (a :: TN.Nat) (b :: TN.Nat) = Min' a b (TN.CmpNat a b) + +-- | Maximum among two type-level naturals. +type Max (a :: TN.Nat) (b :: TN.Nat) = Min' a b (TN.CmpNat a b) + +type family Min' (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) :: TN.Nat where + Min' a _ 'LT = a + Min' a _ 'EQ = a + Min' _ b 'GT = b + +type family Max' (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) :: TN.Nat where + Max' _ b 'LT = b + Max' _ b 'EQ = b + Max' a _ 'GT = a + -- | Comparison of type-level naturals, as a constraint. type (<=) (a :: TN.Nat) (b :: TN.Nat) = LE a b (TN.CmpNat a b) -type family LE (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) :: Constraint where - LE _ _ 'LT = () - LE _ _ 'EQ = () - LE a b 'GT = TL.TypeError +type family LE (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) + = (y :: Constraint) | y -> r where + LE a b 'LT = ('LT ~ TN.CmpNat a b) + LE a b 'EQ = ('EQ ~ TN.CmpNat a b) + LE a b 'GT = ('GT ~ TL.TypeError ('TL.Text "Cannot deduce type-level Nat relation: " 'TL.:<>: 'TL.ShowType a 'TL.:<>: 'TL.Text " <= " 'TL.:<>: 'TL.ShowType b - ) + )) + + +-- | Get the kind of a given type. +-- Useful when we don't want to introduce another type parameter into +-- a type signature (because the kind is determined by the type), +-- but need to have some constraints on the type's kind. +type KindOf (t :: k) = k + +-- | Get the kind of a given list type. +-- Useful when we don't want to introduce another type parameter into +-- a type signature (because the kind is determined by the type), +-- but need to have some constraints on the type's kind. +type KindOfEl (ts :: [k]) = k diff --git a/src/Numeric/Dimensions/Dim.hs b/src/Numeric/Dimensions/Dim.hs --- a/src/Numeric/Dimensions/Dim.hs +++ b/src/Numeric/Dimensions/Dim.hs @@ -4,6 +4,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} @@ -25,6 +26,7 @@ #if __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType #-} #endif +{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-} ----------------------------------------------------------------------------- -- | -- Module : Numeric.Dimensions.Dim @@ -47,21 +49,24 @@ ----------------------------------------------------------------------------- module Numeric.Dimensions.Dim - ( -- * @Dim@ -- a @Nat@-indexed dimension + ( -- * @Dim@: a @Nat@-indexed dimension -- ** Type level numbers that can be unknown. - XNat (..), XN, N, XNatType (..) + Nat, XNat (..), XN, N + , DimType (..), KnownDimType(..), DimKind (..), KnownDimKind(..) -- ** Term level dimension , Dim ( D, Dn, Dx , D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, D10, D11, D12, D13 , D14, D15, D16, D17, D18, D19, D20, D21, D22, D23, D24, D25 ) , SomeDim - , KnownDim (..), BoundedDim (..), minDim, KnownXNatType (..), FixedDim + , KnownDim (..), withKnownXDim + , BoundedDim (..), minimalDim, ExactDim, FixedDim , dimVal, dimVal', typeableDim, someDimVal , sameDim, sameDim' + , lessOrEqDim, lessOrEqDim' , compareDim, compareDim' , constrainBy, relax - -- * Simple Dim arithmetics + -- ** Simple Dim arithmetics -- -- The functions below create singleton values that work as a witness -- of `KnownDim` instance for type-level Nat operations. @@ -76,63 +81,115 @@ -- The good side is the confidence that they behave exactly as -- their @Word@ counterparts. , plusDim, minusDim, minusDimM, timesDim, powerDim, divDim, modDim, log2Dim + , minDim, maxDim -- ** Re-export part of `Data.Type.Lits` for convenience - , Nat, CmpNat, SOrdering (..), type (+), type (-), type (*), type (^), type (<=) - -- ** Inferring kind of type-level dimension - , KnownDimKind (..), DimKind (..) - -- * @Dims@ -- a list of dimensions - , Dims, SomeDims (..), Dimensions (..), BoundedDims (..), minDims - , TypedList ( Dims, XDims, AsXDims, KnownDims + , CmpNat, SOrdering (..), type (+), type (-), type (*), type (^), type (<=) + , Min, Max + -- * @Dims@: a list of dimensions + , Dims, SomeDims (..), Dimensions (..), withKnownXDims + , BoundedDims (..), DimsBound, minimalDims + , ExactDims, FixedDims, inferFixedDims, inferExactFixedDims + , TypedList ( Dims, XDims, KnownDims , U, (:*), Empty, TypeList, Cons, Snoc, Reverse) , typeableDims, inferTypeableDims , listDims, someDimsVal, totalDim, totalDim' , sameDims, sameDims' - , inSpaceOf, asSpaceOf - , xDims, xDims' + , inSpaceOf , stripPrefixDims, stripSuffixDims - -- ** Type-level programming - -- Provide type families to work with lists of dimensions (`[Nat]` or `[XNat]`) - , AsXDims, AsDims, FixedDims, KnownXNatTypes -- ** Re-export type list , RepresentableList (..), TypeList, types , order, order' + , KindOf, KindOfEl +#if !(defined(__HADDOCK__) || defined(__HADDOCK_VERSION__)) + -- hide a plugin-related func + , incohInstBoundedDims +#endif ) where -import Data.Bits (countLeadingZeros, finiteBitSize) +import Data.Bits (countLeadingZeros, finiteBitSize) import Data.Coerce import Data.Constraint -import Data.Data hiding (TypeRep, typeRep, typeRepTyCon) -import Data.Kind (Constraint, Type) -import qualified Data.List (stripPrefix) +import Data.Constraint.Bare +import Data.Constraint.Deriving +import Data.Data hiding (TypeRep, typeRep, + typeRepTyCon) +import Data.Kind (Type) +import qualified Data.List (stripPrefix) import Data.Type.List +import Data.Type.List.Internal import Data.Type.Lits -import GHC.Exts (Proxy#, proxy#, unsafeCoerce#) -import qualified GHC.Generics as G -import Numeric.Natural (Natural) +import GHC.Exts (Proxy#, RuntimeRep, TYPE, proxy#) +import qualified GHC.Generics as G +import Numeric.Natural (Natural) import Numeric.TypedList -import qualified Text.Read as Read -import qualified Text.Read.Lex as Read +import qualified Text.Read as Read +import qualified Text.Read.Lex as Read import Type.Reflection - +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 +type XN = 'XN -- | Known natural number -type N (n::Nat) = 'N n +type N = 'N --- | Find out whether @XNat@ is of known or constrained type. -data XNatType :: XNat -> Type where +-- | GADT to support `KnownDimType` type class. +-- Find out if this type variable is a @Nat@ or @XNat@, +-- and whether @XNat@ is of known or constrained type. +data DimType (d :: k) where + -- | This is a plain @Nat@ + DimTNat :: DimType (n :: Nat) -- | Given @XNat@ is known - Nt :: XNatType ('N n) + DimTXNatN :: DimType (N n) -- | Given @XNat@ is constrained unknown - XNt :: XNatType ('XN m) + DimTXNatX :: DimType (XN m) --- | Same as `SomeNat` -type SomeDim = Dim ('XN 0) +-- | GADT to support `KnownDimKind` type class. +-- Match against its constructors to know if @k@ is @Nat@ or @XNat@ +data DimKind (k :: Type) where + -- | Working on @Nat@. + DimKNat :: DimKind Nat + -- | Working on @XNat@. + DimKXNat :: DimKind XNat +-- | Figure out whether the type-level dimension is `Nat`, or `N Nat`, or `XN Nat`. +class KnownDimType d where + -- | Pattern-match against this to out the value (type) of the dim type variable. + dimType :: DimType d + +-- | Figure out whether the type-level dimension is `Nat` or `XNat`. +class KnownDimKind k where + -- | Pattern-match against this to out the kind of the dim type variable. + dimKind :: DimKind k + +instance KnownDimType (n :: Nat) where + dimType = DimTNat + {-# INLINE dimType #-} + +instance KnownDimType ('N n :: XNat) where + dimType = DimTXNatN + {-# INLINE dimType #-} + +instance KnownDimType ('XN n :: XNat) where + dimType = DimTXNatX + {-# INLINE dimType #-} + +instance KnownDimKind Nat where + dimKind = DimKNat + {-# INLINE dimKind #-} + +instance KnownDimKind XNat where + dimKind = DimKXNat + {-# INLINE dimKind #-} + +instance Class (KnownDimKind k) (KnownDimType (n :: k)) where + cls = Sub $ case dimType @n of + DimTNat -> Dict + DimTXNatN -> Dict + DimTXNatX -> Dict + -- | Singleton type to store type-level dimension value. -- -- On the one hand, it can be used to let type-inference system know @@ -146,39 +203,61 @@ newtype Dim (x :: k) = DimSing Word deriving ( Typeable ) +-- | Same as `SomeNat` +type SomeDim = Dim (XN 0) + -- | Type-level dimensionality. -type Dims (xs :: [k]) = TypedList Dim xs +type Dims = (TypedList Dim :: [k] -> Type) +#define PLEASE_STYLISH_HASKELL \ + forall d . KnownDimType d => \ + (KindOf d ~ Nat, KnownDim d) => \ + Dim d + -- | Match against this pattern to bring `KnownDim` instance into scope. -pattern D :: forall (n :: Nat) . () => KnownDim n => Dim n -pattern D <- (dimEv -> Dict) +pattern D :: PLEASE_STYLISH_HASKELL +pattern D <- (patDim (dimType @d) -> PatNat) where - D = dim @n -{-# COMPLETE D #-} + D = dim @d +#undef PLEASE_STYLISH_HASKELL + +#define PLEASE_STYLISH_HASKELL \ + forall d . KnownDimType d => \ + forall (n :: Nat) . (KindOf d ~ XNat, d ~ N n) => \ + Dim n -> Dim d + -- | 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) +pattern Dn :: PLEASE_STYLISH_HASKELL +pattern Dn k <- (patDim (dimType @d) -> PatXNatN k) where Dn k = coerce k +#undef PLEASE_STYLISH_HASKELL +#define PLEASE_STYLISH_HASKELL \ + forall d . KnownDimType d => \ + forall (m :: Nat) (n :: Nat) . (KindOf d ~ XNat, d ~ XN m, m <= n) => \ + Dim n -> Dim d + -- | `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, m <= n, xn ~ 'XN m) => Dim n -> Dim xn -pattern Dx k <- (dimXNEv (xNatType @xn) -> PatXN k) +pattern Dx :: PLEASE_STYLISH_HASKELL +pattern Dx k <- (patDim (dimType @d) -> PatXNatX k) where Dx k = coerce k +#undef PLEASE_STYLISH_HASKELL + +{-# COMPLETE D #-} {-# COMPLETE Dn, Dx #-} +{-# COMPLETE D, Dn, Dx #-} -- | This class provides the `Dim` associated with a type-level natural. -- --- Note, kind of the @KnownDim@ argument is always @Nat@, because +-- Note, kind of the @KnownDim@ argument is usually @Nat@, because -- it is impossible to create a unique @KnownDim (XN m)@ instance. -class KnownDim (n :: Nat) where +-- Nevertheless, you can have @KnownDim (N n)@, which is useful in some cases. +class KnownDim n where -- | Get value of type-level dim at runtime. -- -- Note, this function is supposed to be used with @TypeApplications@. @@ -198,21 +277,27 @@ -- | Get a minimal or exact bound of a @Dim@. -- -- To satisfy the @BoundedDim@ means to be equal to @N n@ or be not less than @XN m@. -class KnownDimKind k => BoundedDim (n :: k) where +class (KnownDimKind (KindOf d), KnownDimType d, KnownDim (DimBound d)) + => BoundedDim d where -- | Minimal or exact bound of a @Dim@. -- Useful for indexing: it is safe to index something by an index less than -- @DimBound n@ (for both @Nat@ and @Xnat@ indexed dims). - type family DimBound n :: Nat + type family DimBound d :: Nat -- | Get such a minimal @Dim (DimBound n)@, that @Dim n@ is guaranteed -- to be not less than @dimBound@ if @n ~ XN a@, - -- otherwise, the return @Dim@ is the same as @n@. - dimBound :: Dim (DimBound n) - -- | If the runtime value of @Dim y@ satisfies @dimBound @k @x@, + -- otherwise, the return @Dim@ is the same as @n@. + dimBound :: Dim (DimBound d) + -- | If the runtime value of @Dim y@ satisfies @dimBound @x@, -- then coerce to @Dim x@. Otherwise, return @Nothing@. -- -- To satisfy the @dimBound@ means to be equal to @N n@ or be not less than @XN m@. - constrainDim :: forall (l :: Type) (y :: l) . Dim y -> Maybe (Dim n) + constrainDim :: forall y . Dim y -> Maybe (Dim d) +-- | Returns the minimal @Dim@ that satisfies the @BoundedDim@ constraint +-- (this is the exact @dim@ for @Nat@s and the minimal bound for @XNat@s). +minimalDim :: forall n . BoundedDim n => Dim n +minimalDim = coerce (dimBound @n) +{-# INLINE minimalDim #-} instance KnownDim n => BoundedDim (n :: Nat) where type DimBound n = n @@ -223,8 +308,8 @@ | otherwise = Nothing {-# INLINE constrainDim #-} -instance KnownDim n => BoundedDim ('N n) where - type DimBound ('N n) = n +instance KnownDim n => BoundedDim (N n) where + type DimBound (N n) = n dimBound = dim @n {-# INLINE dimBound #-} constrainDim (DimSing y) @@ -232,7 +317,7 @@ | otherwise = Nothing {-# INLINE constrainDim #-} -instance KnownDim m => BoundedDim ('XN m) where +instance KnownDim m => BoundedDim (XN m) where type DimBound ('XN m) = m dimBound = dim @m {-# INLINE dimBound #-} @@ -241,33 +326,20 @@ | otherwise = Nothing {-# INLINE constrainDim #-} -minDim :: forall (k :: Type) (d :: k) . BoundedDim d => Dim d -minDim = coerce (dimBound @k @d) - --- | 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.TypeNats`, but returns `Word`. -dimVal :: forall (k :: Type) (x :: k) . Dim (x :: k) -> Word +dimVal :: forall x . Dim x -> Word dimVal = coerce {-# INLINE dimVal #-} -- | Similar to `natVal` from `GHC.TypeNats`, but returns `Word`. -dimVal' :: forall (n :: Nat) . KnownDim n => Word +dimVal' :: forall n . KnownDim n => Word dimVal' = coerce (dim @n) {-# INLINE dimVal' #-} -- | Construct a @Dim n@ if there is an instance of @Typeable n@ around. +-- +-- Note: we can do this only for @Nat@-indexed dim, because the type @XN m@ +-- does not have enough information to create a dim at runtime. typeableDim :: forall (n :: Nat) . Typeable n => Dim n {- YES, that's right. TyCon of a Nat is a string containing the Nat value. There simply no place in a TyCon to keep the Nat as a number @@ -288,7 +360,12 @@ FixedDim ('N a) b = a ~ b FixedDim ('XN m) b = m <= b -instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where +-- | This is either @Nat@, or a known @XNat@ (i.e. @N n@). +type family ExactDim (d :: k) :: Constraint where + ExactDim (_ :: Nat) = () + ExactDim (x :: XNat) = (x ~ N (DimBound x)) + +instance KnownNat n => KnownDim n where {-# INLINE dim #-} dim = DimSing (fromIntegral (natVal' (proxy# :: Proxy# n))) @@ -345,6 +422,23 @@ instance {-# OVERLAPPING #-} KnownDim 25 where { {-# INLINE dim #-}; dim = DimSing 25 } +instance KnownDim n => KnownDim (N n) where + {-# INLINE dim #-} + dim = coerce (dim @n) + +-- | If you have @KnownDim d@, then @d@ can only be @Nat@ or a known type of +-- @XNat@ (i.e. @N n@). +-- This function assures the type checker that this is indeed the case. +withKnownXDim :: forall (d :: XNat) (rep :: RuntimeRep) (r :: TYPE rep) + . KnownDim d + => ( (KnownDim (DimBound d), ExactDim d + , KnownDimType d, FixedDim d (DimBound d)) => r) + -> r +withKnownXDim + | Dict <- unsafeEqTypes @d @(N (DimBound d)) + = reifyDim @Nat @(DimBound d) (coerce (dim @d)) +{-# INLINE withKnownXDim #-} + instance Class (KnownNat n) (KnownDim n) where cls = Sub $ reifyNat @_ @n (fromIntegral $ dimVal' @n) Dict @@ -355,9 +449,9 @@ -- | `constrainDim` with explicitly-passed constraining @Dim@ -- to avoid @AllowAmbiguousTypes@. -constrainBy :: forall (k :: Type) (x :: k) (p :: k -> Type) (l :: Type) (y :: l) +constrainBy :: forall x p y . BoundedDim x => p x -> Dim y -> Maybe (Dim x) -constrainBy = const (constrainDim @k @x @l @y) +constrainBy = const (constrainDim @x @y) {-# INLINE constrainBy #-} -- | Decrease minimum allowed size of a @Dim (XN x)@. @@ -374,18 +468,32 @@ sameDim :: forall (x :: Nat) (y :: Nat) . Dim x -> Dim y -> Maybe (Dict (x ~ y)) sameDim (DimSing a) (DimSing b) - | a == b = Just (unsafeCoerceDict @(x ~ x) Dict) + | a == b = Just (unsafeEqTypes @x @y) | 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 :: Nat -> Type) (q :: Nat -> Type) - . (KnownDim x, KnownDim y) - => p x -> q y -> Maybe (Dict (x ~ y)) -sameDim' = const . const $ sameDim (dim @x) (dim @y) +sameDim' :: forall (x :: Nat) (y :: Nat) + . (KnownDim x, KnownDim y) => Maybe (Dict (x ~ y)) +sameDim' = sameDim (dim @x) (dim @y) {-# INLINE sameDim' #-} +-- | We either get evidence that @x@ is not greater than @y@, or Nothing. +lessOrEqDim :: forall (x :: Nat) (y :: Nat) + . Dim x -> Dim y -> Maybe (Dict (x <= y)) +lessOrEqDim a b = case compareDim a b of + SLT -> Just Dict + SEQ -> Just Dict + SGT -> Nothing +{-# INLINE lessOrEqDim #-} + +-- | We either get evidence that @x@ is not greater than @y@, or Nothing. +lessOrEqDim' :: forall (x :: Nat) (y :: Nat) + . (KnownDim x, KnownDim y) => Maybe (Dict (x <= y)) +lessOrEqDim' = lessOrEqDim (dim @x) (dim @y) +{-# INLINE lessOrEqDim' #-} + -- | Ordering of dimension values. -- -- Note: `CmpNat` forces type parameters to kind `Nat`; @@ -394,73 +502,90 @@ . Dim a -> Dim b -> SOrdering (CmpNat a b) compareDim a b = case coerce (compare :: Word -> Word -> Ordering) a b of - LT -> unsafeCoerce# SLT - EQ -> unsafeCoerce# SEQ - GT -> unsafeCoerce# SGT + LT -> unsafeCoerce SLT + EQ -> unsafeCoerce SEQ + GT -> unsafeCoerce SGT {-# INLINE compareDim #-} -- | Ordering of dimension values. -- -- Note: `CmpNat` forces type parameters to kind `Nat`; -- if you want to compare unknown `XNat`s, use `Ord` instance of `Dim`. -compareDim' :: forall (a :: Nat) (b :: Nat) (p :: Nat -> Type) (q :: Nat -> Type) - . (KnownDim a, KnownDim b) => p a -> q b -> SOrdering (CmpNat a b) -compareDim' = const . const $ compareDim (dim @a) (dim @b) +compareDim' :: forall (a :: Nat) (b :: Nat) + . (KnownDim a, KnownDim b) => SOrdering (CmpNat a b) +compareDim' = compareDim (dim @a) (dim @b) {-# INLINE compareDim' #-} +-- | Same as `Prelude.(+)`. +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (n + m)@. plusDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (n + m) plusDim = coerce ((+) :: Word -> Word -> Word) {-# INLINE plusDim #-} +-- | Same as `Prelude.(-)`. +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (n - m)@. minusDim :: forall (n :: Nat) (m :: Nat) . (<=) m n => Dim n -> Dim m -> Dim (n - m) minusDim = coerce ((-) :: Word -> Word -> Word) {-# INLINE minusDim #-} +-- | Similar to `minusDim`, but returns @Nothing@ if the result would be negative. +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (n - m)@. minusDimM :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Maybe (Dim (n - m)) minusDimM (DimSing a) (DimSing b) | a >= b = Just (coerce (a - b)) | otherwise = Nothing {-# INLINE minusDimM #-} +-- | Same as `Prelude.(*)`. +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (n * m)@. timesDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((*) n m) timesDim = coerce ((*) :: Word -> Word -> Word) {-# INLINE timesDim #-} +-- | Same as `Prelude.(^)`. +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (n ^ m)@. powerDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((^) n m) powerDim = coerce ((^) :: Word -> Word -> Word) {-# INLINE powerDim #-} +-- | Same as `Prelude.div`. +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (Div n m)@. divDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Div n m) divDim = coerce (div :: Word -> Word -> Word) +-- | Same as `Prelude.mod`. +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (Mod n m)@. modDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Mod n m) modDim = coerce (mod :: Word -> Word -> Word) +-- | Returns log base 2 (round down). +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (Log2 n)@. log2Dim :: forall (n :: Nat) . Dim n -> Dim (Log2 n) log2Dim (DimSing 0) = undefined log2Dim (DimSing x) = DimSing . fromIntegral $ finiteBitSize x - 1 - countLeadingZeros x +-- | Same as `Prelude.min`. +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (Min n m)@. +minDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Min n m) +minDim = coerce (min :: Word -> Word -> Word) --- | 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 +-- | Same as `Prelude.max`. +-- Pattern-matching against the result would produce the evindence +-- @KnownDim (Max n m)@. +maxDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Max n m) +maxDim = coerce (max :: Word -> Word -> Word) --- | Figure out whether the type-level dimension is `Nat` or `XNat`. --- Useful for generalized inference functions. -class KnownDimKind (k :: Type) where - dimKind :: DimKind k -instance KnownDimKind Nat where - dimKind = DimNat -instance KnownDimKind XNat where - dimKind = DimXNat - - -- | Match @Dim n@ against a concrete @Nat@ pattern D0 :: forall (n :: Nat) . () => n ~ 0 => Dim n pattern D0 <- (sameDim (D @0) -> Just Dict) @@ -592,16 +717,42 @@ where D25 = DimSing 25 +#define PLEASE_STYLISH_HASKELL \ + forall ds . KnownDimKind (KindOfEl ds) => \ + (KindOfEl ds ~ Nat, Dimensions ds) => \ + Dims ds -- | @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 :: [Nat]) . () => Dimensions ds => Dims ds -pattern Dims <- (dimsEv -> Dict) +pattern Dims :: PLEASE_STYLISH_HASKELL +pattern Dims <- (patDims (dimKind @(KindOfEl ds)) -> PatNats) where Dims = dims @ds +#undef PLEASE_STYLISH_HASKELL + + +#define PLEASE_STYLISH_HASKELL \ + forall ds . KnownDimKind (KindOfEl ds) => \ + forall (ns :: [Nat]) . (KindOfEl ds ~ XNat, FixedDims ds ns) => \ + Dims ns -> Dims ds + +-- | @O(n)@ +-- 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. +pattern XDims :: PLEASE_STYLISH_HASKELL +pattern XDims ns <- (patDims (dimKind @(KindOfEl ds)) -> PatXNats ns) + where + XDims = unsafeCastTL +#undef PLEASE_STYLISH_HASKELL + {-# COMPLETE Dims #-} +{-# COMPLETE XDims #-} +{-# COMPLETE Dims, XDims #-} -- | @O(Length ds)@ A heavy weapon against all sorts of type errors pattern KnownDims :: forall (ds :: [Nat]) . () @@ -613,31 +764,6 @@ KnownDims = dims @ds {-# COMPLETE KnownDims #-} --- | 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 -{-# COMPLETE XDims #-} - --- | 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 -{-# COMPLETE AsXDims #-} - -- | Same as SomeNat, but for Dimensions: -- Hide all information about Dimensions inside data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns) @@ -645,10 +771,11 @@ -- | Put runtime evidence of `Dims` value inside function constraints. -- Similar to `KnownDim` or `KnownNat`, but for lists of numbers. -- --- Note, kind of the @Dimensions@ list is always @Nat@, restricted by +-- Note, kind of the @Dimensions@ list is usually @Nat@, restricted by -- @KnownDim@ being also @Nat@-indexed -- (it is impossible to create a unique @KnownDim (XN m)@ instance). -class Dimensions (ds :: [Nat]) where +-- Nevertheless, you can have @KnownDim (N n)@, which is useful in some cases. +class Dimensions ds where -- | Get dimensionality of a space at runtime, -- represented as a list of `Dim`. -- @@ -668,15 +795,51 @@ -- dims :: Dims ds -instance Dimensions '[] where + +instance Dimensions ('[] :: [k]) where dims = U {-# INLINE dims #-} -instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds) where +instance (KnownDim d, Dimensions ds) => Dimensions ((d ': ds) :: [k]) where dims = dim :* dims {-# INLINE dims #-} +-- | If you have @Dimensions ds@, then @ds@ can only be @[Nat]@ or a known type of +-- @[XNa]t@ (i.e. all @N n@). +-- This function assures the type checker that this is indeed the case. +withKnownXDims :: forall (ds :: [XNat]) (rep :: RuntimeRep) (r :: TYPE rep) + . Dimensions ds + => (( Dimensions (DimsBound ds), ExactDims ds + , All KnownDimType ds, FixedDims ds (DimsBound ds)) => r) + -> r +withKnownXDims f + | Dict <- unsafeEqTypes @ds @(Map 'N (DimsBound ds)) + = reifyDims @Nat @(DimsBound ds) dsN + (withBareConstraint (dictToBare (inferExactFixedDims @ds dsN)) (\_ -> f) ()) + where + dsN :: Dims (DimsBound ds) + dsN = unsafeCastTL (dims @ds) +{-# INLINE withKnownXDims #-} +-- | Minimal or exact bound of @Dims@. +-- This is a plural form of `DimBound`. +type family DimsBound (ds :: [k]) :: [Nat] where + DimsBound (ns :: [Nat]) = ns + DimsBound ('[] :: [XNat]) = '[] + DimsBound (n ': ns) = DimBound n ': DimsBound ns + +-- | Every dim in a list is either @Nat@, or a known @XNat@ (i.e. @N n@). +type family ExactDims (d :: [k]) :: Constraint where + ExactDims (_ :: [Nat]) = () + ExactDims (xs :: [XNat]) = xs ~ Map 'N (DimsBound xs) + +-- | This is a technical "helper" family that allows to infer BoundedDims +-- constraint on a tail of a list via the superclass relation. +type family BoundedDimsTail (ds :: [k]) where + BoundedDimsTail '[] = UnreachableConstraint (BoundedDims (Tail '[])) + "BoundDimsTail '[] -- BoundedDims (Tail '[])" + BoundedDimsTail (_ ': ns) = BoundedDims ns + -- | Get a minimal or exact bound of @Dims@. -- -- This is a plural form of `BoundedDim`. @@ -685,82 +848,105 @@ -- -- * It is defined for both @[Nat]@ and @[XNat]@; -- * Instance of @Dimensions ds@ always implies @BoundedDims ds@. -class KnownDimKind k => BoundedDims (ds :: [k]) where - -- | Minimal or exact bound of @Dims@. - -- This is a plural form of `DimBound`. - type family DimsBound ds :: [Nat] +-- +-- @BoundedDims@ is a powerful inference tool: +-- its instances do not require much, but it provides a lot via the superclass +-- constraints. +class ( KnownDimKind (KindOfEl ds), All BoundedDim ds, RepresentableList ds + , Dimensions (DimsBound ds), BoundedDimsTail ds) + => BoundedDims ds where -- | Plural form for `dimBound` dimsBound :: Dims (DimsBound ds) -- | Plural form for `constrainDim`. -- -- Given a @Dims ys@, test if its runtime value satisfies constraints imposed by - -- @BoundedDims ds@, and returns it back coerced to @Dims ds@ on success. + -- @BoundedDims xs@, and returns it back coerced to @Dims xs@ on success. -- -- This function allows to guess safely individual dimension values, -- as well as the length of the dimension list. - -- It returns @Nothing@ if @ds@ and @xds@ have different length or if any - -- of the values in @ys@ are less than the corresponding values of @ds@. - constrainDims :: forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds) - -- | BoundedDims means every element dim is @BoundedDim@ and also - -- the length of a dim list is known. - -- - -- Enforcing this as a superclass would complicate instance relations, - -- so it is better to provide these dictionaries on-demand. - inferAllBoundedDims :: Dict (All BoundedDim ds, RepresentableList ds) + -- It returns @Nothing@ if @xs@ and @ys@ have different length or if any + -- of the values in @ys@ are less than the corresponding values of @xs@. + constrainDims :: forall ys . Dims ys -> Maybe (Dims ds) +-- | Minimal runtime @Dims ds@ value that satifies the constraints imposed by +-- the type signature of @Dims ds@ +-- (this is the exact @dims@ for @Nat@s and the minimal bound for @XNat@s). +minimalDims :: forall ds . BoundedDims ds => Dims ds +minimalDims = unsafeCastTL (dimsBound @ds) -instance Dimensions ns => BoundedDims (ns :: [Nat]) where - type DimsBound ns = ns - dimsBound = dims @ns - {-# INLINE dimsBound #-} - constrainDims ys - | listDims ys == listDims (dims @ns) - = Just (unsafeCoerce# ys) + +{-# ANN defineBoundedDims ClassDict #-} +defineBoundedDims :: + forall (k :: Type) (ds :: [k]) + . ( KnownDimKind (KindOfEl ds), All BoundedDim ds, RepresentableList ds + , Dimensions (DimsBound ds), BoundedDimsTail ds) + => Dims (DimsBound ds) + -> (forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds)) + -> Dict (BoundedDims ds) +defineBoundedDims = defineBoundedDims + +-- instance {-# INCOHERENT #-} Dimensions ns => BoundedDims (ns :: [k]) +{-# ANN incohInstBoundedDims (ToInstance Incoherent) #-} +incohInstBoundedDims :: + forall (k :: Type) (ds :: [k]) + . (Dimensions ds, KnownDimKind k) => Dict (BoundedDims ds) +incohInstBoundedDims + = incohInstBoundedDims' @k @ds dims (inferAllBoundedDims ds) + where + ds = dims @ds + +incohInstBoundedDims' :: + forall (k :: Type) (ds :: [k]) + . KnownDimKind k + => Dims ds + -> Dict (All BoundedDim ds, RepresentableList ds) + -> Dict (BoundedDims ds) +incohInstBoundedDims' ds Dict = case dimsBound' of + Dims -> case ds of + U -> defineBoundedDims dimsBound' constrainDims' + _ :* ds' + | _ :* TypeList <- tList @ds + , Dict <- incohInstBoundedDims' ds' Dict + -> defineBoundedDims dimsBound' constrainDims' + _ -> error "incohInstBoundedDims': impossible pattern" + where + dimsBound' :: Dims (DimsBound ds) + dimsBound' = unsafeCastTL ds + constrainDims' :: forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds) + constrainDims' ys + | listDims ys == listDims dimsBound' + = Just (unsafeCastTL ys) | otherwise = Nothing - {-# INLINE constrainDims #-} - inferAllBoundedDims = go (dims @ns) - where - go :: forall (ds :: [Nat]) . Dims ds - -> Dict (All BoundedDim ds, RepresentableList ds) - go U = Dict - go (D :* ds) - | Dict <- go ds = Dict +#if defined(__HADDOCK__) || defined(__HADDOCK_VERSION__) +instance Dimensions ns => BoundedDims (ns :: [Nat]) where + dimsBound = undefined + constrainDims = undefined +#endif + + instance BoundedDims ('[] :: [XNat]) where - type DimsBound '[] = '[] dimsBound = U - constrainDims = const $ Just U - inferAllBoundedDims = Dict + constrainDims U = Just U + constrainDims (_ :* _) = Nothing instance (BoundedDim n, BoundedDims ns) => BoundedDims ((n ': ns) :: [XNat]) where - type DimsBound (n ': ns) = DimBound n ': DimsBound ns - dimsBound = dimBound @XNat @n :* dimsBound @XNat @ns + dimsBound = dimBound @n :* dimsBound @ns constrainDims U = Nothing constrainDims (y :* ys) = (:*) <$> constrainDim y <*> constrainDims ys - inferAllBoundedDims = case inferAllBoundedDims @XNat @ns of Dict -> Dict --- | Minimal runtime @Dims ds@ value that satifies the constraints imposed by --- the type signature of @Dims ds@. -minDims :: forall (k :: Type) (ds :: [k]) - . BoundedDims ds => Dims ds -minDims = unsafeCoerce# (dimsBound @k @ds) - - - -- | Construct a @Dims ds@ if there is an instance of @Typeable ds@ around. typeableDims :: forall (ds :: [Nat]) . Typeable ds => Dims ds typeableDims = case typeRep @ds of App (App _ (tx :: TypeRep (n :: k1))) (txs :: TypeRep (ns :: k2)) - -> case unsafeCoerceDict @(Nat ~ Nat, [Nat] ~ [Nat]) - @(Nat ~ k1 , [Nat] ~ k2) Dict of - Dict -> case unsafeCoerceDict @(ds ~ ds) - @(ds ~ (n ': ns)) Dict of - Dict -> withTypeable tx (typeableDim @n) - :* withTypeable txs (typeableDims @ns) + | Dict <- unsafeEqTypes @k1 @Nat + , Dict <- unsafeEqTypes @k2 @[Nat] + , Dict <- unsafeEqTypes @ds @(n ': ns) + -> withTypeable tx (typeableDim @n) :* withTypeable txs (typeableDims @ns) Con _ - -> unsafeCoerce# U + -> unsafeCoerce U r -> error ("typeableDims -- impossible typeRep: " ++ show r) {-# INLINE typeableDims #-} @@ -773,49 +959,37 @@ = Dict --- | Convert `Dims xs` to a plain haskell list of dimension sizes @O(1)@. +-- | @O(1)@ Convert @Dims xs@ to a plain haskell list of dimension sizes. -- -- Note, for @XNat@-indexed list it returns actual content dimensions, -- not the constraint numbers (@XN m@) -listDims :: forall (k :: Type) (xs :: [k]) . Dims xs -> [Word] -listDims = unsafeCoerce# +listDims :: forall xs . 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# +someDimsVal = SomeDims . unsafeCoerce {-# INLINE someDimsVal #-} -- | Product of all dimension sizes @O(Length xs)@. -totalDim :: forall (k :: Type) (xs :: [k]) . Dims xs -> Word +totalDim :: forall xs . Dims xs -> Word totalDim = product . listDims {-# INLINE totalDim #-} -- | Product of all dimension sizes @O(Length xs)@. -totalDim' :: forall (xs :: [Nat]) . Dimensions xs => Word +totalDim' :: forall xs . Dimensions xs => Word totalDim' = totalDim (dims @xs) {-# INLINE totalDim' #-} --- | Get XNat-indexed dims given their fixed counterpart. -xDims :: forall (xns :: [XNat]) (ns :: [Nat]) - . FixedDims xns ns => Dims ns -> Dims xns -xDims = unsafeCoerce# -{-# INLINE xDims #-} - --- | Get XNat-indexed dims given their fixed counterpart. -xDims' :: forall (xns :: [XNat]) (ns :: [Nat]) - . (FixedDims xns ns, Dimensions ns) => Dims xns -xDims' = xDims @xns (dims @ns) -{-# INLINE xDims' #-} - -- | Drop the given prefix from a Dims list. -- It returns Nothing if the list did not start with the prefix given, -- or Just the Dims after the prefix, if it does. stripPrefixDims :: forall (xs :: [Nat]) (ys :: [Nat]) . Dims xs -> Dims ys -> Maybe (Dims (StripPrefix xs ys)) -stripPrefixDims = unsafeCoerce# (Data.List.stripPrefix :: [Word] -> [Word] -> Maybe [Word]) +stripPrefixDims = unsafeCoerce (Data.List.stripPrefix :: [Word] -> [Word] -> Maybe [Word]) {-# INLINE stripPrefixDims #-} -- | Drop the given suffix from a Dims list. @@ -824,7 +998,7 @@ stripSuffixDims :: forall (xs :: [Nat]) (ys :: [Nat]) . Dims xs -> Dims ys -> Maybe (Dims (StripSuffix xs ys)) -stripSuffixDims = unsafeCoerce# stripSuf +stripSuffixDims = unsafeCoerce stripSuf where stripSuf :: [Word] -> [Word] -> Maybe [Word] stripSuf suf whole = go pref whole @@ -844,7 +1018,7 @@ . Dims as -> Dims bs -> Maybe (Dict (as ~ bs)) sameDims as bs | listDims as == listDims bs - = Just (unsafeCoerceDict @(as ~ as) Dict) + = Just (unsafeEqTypes @as @bs) | otherwise = Nothing {-# INLINE sameDims #-} @@ -857,32 +1031,16 @@ {-# INLINE sameDims' #-} --- | Similar to `const` or `asProxyTypeOf`; --- to be used on such implicit functions as `dim`, `dimMax`, etc. -inSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] -> Type) (q :: [k] -> Type) +-- | Restricted version of `const`, similar to `asProxyTypeOf`; +-- to be used on such implicit functions as `dims`, `dimsBound` etc. +inSpaceOf :: forall ds p q . p ds -> q ds -> p ds inSpaceOf = const {-# INLINE inSpaceOf #-} --- | Similar to `asProxyTypeOf`, --- Give a hint to type checker to fix the type of a function argument. -asSpaceOf :: forall (k :: Type) (ds :: [k]) - (p :: [k] -> Type) (q :: [k] -> Type) (r :: Type) - . p ds -> (q ds -> r) -> (q ds -> r) -asSpaceOf = const id -{-# INLINE asSpaceOf #-} - --- | 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. +-- This is a link connecting the two types of type-level dims; +-- you often need it to convert @Dims@, @Idxs@, and data. type family FixedDims (xns::[XNat]) (ns :: [Nat]) :: Constraint where FixedDims '[] ns = (ns ~ '[]) FixedDims (xn ': xns) ns @@ -890,11 +1048,54 @@ , FixedDim xn (Head ns) , FixedDims xns (Tail ns)) --- | Know the structure of each dimension -type KnownXNatTypes xns = All KnownXNatType xns - +-- | Try to instantiate the `FixedDims` constraint given two @Dims@ lists. +-- +-- The first @Dims@ is assumed to be the output of @minimalDims@, +-- i.e. @listDims xns == toList (listDims xns)@. +-- +-- If you input a list that is not equal to its type-level @DimsBound@, +-- you will just have a lower chance to get @Just Dict@ result. +inferFixedDims :: forall (xns :: [XNat]) (ns :: [Nat]) + . All KnownDimType xns + => Dims xns -> Dims ns -> Maybe (Dict (FixedDims xns ns)) +inferFixedDims U U = Just Dict +inferFixedDims (Dx (a :: Dim n) :* xns) (b :* ns) + | Dict <- unsafeEqTypes @n @(DimBound (Head xns)) + , Just Dict <- lessOrEqDim a b + , Just Dict <- inferFixedDims xns ns + = Just Dict +inferFixedDims (Dn a :* xns) (b :* ns) + | Just Dict <- sameDim a b + , Just Dict <- inferFixedDims xns ns + = Just Dict +inferFixedDims _ _ = Nothing +-- | A very unsafe function that bypasses all type-level checks and constructs +-- the evidence from nothing. +unsafeInferFixedDims :: forall (xns :: [XNat]) (ns :: [Nat]) + . Dims ns -> Dict (FixedDims xns ns) +unsafeInferFixedDims U + | Dict <- unsafeEqTypes @xns @'[] = Dict +unsafeInferFixedDims ((D :: Dim n) :* ns) + {- + Very unsafe operation. + I rely here on the fact that FixedDim xn n has the same + runtime rep as a single type equality. + If that changes, then the code is broke. + -} + | Dict <- unsafeEqTypes @xns @(N n ': Tail xns) + , Dict <- unsafeInferFixedDims @(Tail xns) ns = Dict +{-# INLINE unsafeInferFixedDims #-} +-- | Infer `FixedDims` if you know that all of dims are exact (@d ~ N n@). +-- This function is totally safe and faithful. +inferExactFixedDims :: forall (ds :: [XNat]) . ExactDims ds + => Dims (DimsBound ds) + -> Dict (All KnownDimType ds, FixedDims ds (DimsBound ds)) +inferExactFixedDims U = Dict +inferExactFixedDims (_ :* ns) + | Dict <- inferExactFixedDims @(Tail ds) ns = Dict +{-# INLINE inferExactFixedDims #-} instance Typeable d => Data (Dim (d :: Nat)) where gfoldl _ = id @@ -934,9 +1135,9 @@ {-# INLINE (/=) #-} instance Eq (Dims (ds :: [XNat])) where - (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool) + (==) = unsafeCoerce ((==) :: [Word] -> [Word] -> Bool) {-# INLINE (==) #-} - (/=) = unsafeCoerce# ((/=) :: [Word] -> [Word] -> Bool) + (/=) = unsafeCoerce ((/=) :: [Word] -> [Word] -> Bool) {-# INLINE (/=) #-} instance Eq SomeDims where @@ -958,7 +1159,7 @@ {-# INLINE compare #-} instance Ord (Dims (ds :: [XNat])) where - compare = unsafeCoerce# (compare :: [Word] -> [Word] -> Ordering) + compare = unsafeCoerce (compare :: [Word] -> [Word] -> Ordering) {-# INLINE compare #-} instance Ord SomeDims where @@ -970,7 +1171,7 @@ {-# INLINE showsPrec #-} instance Show (Dims (xs :: [k])) where - showsPrec = typedListShowsPrec @k @Dim @xs showsPrec + showsPrec = typedListShowsPrec @Dim @xs showsPrec instance Show SomeDims where showsPrec p (SomeDims ds) @@ -981,22 +1182,21 @@ readPrec = Read.lexP >>= \case Read.Ident ('D':s) | Just d <- Read.readMaybe s - >>= constrainDim @k @x @XNat @(XN 0) . DimSing + >>= constrainDim @x @(XN 0) . DimSing -> return d _ -> Read.pfail readList = Read.readListDefault readListPrec = Read.readListPrecDefault instance BoundedDims xs => Read (Dims (xs :: [k])) where - readPrec = case inferAllBoundedDims @k @xs of - Dict -> typedListReadPrec @k @BoundedDim ":*" Read.readPrec (tList @k @xs) + readPrec = typedListReadPrec @BoundedDim ":*" Read.readPrec (tList @xs) readList = Read.readListDefault readListPrec = Read.readListPrecDefault instance Read SomeDims where readPrec = Read.parens . Read.prec 10 $ do Read.lift . Read.expect $ Read.Ident "SomeDims" - withTypedListReadPrec @Nat @Dim @SomeDims + withTypedListReadPrec @Dim @SomeDims (\g -> (\(Dx d) -> g d) <$> Read.readPrec @(Dim (XN 0))) SomeDims @@ -1006,72 +1206,79 @@ -- 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 :: Type) (d :: Nat) . Dim d -> (KnownDim d => r) -> r -reifyDim d k = unsafeCoerce# (MagicDim k :: MagicDim d r) d +reifyDim :: forall (k :: Type) (d :: k) (rep :: RuntimeRep) (r :: TYPE rep) + . Dim d -> (KnownDim d => r) -> r +reifyDim d k = unsafeCoerce (MagicDim k :: MagicDim d r) d {-# INLINE reifyDim #-} -newtype MagicDim (d :: Nat) (r :: Type) = MagicDim (KnownDim d => r) +newtype MagicDim (d :: k) (r :: TYPE rep) = MagicDim (KnownDim d => r) reifyNat :: forall (r :: Type) (d :: Nat) . Natural -> (KnownNat d => r) -> r -reifyNat d k = unsafeCoerce# (MagicNat k :: MagicNat d r) d +reifyNat d k = unsafeCoerce (MagicNat k :: MagicNat d r) d {-# INLINE reifyNat #-} newtype MagicNat (d :: Nat) (r :: Type) = MagicNat (KnownNat d => r) -dimEv :: forall (d :: Nat) . Dim d -> Dict (KnownDim d) -dimEv d = reifyDim d Dict -{-# INLINE dimEv #-} - -reifyDims :: forall (r :: Type) (ds :: [Nat]) . Dims ds -> (Dimensions ds => r) -> r -reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds +reifyDims :: forall (k :: Type) (ds :: [k]) (rep :: RuntimeRep) (r :: TYPE rep) + . Dims ds -> (Dimensions ds => r) -> r +reifyDims ds k = unsafeCoerce (MagicDims k :: MagicDims ds r) ds {-# INLINE reifyDims #-} -newtype MagicDims (ds :: [Nat]) (r :: Type) = MagicDims (Dimensions ds => r) - -dimsEv :: forall (ds :: [Nat]) . Dims ds -> Dict (Dimensions ds) -dimsEv ds = reifyDims ds Dict -{-# INLINE dimsEv #-} +newtype MagicDims (ds :: [k]) (r :: TYPE rep) = MagicDims (Dimensions ds => r) -data PatXDim (xn :: XNat) where - PatN :: KnownDim n => Dim n -> PatXDim ('N n) - PatXN :: (KnownDim n, m <= n) => Dim n -> PatXDim ('XN m) +data PatDim (d :: k) where + PatNat :: KnownDim n => PatDim (n :: Nat) + PatXNatN :: Dim n -> PatDim (N n) + PatXNatX :: (m <= n) => Dim n -> PatDim (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) +patDim :: forall (k :: Type) (d :: k) . DimType d -> Dim d -> PatDim d +patDim DimTNat d = reifyDim d PatNat +patDim DimTXNatN d = PatXNatN (coerce d) +patDim DimTXNatX d = f (coerce d) d where - dd = DimSing @Nat @_ k - f :: forall (d :: Nat) (m :: Nat) - . KnownDim d => Dim d -> Dim ('XN m) -> PatXDim ('XN m) - f d = case unsafeCoerceDict @(m <= m) @(m <= d) Dict of - Dict -> const (PatXN d) -{-# INLINE dimXNEv #-} - -data PatXDims (xns :: [XNat]) - = forall (ns :: [Nat]) - . (FixedDims xns ns, Dimensions ns) => PatXDims (Dims ns) + f :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim (XN m) -> PatDim (XN m) + f n = case unsafeCoerceDict @(m <= m) @(m <= n) Dict of + Dict -> const (PatXNatX n) +{-# INLINE patDim #-} -patXDims :: forall (xns :: [XNat]) - . 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) -{-# INLINE patXDims #-} +data PatDims (ds :: [k]) where + PatNats :: Dimensions ds => PatDims (ds :: [Nat]) + PatXNats :: FixedDims ds ns => Dims ns -> PatDims (ds :: [XNat]) -data PatAsXDims (ns :: [Nat]) - = (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns)) - => PatAsXDims (Dims (AsXDims ns)) +patDims :: forall (k :: Type) (ds :: [k]) . DimKind k -> Dims ds -> PatDims ds +patDims DimKNat ds = reifyDims ds PatNats +patDims DimKXNat ds = withBareConstraint + (dictToBare (unsafeInferFixedDims @ds ds')) (PatXNats ds') + where + ds' = unsafeCastTL ds -- convert to *some* [Nat] +{-# INLINE patDims #-} -patAsXDims :: forall (ns :: [Nat]) . Dims ns -> PatAsXDims ns -patAsXDims U = PatAsXDims U -patAsXDims (n@D :* ns) = case patAsXDims ns of - PatAsXDims xns -> PatAsXDims (Dn n :* xns) -{-# INLINE patAsXDims #-} +{- +I know that Dimensions can be either Nats or N-known XNats. +Therefore, inside the worker function I can (un)safely pick up a BoundedDim +instance for (d ~ N n) + -} +inferAllBoundedDims :: forall (k :: Type) (ds :: [k]) + . (Dimensions ds, KnownDimKind k) + => Dims ds -> Dict (All BoundedDim ds, RepresentableList ds) +inferAllBoundedDims = go + where + reifyBoundedDim :: forall (d :: k) . Dim d -> Dict (BoundedDim d) + reifyBoundedDim = case dimKind @k of + DimKNat -> \d -> reifyDim d Dict + DimKXNat + | Dict <- unsafeEqTypes @d @(N (DimBound d)) + -> \d -> reifyDim (coerce d :: Dim (DimBound d)) Dict + go :: forall (xs :: [k]) . Dims xs + -> Dict (All BoundedDim xs, RepresentableList xs) + go U = Dict + go (d :* ds) + | Dict <- reifyBoundedDim d + , Dict <- go ds = Dict +{-# INLINE inferAllBoundedDims #-} data PatKDims (ns :: [Nat]) - = (All KnownDim ns, All BoundedDim ns, RepresentableList ns, Dimensions ns) => PatKDims + = ( All KnownDim ns, All BoundedDim ns + , RepresentableList ns, Dimensions ns) + => PatKDims patKDims :: forall (ns :: [Nat]) . Dims ns -> PatKDims ns patKDims U = PatKDims @@ -1081,4 +1288,7 @@ unsafeCoerceDict :: forall (a :: Constraint) (b :: Constraint) . Dict a -> Dict b -unsafeCoerceDict = unsafeCoerce# +unsafeCoerceDict = unsafeCoerce + +unsafeCastTL :: TypedList f (xs :: [k]) -> TypedList g (ys :: [l]) +unsafeCastTL = unsafeCoerce diff --git a/src/Numeric/Dimensions/Dim.hs-boot b/src/Numeric/Dimensions/Dim.hs-boot --- a/src/Numeric/Dimensions/Dim.hs-boot +++ b/src/Numeric/Dimensions/Dim.hs-boot @@ -5,9 +5,8 @@ {-# LANGUAGE TypeOperators #-} -- This module recursively depends on Numeric.TypedList. -- I thought hs-boot is better than orphan instances. -module Numeric.Dimensions.Dim ( Dim, Nat, dimVal, minusDimM ) where -import Data.Kind (Type) +module Numeric.Dimensions.Dim ( Dim, dimVal, minusDimM ) where import Data.Type.Lits (type (-), Nat) newtype Dim (x :: k) = DimSing Word -dimVal :: forall (k :: Type) (x :: k) . Dim (x :: k) -> Word +dimVal :: forall x . Dim x -> Word minusDimM :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Maybe (Dim (n - m)) diff --git a/src/Numeric/Dimensions/Idx.hs b/src/Numeric/Dimensions/Idx.hs --- a/src/Numeric/Dimensions/Idx.hs +++ b/src/Numeric/Dimensions/Idx.hs @@ -17,7 +17,12 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE UnboxedTuples #-} {-# LANGUAGE UndecidableInstances #-} - +{-# LANGUAGE ViewPatterns #-} +#if defined(__HADDOCK__) || defined(__HADDOCK_VERSION__) +{-# LANGUAGE StandaloneDeriving #-} +#else +{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-} +#endif ----------------------------------------------------------------------------- -- | -- Module : Numeric.Dimensions.Idx @@ -32,86 +37,144 @@ -- is i = i1*n1*n2*...*n(k-1) + ... + i(k-2)*n1*n2 + i(k-1)*n1 + ik -- This corresponds to row-first layout of matrices and multidimenional arrays. -- +-- == Type safety +-- +-- Same as `Dim` and `Dims`, `Idx` and `Idxs` defined in this module incorporate +-- two different indexing mechanics. +-- Both of them can be specified with exact @Nat@ values +-- (when @d :: Nat@ or @d ~ N n@), +-- or with lower bound values (i.e. @d ~ XN m@). +-- In the former case, the @Idx@/@Idxs@ type itself guarantees that the value +-- inside is within the @Dim@/@Dims@ bounds. +-- In the latter case, @Idx@/@Idxs@ can contain any values of type @Word@. +-- In other words: +-- +-- * @(d :: Nat) || (d ~ N n) =>@ using @Idx d@ to index data is always safe, +-- but creating an index using unsafe functions can yield an `OutOfDimBounds` +-- exception at runtime. +-- * @(d ~ XN m) =>@ using @Idx d@ to index data can result in an `OutOfDimBounds` +-- exception, but you can safely manipulate the index itself +-- using familiar interfaces, such as @Enum@, @Num@, etc; as if @Idx d@ +-- was a plain synonym to @Word@. +-- ----------------------------------------------------------------------------- module Numeric.Dimensions.Idx ( -- * Data types Idx (Idx), Idxs - , idxFromWord, unsafeIdxFromWord, idxToWord + , idxFromWord, idxToWord , listIdxs, idxsFromWords + , liftIdxs, unliftIdxs, unsafeUnliftIdxs + , TypedList ( XIdxs, U, (:*), Empty, Cons, Snoc, Reverse) + -- * Checking the index bounds + , OutOfDimBounds (..), outOfDimBounds, outOfDimBoundsNoCallStack +#if !defined(__HADDOCK__) && !defined(__HADDOCK_VERSION__) + , xnatNInstEnumIdx, xnatXInstEnumIdx, incohInstEnumIdx + , xnatNInstNumIdx, xnatXInstNumIdx, incohInstNumIdx + , instRealIdx, instIntegralIdx +#endif ) where import Data.Coerce -import Data.Constraint (Dict (..)) import Data.Data (Data) import Foreign.Storable (Storable) import GHC.Enum import GHC.Generics (Generic) import qualified Text.Read as P +import Unsafe.Coerce +import GHC.Exception +import GHC.Stack #ifdef UNSAFE_INDICES -import GHC.Base (Int (..), Type, Word (..), int2Word#, unsafeCoerce#, word2Int#) +import GHC.Base (Int (..), Type, Word (..), int2Word#, word2Int#) #else import GHC.Base (Int (..), Type, Word (..), int2Word#, maxInt, plusWord2#, - timesWord2#, unsafeCoerce#, word2Int#) + timesWord2#, word2Int#) #endif +#if !defined(__HADDOCK__) && !defined(__HADDOCK_VERSION__) +import Data.Constraint +import Data.Constraint.Bare +import Data.Constraint.Deriving +#endif + import Numeric.Dimensions.Dim import Numeric.TypedList (typedListReadPrec, typedListShowsPrec) --- | This type is used to index a single dimension; --- the range of indices is from @0@ to @n-1@. --- -newtype Idx (n :: k) = Idx' Word - deriving ( Data, Generic, Integral, Real, Storable, Eq, Ord ) +{- | This type is used to index a single dimension. + * @(k ~ Nat) =>@ the range of indices is from @0@ to @d-1@. + * @(d ~ N n) =>@ the range of indices is from @0@ to @n-1@. + * @(d ~ XN m) =>@ the range of indices is from @0@ to @maxBound :: Word@. --- | Convert between `Word` and `Idx`. --- --- If the word is outside of the bounds, fails with an error --- (unless @unsafeindices@ flag is turned on). --- -pattern Idx :: forall (k :: Type) (n :: k) . BoundedDim n => Word -> Idx n +That is, using @Idx (n :: Nat)@ or @Idx (N n)@ is guaranteed to be safe by the +type system. +But an index of type @Idx (XN m)@ can have any value, and using it may yield +an `OutOfDimBounds` exception -- just the same as a generic @index@ function that +takes a plain @Int@ or @Word@ as an argument. +Thus, if you have data indexed by @(XN m)@, I would suggest to use @lookup@-like +functions that return @Maybe@. You're warned. + + -} +newtype Idx (d :: k) = Idx' Word + deriving ( Data, Generic, Storable, Eq, Ord ) + + +{- | Convert between `Word` and `Idx`. + +Converting from `Idx` to `Word` is always safe. + +Converting from `Word` to `Idx` generally is unsafe: + + * @(k ~ Nat) =>@ if @w >= d@, it fails with an `OutOfDimBounds` exception. + * @(d ~ N n) =>@ if @w >= n@, it fails with an `OutOfDimBounds` exception. + * @(d ~ XN m) =>@ the constructor always succeeds, but using the result for + indexing may fail with an `OutOfDimBounds` exception later. + +If @unsafeindices@ flag it turned on, this function always succeeds. + -} +pattern Idx :: forall d . BoundedDim d => Word -> Idx d pattern Idx w <- Idx' w where Idx = unsafeIdxFromWord {-# COMPLETE Idx #-} -- | Type-level dimensional indexing with arbitrary Word values inside. --- Most of the operations on it require `Dimensions` constraint, +-- Most of the operations on it require `Dimensions` or `BoundedDims` constraint, -- because the @Idxs@ itself does not store info about dimension bounds. -type Idxs (xs :: [k]) = TypedList Idx xs +type Idxs = (TypedList Idx :: [k] -> Type) --- | Convert an arbitrary Word to @Idx@. --- --- If the word is outside of the bounds, fails with an error --- (unless @unsafeindices@ flag is turned on). --- + unsafeIdxFromWord :: forall (k :: Type) (d :: k) . BoundedDim d => Word -> Idx d #ifdef UNSAFE_INDICES unsafeIdxFromWord = coerce #else unsafeIdxFromWord w + | DimTXNatX <- dimType @d + = coerce w | w < d = coerce w - | otherwise = errorWithoutStackTrace - $ "idxFromWord{" ++ showIdxType @k @d ++ "}: word " - ++ show w ++ " is outside of index bounds." + | otherwise = outOfDimBoundsNoCallStack "unsafeIdxFromWord" w d Nothing Nothing where - d = dimVal (dimBound @k @d) + d = dimVal (dimBound @d) #endif {-# INLINE unsafeIdxFromWord #-} -- | Convert an arbitrary Word to @Idx@. -idxFromWord :: forall (k :: Type) (d :: k) . BoundedDim d => Word -> Maybe (Idx d) +-- This is a safe alternative to the pattern @Idx@. +-- +-- Note, when @(d ~ XN m)@, it returns @Nothing@ if @w >= m@. +-- Thus, the resulting index is always safe to use +-- (but you cannot index stuff beyond @DimBound d@ this way). +idxFromWord :: forall d . BoundedDim d => Word -> Maybe (Idx d) idxFromWord w - | w < dimVal (dimBound @k @d) = Just (coerce w) - | otherwise = Nothing + | w < dimVal (dimBound @d) = Just (coerce w) + | otherwise = Nothing {-# INLINE idxFromWord #-} -- | Get the value of an @Idx@. -idxToWord :: forall (k :: Type) (d :: k) . Idx d -> Word +idxToWord :: forall d . Idx d -> Word idxToWord = coerce {-# INLINE idxToWord #-} @@ -120,13 +183,18 @@ fromIntegral = idxToWord #-} -listIdxs :: forall (k :: Type) (xs :: [k]) . Idxs xs -> [Word] -listIdxs = unsafeCoerce# +-- | /O(1)/ Convert @Idxs xs@ to a plain list of words. +listIdxs :: forall ds . Idxs ds -> [Word] +listIdxs = unsafeCoerce {-# INLINE listIdxs #-} -idxsFromWords :: forall (k :: Type) (xs :: [k]) - . BoundedDims xs => [Word] -> Maybe (Idxs xs) -idxsFromWords = unsafeCoerce# . go (listDims (dimsBound @k @xs)) +-- | /O(n)/ Convert a plain list of words into an @Idxs@, while checking +-- the index bounds. +-- +-- Same as with `idxFromWord`, it is always safe to use the resulting index, +-- but you cannot index stuff outside of the @DimsBound ds@ this way. +idxsFromWords :: forall ds . BoundedDims ds => [Word] -> Maybe (Idxs ds) +idxsFromWords = unsafeCoerce . go (listDims (dimsBound @ds)) where go :: [Word] -> [Word] -> Maybe [Word] go [] [] = Just [] @@ -135,33 +203,87 @@ go _ _ = Nothing +-- | Transform between @Nat@-indexed and @XNat@-indexed @Idxs@. +-- +-- Note, this pattern is not a @COMPLETE@ match, because converting from @XNat@ +-- to @Nat@ indexed @Idxs@ may fail (see `unliftIdxs`). +pattern XIdxs :: forall (ds :: [XNat]) (ns :: [Nat]) + . (FixedDims ds ns, Dimensions ns) => Idxs ns -> Idxs ds +pattern XIdxs ns <- (unliftIdxs -> Just ns) + where + XIdxs = liftIdxs -instance BoundedDim x => Read (Idx (x :: k)) where +-- | @O(1)@ Coerce a @Nat@-indexed list of indices into a @XNat@-indexed one. +-- This function does not need any runtime checks and thus runs in constant time. +liftIdxs :: forall (ds :: [XNat]) (ns :: [Nat]) + . FixedDims ds ns => Idxs ns -> Idxs ds +liftIdxs = unsafeCoerce +{-# INLINE liftIdxs #-} + +-- | @O(n)@ Coerce a @XNat@-indexed list of indices into a @Nat@-indexed one. +-- This function checks if an index is within Dim bounds for every dimension. +unliftIdxs :: forall (ds :: [XNat]) (ns :: [Nat]) + . (FixedDims ds ns, Dimensions ns) => Idxs ds -> Maybe (Idxs ns) +unliftIdxs U = Just U +unliftIdxs (Idx' i :* is) + | d :* Dims <- dims @ns + , i < dimVal d = (Idx' i :*) <$> unliftIdxs is + | otherwise = Nothing +{-# INLINE unliftIdxs #-} + +-- | Coerce a @XNat@-indexed list of indices into a @Nat@-indexed one. +-- Can throw an `OutOfDimBounds` exception unless @unsafeindices@ flag is active. +unsafeUnliftIdxs :: forall (ds :: [XNat]) (ns :: [Nat]) + . (FixedDims ds ns, Dimensions ns) => Idxs ds -> Idxs ns +#ifdef UNSAFE_INDICES +unsafeUnliftIdxs = unsafeCoerce +#else +unsafeUnliftIdxs is' = unsafeCoerce (zipWith f is ds) + where + f i d | i < d = i + | otherwise = err i d + is = listIdxs is' + ds = listDims (dims @ns) + err i d = outOfDimBoundsNoCallStack + "unsafeUnliftIdxs" i d Nothing (Just (ds, is)) +#endif +{-# INLINE unsafeUnliftIdxs #-} + + +instance BoundedDim d => Read (Idx d) where readPrec = do w <- P.readPrec - if w < dimVal (dimBound @k @x) - then return (Idx' w) - else P.pfail + case dimType @d of + DimTXNatX -> return (Idx' w) + _ | w < dimVal (dimBound @d) + -> return (Idx' w) + | otherwise -> P.pfail readList = P.readListDefault readListPrec = P.readListPrecDefault -instance Show (Idx (x :: k)) where +instance Show (Idx d) where showsPrec = coerce (showsPrec :: Int -> Word -> ShowS) -instance BoundedDim n => Bounded (Idx (n :: k)) where - minBound = 0 +instance BoundedDim d => Bounded (Idx d) where + minBound = coerce (0 :: Word) {-# INLINE minBound #-} - maxBound = coerce (dimVal(dimBound @k @n) - 1) + {- | Note, @maxBound == Idx (dimVal (dimBound @d) - 1)@ + -- is defined in terms of @BoundedDim@. + Thus, when @(d ~ XN m)@, your actual index may be larger than @maxBound@. + -} + maxBound = coerce (dimVal (dimBound @d) - 1) {-# INLINE maxBound #-} -instance BoundedDim n => Enum (Idx (n :: k)) where +instance KnownDim n => Enum (Idx (n :: Nat)) where + #ifdef UNSAFE_INDICES succ = coerce ((+ 1) :: Word -> Word) #else succ x@(Idx' i) | x < maxBound = coerce (i + 1) - | otherwise = succError $ showIdxType @k @n + | otherwise = outOfDimBoundsNoCallStack + "Enum.succ{Idx}" (i + 1) (dimVal' @n) Nothing Nothing #endif {-# INLINE succ #-} @@ -170,7 +292,8 @@ #else pred x@(Idx' i) | x > minBound = coerce (i - 1) - | otherwise = predError $ showIdxType @k @n + | otherwise = outOfDimBoundsNoCallStack + "Enum.pred{Idx}" (-1 :: Int) (dimVal' @n) Nothing Nothing #endif {-# INLINE pred #-} @@ -179,9 +302,10 @@ #else toEnum i | i >= 0 && i' < d = coerce i' - | otherwise = toEnumError (showIdxType @k @n) i (0, d - 1) + | otherwise = outOfDimBoundsNoCallStack + "Enum.toEnum{Idx}" i d Nothing Nothing where - d = dimVal (dimBound @k @n) + d = dimVal' @n i' = fromIntegral i #endif {-# INLINE toEnum #-} @@ -191,19 +315,17 @@ #else fromEnum (Idx' x@(W# w#)) | x <= maxIntWord = I# (word2Int# w#) - | otherwise = fromEnumError (showIdxType @k @n) x + | otherwise = fromEnumError "Idx" x where maxIntWord = W# (case maxInt of I# i -> int2Word# i) #endif {-# INLINE fromEnum #-} - - enumFrom (Idx' n) - = coerce (enumFromTo n (dimVal (dimBound @k @n) - 1)) + enumFrom (Idx' n) = coerce (enumFromTo n (dimVal' @n - 1)) {-# INLINE enumFrom #-} enumFromThen (Idx' n0) (Idx' n1) = coerce (enumFromThenTo n0 n1 lim) where - lim = if n1 >= n0 then dimVal (dimBound @k @n) - 1 else 0 + lim = if n1 >= n0 then maxBound else minBound {-# INLINE enumFromThen #-} enumFromTo = coerce (enumFromTo :: Word -> Word -> [Word]) @@ -212,22 +334,22 @@ = coerce (enumFromThenTo :: Word -> Word -> Word -> [Word]) {-# INLINE enumFromThenTo #-} -instance BoundedDim n => Num (Idx (n :: k)) where +instance KnownDim n => Num (Idx (n :: Nat)) where + #ifdef UNSAFE_INDICES (+) = coerce ((+) :: Word -> Word -> Word) #else - (Idx' a@(W# a#)) + b@(Idx' (W# b#)) + (Idx' a@(W# a#)) + (Idx' b@(W# b#)) | ovf || r >= d - = errorWithoutStackTrace - $ "Num.(+){" ++ showIdxType @k @n ++ "}: sum of " - ++ show a ++ " and " ++ show b - ++ " is outside of index bounds." + = outOfDimBoundsNoCallStack + ("Num.(" ++ show a ++ " + " ++ show b ++ "){Idx}") + (toInteger a + toInteger b) d Nothing Nothing | otherwise = coerce r where (ovf, r) = case plusWord2# a# b# of (# r2#, r1# #) -> ( W# r2# > 0 , W# r1# ) - d = dimVal (dimBound @k @n) + d = dimVal' @n #endif {-# INLINE (+) #-} @@ -236,10 +358,9 @@ #else (Idx' a) - (Idx' b) | b > a - = errorWithoutStackTrace - $ "Num.(-){" ++ showIdxType @k @n ++ "}: difference of " - ++ show a ++ " and " ++ show b - ++ " is negative." + = outOfDimBoundsNoCallStack + ("Num.(" ++ show a ++ " - " ++ show b ++ "){Idx}") + (toInteger a - toInteger b) (dimVal' @n) Nothing Nothing | otherwise = coerce (a - b) #endif {-# INLINE (-) #-} @@ -247,22 +368,26 @@ #ifdef UNSAFE_INDICES (*) = coerce ((*) :: Word -> Word -> Word) #else - (Idx' a@(W# a#)) * b@(Idx' (W# b#)) + (Idx' a@(W# a#)) * (Idx' b@(W# b#)) | ovf || r >= d - = errorWithoutStackTrace - $ "Num.(*){" ++ showIdxType @k @n ++ "}: product of " - ++ show a ++ " and " ++ show b - ++ " is outside of index bounds." + = outOfDimBoundsNoCallStack + ("Num.(" ++ show a ++ " * " ++ show b ++ "){Idx}") + (toInteger a * toInteger b) d Nothing Nothing | otherwise = coerce r where (ovf, r) = case timesWord2# a# b# of (# r2#, r1# #) -> ( W# r2# > 0 , W# r1# ) - d = dimVal (dimBound @k @n) + d = dimVal' @n #endif {-# INLINE (*) #-} - negate = errorWithoutStackTrace - $ "Num.(*){" ++ showIdxType @k @n ++ "}: cannot negate index." +#ifdef UNSAFE_INDICES + negate = id +#else + negate (Idx' 0) = Idx' 0 + negate (Idx' i) = outOfDimBoundsNoCallStack + "Num.negate{Idx}" (- toInteger i) (dimVal' @n) Nothing Nothing +#endif {-# INLINE negate #-} abs = id {-# INLINE abs #-} @@ -273,20 +398,128 @@ fromInteger = coerce (fromInteger :: Integer -> Word) #else fromInteger i - | i >= 0 && i < d = Idx' $ fromInteger i - | otherwise = errorWithoutStackTrace - $ "Num.fromInteger{" ++ showIdxType @k @n ++ "}: integer " - ++ show i ++ " is outside of index bounds." + | i >= 0 && i < toInteger d + = Idx' (fromInteger i) + | otherwise = outOfDimBoundsNoCallStack + "Num.fromInteger{Idx}" i d Nothing Nothing where - d = toInteger $ dimVal (dimBound @k @n) + d = dimVal' @n #endif {-# INLINE fromInteger #-} +#if defined(__HADDOCK__) || defined(__HADDOCK_VERSION__) +{- | +Although @Enum (Idx d)@ requires @BoundedDim d@, it does not use @maxBound@ +when @(d ~ XN m)@. +You can use list comprehensions safely for known dims +(@(k ~ Nat)@ or @(d ~ N d)@), +but you may get an index larger than your struct to be indexed when @d ~ XN m@. + -} +deriving instance BoundedDim d => Enum (Idx d) +deriving instance BoundedDim d => Integral (Idx d) +deriving instance BoundedDim d => Real (Idx d) +{- | +Although @Num (Idx d)@ requires @BoundedDim d@, it does not use @maxBound@ +when @(d ~ XN m)@. +That is, if @(d ~ XN m)@ then @i = fromIntegral n@ always succeeds. + -} +deriving instance BoundedDim d => Num (Idx d) + +#else + +{-# ANN xnatNInstEnumIdx (ToInstance NoOverlap) #-} +xnatNInstEnumIdx :: + forall (n :: Nat) + . KnownDim n => Dict (Enum (Idx (N n))) +xnatNInstEnumIdx = unsafeCoerce (Dict @(Enum (Idx n))) + +{-# ANN xnatXInstEnumIdx (ToInstance NoOverlap) #-} +xnatXInstEnumIdx :: + forall (m :: Nat) + . Dict (Enum (Idx (XN m))) +xnatXInstEnumIdx = unsafeCoerce (Dict @(Enum Word)) + +{-# ANN incohInstEnumIdx (ToInstance Incoherent) #-} +incohInstEnumIdx :: + forall (k :: Type) (d :: k) + . BoundedDim d => Dict (Enum (Idx d)) +incohInstEnumIdx = case dimType @d of + DimTNat -> Dict + DimTXNatN -> xnatNInstEnumIdx + DimTXNatX -> xnatXInstEnumIdx + +{-# ANN xnatNInstNumIdx (ToInstance NoOverlap) #-} +xnatNInstNumIdx :: + forall (n :: Nat) + . KnownDim n => Dict (Num (Idx (N n))) +xnatNInstNumIdx = unsafeCoerce (Dict @(Num (Idx n))) + +{-# ANN xnatXInstNumIdx (ToInstance NoOverlap) #-} +xnatXInstNumIdx :: + forall (m :: Nat) + . Dict (Num (Idx (XN m))) +xnatXInstNumIdx = unsafeCoerce (Dict @(Num Word)) + +{-# ANN incohInstNumIdx (ToInstance Incoherent) #-} +incohInstNumIdx :: + forall (k :: Type) (d :: k) + . BoundedDim d => Dict (Num (Idx d)) +incohInstNumIdx = case dimType @d of + DimTNat -> Dict + DimTXNatN -> xnatNInstNumIdx + DimTXNatX -> xnatXInstNumIdx + +{-# ANN defineReal ClassDict #-} +defineReal :: + forall a + . (Num a, Ord a) + => (a -> Rational) -- toRational + -> Dict (Real a) +defineReal = defineReal + +{-# ANN instRealIdx (ToInstance NoOverlap) #-} +instRealIdx :: + forall (k :: Type) (d :: k) + . BoundedDim d => Dict (Real (Idx d)) +instRealIdx + = withBareConstraint (dictToBare (incohInstNumIdx @k @d)) + $ defineReal (coerce (toRational @Word)) + +{-# ANN defineIntegral ClassDict #-} +defineIntegral :: + forall a + . (Real a, Enum a) + => (a -> a -> a) -- quot + -> (a -> a -> a) -- rem + -> (a -> a -> a) -- div + -> (a -> a -> a) -- mod + -> (a -> a -> (a,a)) -- quotRem + -> (a -> a -> (a,a)) -- divMod + -> (a -> Integer) -- toInteger + -> Dict (Integral a) +defineIntegral = defineIntegral + +{-# ANN instIntegralIdx (ToInstance NoOverlap) #-} +instIntegralIdx :: + forall (k :: Type) (d :: k) + . BoundedDim d => Dict (Integral (Idx d)) +instIntegralIdx + = withBareConstraint (dictToBare (instRealIdx @k @d)) + $ withBareConstraint (dictToBare (incohInstEnumIdx @k @d)) + $ defineIntegral + (coerce (quot @Word)) (coerce (rem @Word)) + (coerce (div @Word)) (coerce (mod @Word)) + (coerce (quotRem @Word)) (coerce (divMod @Word)) + (coerce (toInteger @Word)) + + +#endif + instance Eq (Idxs (xs :: [k])) where - (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool) + (==) = unsafeCoerce ((==) :: [Word] -> [Word] -> Bool) {-# INLINE (==) #-} -- | Compare indices by their importance in lexicorgaphic order @@ -303,60 +536,43 @@ -- > sort == sortOn fromEnum -- instance Ord (Idxs (xs :: [k])) where - compare = unsafeCoerce# (compare :: [Word] -> [Word] -> Ordering) + compare = unsafeCoerce (compare :: [Word] -> [Word] -> Ordering) {-# INLINE compare #-} instance Show (Idxs (xs :: [k])) where - showsPrec = typedListShowsPrec @k @Idx @xs showsPrec + showsPrec = typedListShowsPrec @Idx @xs showsPrec instance BoundedDims xs => Read (Idxs (xs :: [k])) where - readPrec = case inferAllBoundedDims @k @xs of - Dict -> typedListReadPrec @k @BoundedDim ":*" P.readPrec (tList @k @xs) + readPrec = typedListReadPrec @BoundedDim ":*" P.readPrec (tList @xs) readList = P.readListDefault readListPrec = P.readListPrecDefault --- | With this instance we can slightly reduce indexing expressions, e.g. --- --- > x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U) --- -instance BoundedDim n => Num (Idxs '[(n :: k)]) 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 BoundedDims ds => Bounded (Idxs (ds :: [k])) where - maxBound = f (minDims @k @ds) + maxBound = f (minimalDims @ds) where f :: forall (ns :: [k]) . Dims ns -> Idxs ns f U = U f (d :* ds) = coerce (dimVal d - 1) :* f ds {-# INLINE maxBound #-} - minBound = f (minDims @k @ds) + minBound = f (minimalDims @ds) where f :: forall (ns :: [k]) . Dims ns -> Idxs ns f U = U f (_ :* ds) = Idx' 0 :* f ds {-# INLINE minBound #-} --- @ds@ must be @[Nat]@ for @Enum (Idxs ds)@, --- because succ and pred would break otherwise -instance Dimensions ds => Enum (Idxs (ds :: [Nat])) where +{- | +@ds@ must be fixed (either @[Nat]@ or all (N n)) to know exact bounds in +each dimension. + -} +instance Dimensions ds => Enum (Idxs ds) where succ idx = case go dds idx of (True , _ ) -> succError $ showIdxsType dds (False, i') -> i' where dds = dims @ds - go :: forall (ns :: [Nat]) . Dims ns -> Idxs ns -> (Bool, Idxs ns) + go :: forall ns . Dims ns -> Idxs ns -> (Bool, Idxs ns) go U U = (True, U) go (d :* ds) (Idx' i :* is) = case go ds is of (True , is') @@ -370,7 +586,7 @@ (False, i') -> i' where dds = dims @ds - go :: forall (ns :: [Nat]) . Dims ns -> Idxs ns -> (Bool, Idxs ns) + go :: forall ns . Dims ns -> Idxs ns -> (Bool, Idxs ns) go U U = (True, U) go (d :* ds) (Idx' i :* is) = case go ds is of (True , is') @@ -384,7 +600,7 @@ _ -> toEnumError (showIdxsType dds) off0 (0, totalDim dds - 1) where dds = dims @ds - go :: forall (ns :: [Nat]) . Dims ns -> (Word, Idxs ns) + go :: forall ns . Dims ns -> (Word, Idxs ns) go U = (fromIntegral off0, U) go (d :* ds) | (off , is) <- go ds @@ -400,7 +616,7 @@ f (d, i) (td, off) = (d * td, off + td * i) {-# INLINE fromEnum #-} - enumFrom = unsafeCoerce# go True (dims @ds) + enumFrom = unsafeCoerce go True (dims @ds) where go :: Bool -> [Word] -> [Word] -> [[Word]] go b (d:ds) (i:is) = @@ -410,7 +626,7 @@ go _ _ _ = [[]] {-# INLINE enumFrom #-} - enumFromTo = unsafeCoerce# go True True (dims @ds) + enumFromTo = unsafeCoerce go True True (dims @ds) where go :: Bool -> Bool -> [Word] -> [Word] -> [Word] -> [[Word]] go bl bu (d:ds) (x:xs) (y:ys) = @@ -428,9 +644,17 @@ {-# INLINE enumFromTo #-} enumFromThen x0 x1 = case compare x1 x0 of - EQ -> repeat x0 - GT -> enumFromThenTo x0 x1 maxBound - LT -> enumFromThenTo x0 x1 minBound + EQ -> repeat x0 + GT -> enumFromThenTo x0 x1 $ maxB ds + LT -> enumFromThenTo x0 x1 $ minB ds + where + ds = dims @ds + maxB :: forall ns . Dims ns -> Idxs ns + maxB U = U + maxB (x :* xs) = coerce (dimVal x - 1) :* maxB xs + minB :: forall ns . Dims ns -> Idxs ns + minB U = U + minB (_ :* xs) = Idx' 0 :* minB xs {-# INLINE enumFromThen #-} enumFromThenTo x0 x1 y = case dir of @@ -442,7 +666,7 @@ (0, is') -> repeatStep is' _ -> [] else [] - in unsafeCoerce# (repeatStep allX0s) + in unsafeCoerce (repeatStep allX0s) LT -> let (_, allDXs) = idxMinus allDs allX1s allX0s repeatStep is = if is >= allYs @@ -450,7 +674,7 @@ (0, is') -> repeatStep is' _ -> [] else [] - in unsafeCoerce# (repeatStep allX0s) + in unsafeCoerce (repeatStep allX0s) where allDs = listDims $ dims @ds allX0s = listIdxs x0 @@ -473,11 +697,121 @@ {-# INLINE enumFromThenTo #-} - --- | Show type of Idx (for displaying nice errors). -showIdxType :: forall (k :: Type) (x :: k) . BoundedDim x => String -showIdxType = "Idx " ++ show (dimVal (dimBound @k @x)) - -- | Show type of Idxs (for displaying nice errors). showIdxsType :: Dims ns -> String showIdxsType ds = "Idxs '" ++ show (listDims ds) + +-- | Throw an `OutOfDimBounds` exception without the CallStack attached. +outOfDimBoundsNoCallStack :: + Integral i + => String -- ^ Label (e.g. function name) + -> i -- ^ Bad index + -> Word -- ^ Target dim + -> Maybe Word -- ^ SubSpace Dim, if applicable. + -> Maybe ([Word], [Word]) -- ^ Larger picture: Dims and Idxs + -> a +outOfDimBoundsNoCallStack s i d msubd dimsCtx + = throw OutOfDimBounds + { oodIdx = toInteger i + , oodDim = d + , oodSubDim = msubd + , oodDimsCtx = dimsCtx + , oodName = s + , oodCallStack = Nothing + } + +-- | Throw an `OutOfDimBounds` exception. +outOfDimBounds :: + (HasCallStack, Integral i) + => String -- ^ Label (e.g. function name) + -> i -- ^ Bad index + -> Word -- ^ Target dim + -> Maybe Word -- ^ SubSpace Dim, if applicable. + -> Maybe ([Word], [Word]) -- ^ Larger picture: Dims and Idxs + -> a +outOfDimBounds s i d msubd dimsCtx + = throw OutOfDimBounds + { oodIdx = toInteger i + , oodDim = d + , oodSubDim = msubd + , oodDimsCtx = dimsCtx + , oodName = s + , oodCallStack = Just callStack + } + +{- | +Typically, this exception can occur in the following cases: + + * Converting from integral values to @Idx d@ when @d ~ N n@ or @d :: Nat@. + * Using @Enum@ and @Num@ when @d ~ N n@ or @d :: Nat@. + * Converting from @Idx (XN m :: XNat)@ to @Idx (n :: Nat)@. + * Indexing or slicing data using @Idx (XN m :: XNat)@. + +If you are mad and want to avoid any overhead related to bounds checking and the +related error handling, you can turn on the @unsafeindices@ flag to remove all of +this from the library at once. + -} +data OutOfDimBounds + = OutOfDimBounds + { oodIdx :: Integer + -- ^ A value that should have been a valid `Idx` + , oodDim :: Word + -- ^ A runtime value of a `Dim` + , oodSubDim :: Maybe Word + -- ^ When used for slicing, this should have satisfied + -- @oodIdx + oodSubDim <= oodDim@. + , oodDimsCtx :: Maybe ([Word], [Word]) + -- ^ If available, contains (Dims xns, Idxs xns). + , oodName :: String + -- ^ Short description of the error location, typically a function name. + , oodCallStack :: Maybe CallStack + -- ^ Function call stack, if available. + -- Note, this field is ignored in the `Eq` and `Ord` instances. + } + +-- | Note, this instance ignores `oodCallStack` +instance Eq OutOfDimBounds where + (==) a b = and + [ (==) (oodIdx a) (oodIdx b) + , (==) (oodDim a) (oodDim b) + , (==) (oodSubDim a) (oodSubDim b) + , (==) (oodDimsCtx a) (oodDimsCtx b) + , (==) (oodName a) (oodName b) + ] + +-- | Note, this instance ignores `oodCallStack` +instance Ord OutOfDimBounds where + compare a b = mconcat + [ compare (oodIdx a) (oodIdx b) + , compare (oodDim a) (oodDim b) + , compare (oodSubDim a) (oodSubDim b) + , compare (oodDimsCtx a) (oodDimsCtx b) + , compare (oodName a) (oodName b) + ] + +instance Show OutOfDimBounds where + showsPrec p e = addLoc errStr + where + addLoc s + = let someE = case oodCallStack e of + Nothing -> errorCallException s + Just st -> errorCallWithCallStackException s st + errc :: ErrorCall + errc = case fromException someE of + Nothing -> ErrorCall s + Just ec -> ec + in showsPrec p errc + errStr = oodName e ++ ": " ++ errContent ++ errCtx + errContent = case oodSubDim e of + Nothing -> "index " ++ show (oodIdx e) ++ + " is outside of Dim bounds (0 <= i < " ++ show (oodDim e) ++ ")" + Just sd -> "index " ++ show (oodIdx e) ++ + " and subspace dim " ++ show sd ++ + " together exceed the original space dim " ++ show (oodDim e) + errCtx = case oodDimsCtx e of + Nothing -> "." + Just (ds, is) + -> ";\n dims: " ++ (case someDimsVal ds of SomeDims x -> show x) + ++ "\n idxs: " ++ show (unsafeCoerce is :: Idxs ns) + +instance Exception OutOfDimBounds diff --git a/src/Numeric/Tuple.hs b/src/Numeric/Tuple.hs --- a/src/Numeric/Tuple.hs +++ b/src/Numeric/Tuple.hs @@ -16,6 +16,8 @@ import Numeric.Tuple.Strict as TS import Unsafe.Coerce (unsafeCoerce) +-- | /O(n)/ Convert a lazy @Tuple@ to a strict @Tuple@, forcing all its values +-- to the WHNF along the way. toStrict :: TL.Tuple xs -> TS.Tuple xs toStrict U = U toStrict (TL.Id x :* xs) @@ -23,6 +25,7 @@ !ys = toStrict xs in y :* ys +-- | /O(n)/ Convert a strict @Tuple@ to a lazy @Tuple@ by means of a simple coercion. 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 --- a/src/Numeric/Tuple/Lazy.hs +++ b/src/Numeric/Tuple/Lazy.hs @@ -49,10 +49,10 @@ import Data.Semigroup as Sem (Semigroup (..)) import Data.String (IsString) import Foreign.Storable (Storable) -import GHC.Base (Type) -import GHC.Exts +import GHC.Base (Type, Any) import GHC.Generics (Generic, Generic1) import qualified Text.Read as P +import Unsafe.Coerce (unsafeCoerce) import Data.Type.List import Numeric.TypedList @@ -126,7 +126,7 @@ -- | A tuple indexed by a list of types -type Tuple (xs :: [Type]) = TypedList Id xs +type Tuple = (TypedList Id :: [Type] -> Type) {-# COMPLETE U, (:$) #-} {-# COMPLETE U, (:!) #-} @@ -157,32 +157,32 @@ -- | Grow a tuple on the left O(1). (*$) :: x -> Tuple xs -> Tuple (x :+ xs) -(*$) x xs = unsafeCoerce# (unsafeCoerce# x : unsafeCoerce# xs :: [Any]) +(*$) 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 +(*!) !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]) +($*) 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] +(!*) !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 + in unsafeCoerce r {-# INLINE (!*) #-} infixl 5 !* @@ -194,7 +194,7 @@ instance ( RepresentableList xs , All Semigroup xs , All Monoid xs) => Mon.Monoid (Tuple xs) where - mempty = go (tList @Type @xs) + mempty = go (tList @xs) where go :: forall (ys :: [Type]) . All Monoid ys => TypeList ys -> Tuple ys @@ -206,13 +206,13 @@ instance (RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) where - minBound = go (tList @Type @xs) + minBound = go (tList @xs) where go :: forall (ys :: [Type]) . All Bounded ys => TypeList ys -> Tuple ys go U = U go (_ :* xs) = minBound *$ go xs - maxBound = go (tList @Type @xs) + maxBound = go (tList @xs) where go :: forall (ys :: [Type]) . All Bounded ys => TypeList ys -> Tuple ys @@ -231,10 +231,10 @@ compare (x :* tx) (y :* ty) = compare1 x y <> compare tx ty instance All Show xs => Show (Tuple xs) where - showsPrec = typedListShowsPrecC @Type @Show ":$" showsPrec1 + showsPrec = typedListShowsPrecC @Show ":$" showsPrec1 instance (All Read xs, RepresentableList xs) => Read (Tuple xs) where - readPrec = typedListReadPrec @Type @Read ":$" readPrec1 (tList @Type @xs) + readPrec = typedListReadPrec @Read ":$" readPrec1 (tList @xs) readList = P.readListDefault readListPrec = P.readListPrecDefault diff --git a/src/Numeric/Tuple/Strict.hs b/src/Numeric/Tuple/Strict.hs --- a/src/Numeric/Tuple/Strict.hs +++ b/src/Numeric/Tuple/Strict.hs @@ -49,10 +49,10 @@ import Data.Semigroup as Sem (Semigroup (..)) import Data.String (IsString) import Foreign.Storable (Storable) -import GHC.Base (Type) -import GHC.Exts +import GHC.Base (Type, Any) import GHC.Generics (Generic, Generic1) import qualified Text.Read as P +import Unsafe.Coerce (unsafeCoerce) import Data.Type.List import Numeric.TypedList @@ -126,7 +126,7 @@ -- | A tuple indexed by a list of types -type Tuple (xs :: [Type]) = TypedList Id xs +type Tuple = (TypedList Id :: [Type] -> Type) {-# COMPLETE U, (:$) #-} {-# COMPLETE U, (:!) #-} @@ -157,32 +157,32 @@ -- | Grow a tuple on the left O(1). (*$) :: x -> Tuple xs -> Tuple (x :+ xs) -(*$) x xs = unsafeCoerce# (unsafeCoerce# x : unsafeCoerce# xs :: [Any]) +(*$) 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 +(*!) !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]) +($*) 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] +(!*) !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 + in unsafeCoerce r {-# INLINE (!*) #-} infixl 5 !* @@ -194,7 +194,7 @@ instance ( RepresentableList xs , All Semigroup xs , All Monoid xs) => Mon.Monoid (Tuple xs) where - mempty = go (tList @Type @xs) + mempty = go (tList @xs) where go :: forall (ys :: [Type]) . All Monoid ys => TypeList ys -> Tuple ys @@ -206,13 +206,13 @@ instance (RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) where - minBound = go (tList @Type @xs) + minBound = go (tList @xs) where go :: forall (ys :: [Type]) . All Bounded ys => TypeList ys -> Tuple ys go U = U go (_ :* xs) = minBound *! go xs - maxBound = go (tList @Type @xs) + maxBound = go (tList @xs) where go :: forall (ys :: [Type]) . All Bounded ys => TypeList ys -> Tuple ys @@ -231,10 +231,10 @@ compare (x :* tx) (y :* ty) = compare1 x y <> compare tx ty instance All Show xs => Show (Tuple xs) where - showsPrec = typedListShowsPrecC @Type @Show ":!" showsPrec1 + showsPrec = typedListShowsPrecC @Show ":!" showsPrec1 instance (All Read xs, RepresentableList xs) => Read (Tuple xs) where - readPrec = typedListReadPrec @Type @Read ":!" readPrec1 (tList @Type @xs) + readPrec = typedListReadPrec @Read ":!" readPrec1 (tList @xs) readList = P.readListDefault readListPrec = P.readListPrecDefault diff --git a/src/Numeric/TypedList.hs b/src/Numeric/TypedList.hs --- a/src/Numeric/TypedList.hs +++ b/src/Numeric/TypedList.hs @@ -38,7 +38,7 @@ ( TypedList (U, (:*), Empty, TypeList, EvList, Cons, Snoc, Reverse) , RepresentableList (..) , Dict1 (..), DictList - , TypeList, types, typeables,inferTypeableList + , TypeList, types, typeables, inferTypeableList , order, order' , cons, snoc , Numeric.TypedList.reverse @@ -65,6 +65,8 @@ import Data.Constraint hiding ((***)) import Data.Data import Data.Type.List +import Data.Type.List.Internal +import Data.Type.Lits import Data.Void import GHC.Base (Type) import GHC.Exts @@ -73,8 +75,9 @@ import qualified Text.Read as Read import qualified Text.Read.Lex as Read import qualified Type.Reflection as R +import Unsafe.Coerce (unsafeCoerce) -import {-# SOURCE #-} Numeric.Dimensions.Dim (Dim, Nat, dimVal, minusDimM) +import {-# SOURCE #-} Numeric.Dimensions.Dim (Dim, dimVal, minusDimM) -- | Type-indexed list newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any] @@ -96,11 +99,11 @@ instance (Typeable k, Typeable f, Typeable xs, All Data (Map f xs)) => Data (TypedList (f :: (k -> Type)) (xs :: [k])) where gfoldl _ z U = z U - gfoldl k z (x :* xs) = case inferTypeableCons @_ @xs of + gfoldl k z (x :* xs) = case inferTypeableCons @xs of Dict -> z (:*) `k` x `k` xs - gunfold k z _ = case typeables @k @xs of + gunfold k z _ = case typeables @xs of U -> z U - _ :* _ -> case inferTypeableCons @_ @xs of Dict -> k (k (z (:*))) + _ :* _ -> case inferTypeableCons @xs of Dict -> k (k (z (:*))) toConstr U = typedListConstrEmpty toConstr (_ :* _) = typedListConstrCons dataTypeOf _ = typedListDataType @@ -121,12 +124,16 @@ TypedListRepNil (_ ': _) = Rec0 Void type family TypedListRepCons (f :: (k -> Type)) (xs :: [k]) :: (Type -> Type) where - TypedListRepCons _ '[] = Rec0 Void - TypedListRepCons f (x ': xs) = C1 ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False) - ( S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) + TypedListRepCons _ '[] + = Rec0 Void + TypedListRepCons f (x ': xs) + = C1 ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False) + ( S1 ('MetaSel 'Nothing 'NoSourceUnpackedness + 'NoSourceStrictness 'DecidedLazy) (Rec0 (f x)) :*: - S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) + S1 ('MetaSel 'Nothing 'NoSourceUnpackedness + 'NoSourceStrictness 'DecidedLazy) (Rec0 (TypedList f xs)) ) @@ -137,13 +144,13 @@ from U = M1 (L1 (M1 U1)) from (x :* xs) = M1 (R1 (M1 (M1 (K1 x) :*: M1 (K1 xs)))) to (M1 (L1 _)) - | Dict <- unsafeEqTypes @[k] @xs @'[] = U + | Dict <- unsafeEqTypes @xs @'[] = U to (M1 (R1 xxs)) - | Dict <- unsafeEqTypes @[k] @xs @(Head xs ': Tail xs) + | Dict <- unsafeEqTypes @xs @(Head xs ': Tail xs) , M1 (M1 (K1 x) :*: M1 (K1 xs)) <- xxs = x :* xs -- | A list of type proxies -type TypeList (xs :: [k]) = TypedList Proxy xs +type TypeList = (TypedList Proxy :: [k] -> Type) -- | Same as `Dict`, but allows to separate constraint function from -- the type it is applied to. @@ -170,26 +177,25 @@ -- | A list of dicts for the same constraint over several types. -type DictList (c :: k -> Constraint) (xs :: [k]) - = TypedList (Dict1 c) xs +type DictList (c :: k -> Constraint) + = (TypedList (Dict1 c) :: [k] -> Type) -- | 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 (k :: Type) (xs :: [k]) - . () => RepresentableList xs => TypeList xs +pattern TypeList :: forall xs . () => RepresentableList xs => TypeList xs pattern TypeList <- (mkRTL -> Dict) where - TypeList = tList @k @xs + TypeList = tList @xs -- | Pattern matching against this allows manipulating lists of constraints. -- Useful when creating functions that change the shape of dimensions. -pattern EvList :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k]) +pattern EvList :: forall c xs . () => (All c xs, RepresentableList xs) => DictList c xs pattern EvList <- (mkEVL -> Dict) where - EvList = _evList (tList @k @xs) + EvList = _evList (tList @xs) -- | Zero-length type list pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) @@ -204,116 +210,142 @@ pattern Empty = U -- | Constructing a type-indexed list -pattern (:*) :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) +pattern (:*) :: forall f xs . () - => forall (y :: k) (ys :: [k]) + => forall y ys . (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 (k :: Type) (f :: k -> Type) (xs :: [k]) +pattern Cons :: forall f xs . () - => forall (y :: k) (ys :: [k]) + => forall y ys . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs -pattern Cons x xs <- (patTL @k @f @xs -> PatCons x 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 (k :: Type) (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 @k @f @xs -> PatSnoc sx x) +pattern Snoc :: forall f xs . () + => forall sy y . SnocList sy y xs + => 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 (k :: Type) (f :: k -> Type) (xs :: [k]) - . () - => forall (sx :: [k]) - . (xs ~ Reverse sx, sx ~ Reverse xs) +pattern Reverse :: forall f xs . () + => forall sx . ReverseList xs sx => TypedList f sx -> TypedList f xs -pattern Reverse sx <- (unreverseTL @k @f @xs -> PatReverse sx) +pattern Reverse sx <- (unreverseTL @_ @f @xs -> PatReverse sx) where Reverse = Numeric.TypedList.reverse -cons :: forall (k :: Type) (f :: k -> Type) (x :: k) (xs :: [k]) +-- | /O(1)/ append an element in front of a @TypedList@ (same as `(:)` for lists). +cons :: forall f x xs . f x -> TypedList f xs -> TypedList f (x :+ xs) -cons x xs = TypedList (unsafeCoerce# x : coerce xs) +cons x xs = TypedList (unsafeCoerce x : coerce xs) {-# INLINE cons #-} -snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (x :: k) +-- | /O(n)/ append an element to the end of a @TypedList@. +snoc :: forall f xs x . TypedList f xs -> f x -> TypedList f (xs +: x) -snoc xs x = TypedList (coerce xs ++ [unsafeCoerce# x]) +snoc xs x = TypedList (coerce xs ++ [unsafeCoerce x]) {-# INLINE snoc #-} -reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) +-- | /O(n)/ return elements of a @TypedList@ in reverse order. +reverse :: forall f xs . TypedList f xs -> TypedList f (Reverse xs) reverse = coerce (Prelude.reverse :: [Any] -> [Any]) {-# INLINE reverse #-} -head :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) +-- | /O(1)/ Extract the first element of a @TypedList@, which must be non-empty. +head :: forall f xs . TypedList f xs -> f (Head xs) -head (TypedList xs) = unsafeCoerce# (Prelude.head xs) +head (TypedList xs) = unsafeCoerce (Prelude.head xs) {-# INLINE head #-} -tail :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) +-- | /O(1)/ Extract the elements after the head of a @TypedList@, +-- which must be non-empty. +tail :: forall f xs . TypedList f xs -> TypedList f (Tail xs) tail = coerce (Prelude.tail :: [Any] -> [Any]) {-# INLINE tail #-} -init :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) +-- | /O(n)/ Return all the elements of a @TypedList@ except the last one +-- (the list must be non-empty). +init :: forall f xs . TypedList f xs -> TypedList f (Init xs) init = coerce (Prelude.init :: [Any] -> [Any]) {-# INLINE init #-} -last :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) +-- | /O(n)/ Extract the last element of a @TypedList@, which must be non-empty. +last :: forall f xs . TypedList f xs -> f (Last xs) -last (TypedList xs) = unsafeCoerce# (Prelude.last xs) +last (TypedList xs) = unsafeCoerce (Prelude.last xs) {-# INLINE last #-} -take :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k]) +-- | /O(min(n,k))/ @take k xs@ returns a prefix of @xs@ of length @min(length xs, k)@. +-- It calls `Prelude.take` under the hood, so expect the same behavior. +take :: forall (n :: Nat) f xs . Dim n -> TypedList f xs -> TypedList f (Take n xs) take = coerce (Prelude.take . dimValInt :: Dim n -> [Any] -> [Any]) {-# INLINE take #-} -drop :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k]) +-- | /O(min(n,k))/ @drop k xs@ returns a suffix of @xs@ of length @max(0, length xs - k)@. +-- It calls `Prelude.drop` under the hood, so expect the same behavior. +drop :: forall (n :: Nat) f xs . Dim n -> TypedList f xs -> TypedList f (Drop n xs) drop = coerce (Prelude.drop . dimValInt :: Dim n -> [Any] -> [Any]) {-# INLINE drop #-} -length :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) +-- | Return the number of elements in a @TypedList@ (same as `order`). +length :: forall f xs . TypedList f xs -> Dim (Length xs) length = order {-# INLINE length #-} -splitAt :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k]) + +-- | /O(min(n,k))/ @splitAt k xs@ has the same effect as @('take' k xs, 'drop' k xs)@. +-- It calls `Prelude.splitAt` under the hood, so expect the same behavior. +splitAt :: forall (n :: Nat) f xs . Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs)) splitAt = coerce (Prelude.splitAt . dimValInt :: Dim n -> [Any] -> ([Any], [Any])) {-# INLINE splitAt #-} -order' :: forall (k :: Type) (xs :: [k]) - . RepresentableList xs => Dim (Length xs) -order' = order (tList @_ @xs) + +-- | Return the number of elements in a type list @xs@ bound by a constraint +-- @RepresentableList xs@ (same as `order`, but takes no value arguments). +order' :: forall xs . RepresentableList xs => Dim (Length xs) +order' = order (tList @xs) {-# INLINE order' #-} -order :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) +-- | Return the number of elements in a @TypedList@ (same as `length`). +order :: forall f xs . TypedList f xs -> Dim (Length xs) -order = unsafeCoerce# (fromIntegral . Prelude.length :: [Any] -> Word) +order = unsafeCoerce (fromIntegral . Prelude.length :: [Any] -> Word) {-# INLINE order #-} -concat :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]) +-- | Concat two @TypedList@s. +-- It calls `Prelude.(++)` under the hood, so expect the same behavior. +concat :: forall f xs ys . TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys) concat = coerce ((++) :: [Any] -> [Any] -> [Any]) {-# INLINE concat #-} -stripPrefix :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]) +-- | Drops the given prefix from a @TypedList@. +-- It returns 'Nothing' if the @TypedList@ does not start with the prefix +-- given, or 'Just' the @TypedList@ after the prefix, if it does. +-- It calls `Prelude.stripPrefix` under the hood, so expect the same behavior. +-- +-- This function can be used to find the type-level evidence that one type-level +-- list is indeed a prefix of another. +stripPrefix :: forall f xs ys . ( All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys @@ -326,7 +358,13 @@ | otherwise = Nothing {-# INLINE stripPrefix #-} -stripSuffix :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]) +-- | Drops the given suffix from a @TypedList@. +-- It returns 'Nothing' if the @TypedList@ does not end with the suffix +-- given, or 'Just' the @TypedList@ before the suffix, if it does. +-- +-- This function can be used to find the type-level evidence that one type-level +-- list is indeed a suffix of another. +stripSuffix :: forall f xs ys . ( All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys @@ -344,7 +382,7 @@ -- | Returns two things at once: -- (Evidence that types of lists match, value-level equality). -sameList :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]) +sameList :: forall f xs ys . ( All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys @@ -359,14 +397,14 @@ sameList _ _ = Nothing -- | Map a function over contents of a typed list -map :: forall (k :: Type) (f :: k -> Type) (g :: k -> Type) (xs :: [k]) - . (forall (a :: k) . f a -> g a) +map :: forall f g xs + . (forall a . f a -> g a) -> TypedList f xs -> TypedList g xs map k = coerce (Prelude.map k') where k' :: Any -> Any - k' = unsafeCoerce# . k . unsafeCoerce# + k' = unsafeCoerce k {-# INLINE map #-} -- | Get a constructible `TypeList` from any other `TypedList`; @@ -375,9 +413,9 @@ -- -- > case types ts of TypeList -> ... -- -types :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) +types :: forall f xs . TypedList f xs -> TypeList xs -types (TypedList xs) = unsafeCoerce# (Prelude.map (const Proxy) xs) +types = Numeric.TypedList.map (const Proxy) {-# INLINE types #-} -- | Construct a @TypeList xs@ if there is an instance of @Typeable xs@ around. @@ -385,30 +423,29 @@ -- This way, you can always bring `RepresentableList` instance into the scope -- if you have a `Typeable` instance. -- -typeables :: forall (k :: Type) (xs :: [k]) . Typeable xs => TypeList xs +typeables :: forall xs . Typeable xs => TypeList xs typeables = case R.typeRep @xs of - R.App (R.App _ (_ :: R.TypeRep (n :: k1))) (txs :: R.TypeRep (ns :: k2)) - -> case (unsafeCoerce# (Dict @(k1 ~ k1, k2 ~ k2)) - :: Dict (k ~ k1, [k] ~ k2)) of - Dict -> case (unsafeCoerce# (Dict @(xs ~ xs)) - :: Dict (xs ~ (n ': ns))) of - Dict -> Proxy @n :* R.withTypeable txs (typeables @k @ns) + R.App (R.App _ (_ :: R.TypeRep (n :: k))) (txs :: R.TypeRep (ns :: ks)) + | Dict <- unsafeCoerce (Dict @(k ~ k, ks ~ ks)) + :: Dict (k ~ KindOfEl xs, ks ~ KindOf xs) + , Dict <- unsafeEqTypes @xs @(n ': ns) + -> Proxy @n :* R.withTypeable txs (typeables @ns) R.Con _ - -> unsafeCoerce# U + -> unsafeCoerce U r -> error ("typeables -- impossible typeRep: " ++ show r) {-# INLINE typeables #-} -- | If all elements of a @TypedList@ are @Typeable@, -- then the list of these elements is also @Typeable@. -inferTypeableList :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) - . (Typeable k, All Typeable xs) +inferTypeableList :: forall f xs + . (Typeable (KindOfEl xs), All Typeable xs) => TypedList f xs -> Dict (Typeable xs) inferTypeableList U = Dict inferTypeableList (_ :* xs) = case inferTypeableList xs of Dict -> Dict -- | Representable type lists. -- Allows getting type information about list structure at runtime. -class RepresentableList (xs :: [k]) where +class RepresentableList xs where -- | Get type-level constructed list tList :: TypeList xs @@ -416,39 +453,38 @@ tList = U instance RepresentableList xs => RepresentableList (x ': xs :: [k]) where - tList = Proxy @x :* tList @k @xs + tList = Proxy @x :* tList @xs -- | Generic show function for a @TypedList@. -typedListShowsPrecC :: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type) (xs :: [k]) +typedListShowsPrecC :: forall c f xs . All c xs => String -- ^ Override cons symbol - -> ( forall (x :: k) . c x => Int -> f x -> ShowS ) + -> ( forall x . c x => Int -> f x -> ShowS ) -- ^ How to show a single element -> Int -> TypedList f xs -> ShowS typedListShowsPrecC _ _ _ U = showChar 'U' typedListShowsPrecC consS elShowsPrec p (x :* xs) = showParen (p >= 6) $ elShowsPrec 6 x . showChar ' ' . showString consS . showChar ' ' - . typedListShowsPrecC @k @c @f consS elShowsPrec 5 xs + . typedListShowsPrecC @c @f consS elShowsPrec 5 xs -- | Generic show function for a @TypedList@. -typedListShowsPrec :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) - . ( forall (x :: k) . Int -> f x -> ShowS ) +typedListShowsPrec :: forall f xs + . ( forall x . Int -> f x -> ShowS ) -- ^ How to show a single element -> Int -> TypedList f xs -> ShowS typedListShowsPrec _ _ U = showChar 'U' typedListShowsPrec elShowsPrec p (x :* xs) = showParen (p >= 6) $ - elShowsPrec 6 x . showString " :* " . typedListShowsPrec @k @f elShowsPrec 5 xs + elShowsPrec 6 x . showString " :* " . typedListShowsPrec @f elShowsPrec 5 xs -- | Generic read function for a @TypedList@. -- Requires a "template" to enforce the structure of the type list. -typedListReadPrec :: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type) - (xs :: [k]) (g :: k -> Type) +typedListReadPrec :: forall c f xs g . All c xs => String -- ^ Override cons symbol - -> ( forall (x :: k) . c x => Read.ReadPrec (f x) ) + -> ( forall x . c x => Read.ReadPrec (f x) ) -- ^ How to read a single element -> TypedList g xs -- ^ Enforce the type structure of the result @@ -457,15 +493,15 @@ typedListReadPrec consS elReadPrec (_ :* ts) = Read.parens . Read.prec 5 $ do x <- Read.step elReadPrec Read.lift . Read.expect $ Read.Symbol consS - xs <- typedListReadPrec @k @c consS elReadPrec ts + xs <- typedListReadPrec @c consS elReadPrec ts return (x :* xs) -- | Generic read function for a @TypedList@ of unknown length. -withTypedListReadPrec :: forall (k :: Type) (f :: k -> Type) (r :: Type) +withTypedListReadPrec :: forall f (r :: Type) . (forall (z :: Type) . - ( forall (x :: k) . f x -> z) -> Read.ReadPrec z ) + ( forall x . f x -> z) -> Read.ReadPrec z ) -- ^ How to read a single element - -> (forall (xs :: [k]) . TypedList f xs -> r ) + -> (forall xs . TypedList f xs -> r ) -- ^ Consume the result -> Read.ReadPrec r withTypedListReadPrec withElReadPrec use = Read.parens $ @@ -474,7 +510,7 @@ Read.prec 5 (do WithAnyTL withX <- Read.step $ withElReadPrec (\x -> WithAnyTL $ use . (x :*)) Read.lift . Read.expect $ Read.Symbol ":*" - withTypedListReadPrec @k @f @r withElReadPrec withX + withTypedListReadPrec @f @r withElReadPrec withX ) -- Workaround impredicative polymorphism @@ -494,21 +530,18 @@ . TypeList xs -> (RepresentableList xs => r) -> r -reifyRepList tl k = unsafeCoerce# (MagicRepList k :: MagicRepList xs r) tl +reifyRepList tl k = unsafeCoerce (MagicRepList k :: MagicRepList xs r) tl {-# INLINE reifyRepList #-} newtype MagicRepList xs r = MagicRepList (RepresentableList xs => r) data PatReverse (f :: k -> Type) (xs :: [k]) - = forall (sx :: [k]) . (xs ~ Reverse sx, sx ~ Reverse xs) - => PatReverse (TypedList f sx) + = forall (sx :: [k]) . ReverseList xs sx => PatReverse (TypedList f sx) unreverseTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) . TypedList f xs -> PatReverse f xs -unreverseTL (TypedList xs) - = case (unsafeCoerce# (Dict @(xs ~ xs, xs ~ xs)) - :: Dict (xs ~ Reverse sx, sx ~ Reverse xs) - ) of - Dict -> PatReverse (unsafeCoerce# (Prelude.reverse xs)) +unreverseTL xs + = case unsafeEqTypes @xs @(Reverse (Reverse xs)) of + Dict -> PatReverse @k @f @xs @(Reverse xs) (Numeric.TypedList.reverse xs) {-# INLINE unreverseTL #-} @@ -521,16 +554,16 @@ data PatSnoc (f :: k -> Type) (xs :: [k]) where PatSNil :: PatSnoc f '[] - PatSnoc :: TypedList f ys -> f y -> PatSnoc f (ys +: y) + PatSnoc :: SnocList xs s xss => TypedList f xs -> f s -> PatSnoc f xss unsnocTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) . TypedList f xs -> PatSnoc f xs unsnocTL (TypedList []) - = case unsafeEqTypes @_ @xs @'[] of + = case unsafeEqTypes @xs @'[] of Dict -> PatSNil unsnocTL (TypedList (x:xs)) - = case unsafeEqTypes @_ @xs @(Init xs +: Last xs) of - Dict -> PatSnoc (unsafeCoerce# sy) (unsafeCoerce# y) + = case unsafeEqTypes @xs @(Init xs +: Last xs) of + Dict -> PatSnoc (coerce sy) (unsafeCoerce y) where (sy, y) = unsnoc x xs unsnoc :: Any -> [Any] -> ([Any], Any) @@ -546,11 +579,11 @@ patTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) . TypedList f xs -> PatCons f xs patTL (TypedList []) - = case unsafeEqTypes @_ @xs @'[] of + = case unsafeEqTypes @xs @'[] of Dict -> PatCNil patTL (TypedList (x : xs)) - = case unsafeEqTypes @_ @xs @(Head xs ': Tail xs) of - Dict -> PatCons (unsafeCoerce# x) (unsafeCoerce# xs) + = case unsafeEqTypes @xs @(Head xs ': Tail xs) of + Dict -> PatCons (unsafeCoerce x) (coerce xs) {-# INLINE patTL #-} mkEVL :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k]) @@ -564,8 +597,6 @@ _evList U = U _evList (_ :* xs) = case _evList xs of evs -> Dict1 :* evs -unsafeEqTypes :: forall (k :: Type) (a :: k) (b :: k) . Dict (a ~ b) -unsafeEqTypes = unsafeCoerce# (Dict :: Dict (a ~ a)) dimValInt :: forall (k :: Type) (x :: k) . Dim x -> Int dimValInt = fromIntegral . dimVal diff --git a/test/Data/Type/ListTest.hs b/test/Data/Type/ListTest.hs new file mode 100644 --- /dev/null +++ b/test/Data/Type/ListTest.hs @@ -0,0 +1,193 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Type.ListTest where + +import Data.Constraint +import Data.Kind (Type) +import Data.Type.Equality +import Data.Type.List +import Data.Type.Lits +import Numeric.Natural +import Test.QuickCheck +import Unsafe.Coerce + +data P (a :: k) = P Natural + deriving (Eq, Show, Read) + +p :: KnownNat n => P n +p = let x = P (natVal x) in x + +cmpP :: P n -> P m -> SEq n m +cmpP (P a) (P b) + | a == b = unsafeCoerce (SEq @() @()) + | otherwise = unsafeCoerce (SNe @1 @2) + +data L :: [k] -> Type where + N :: L '[] + (:^) :: P n -> L ns -> L (n ': ns) +infixr 5 :^ + +data SEq :: k -> k -> Type where + SEq :: (a ~ b, (a == b) ~ 'True) => SEq a b + SNe :: ((a == b) ~ 'False) => SEq a b + +cmpL :: L as -> L bs -> SEq as bs +cmpL N N = SEq +cmpL (a :^ as) (b :^ bs) = case (cmpP a b, cmpL as bs) of + (SEq, SEq) -> SEq + (SNe, _) -> SNe + (_, SNe) -> SNe +cmpL N (_ :^ _) = SNe +cmpL (_ :^ _) N = SNe + +instance Show (L as) where + show N = "" + show (P n :^ N) = show n + show (P n :^ xs) = show n ++ "." ++ show xs + + +data SomeL (k :: Type) = forall (as :: [k]) . SomeL (L as) + +instance Show (SomeL k) where + show (SomeL a) = show a + +x00 :: P 0 +x00 = p + +x01 :: P 1 +x01 = p + +xs00 :: L ('[] :: [Nat]) +xs00 = N + +xs01 :: L '[3] +xs01 = p :^ N + +xs02 :: L '[4,8] +xs02 = p :^ p :^ N + +xs03 :: L '[5,7,9,2] +xs03 = p :^ p :^ p :^ p :^ N + +snoc :: forall (k :: Type) (xs :: [k]) (s :: k) (xss :: [k]) + . SnocList xs s xss => L xs -> P s -> L xss +snoc N x = x :^ N +snoc (x :^ xs) y = x :^ (snoc xs y) + +someXs00 :: SomeL Nat +someXs00 = SomeL xs00 +someXs01 :: SomeL Nat +someXs01 = SomeL xs01 +someXs02 :: SomeL Nat +someXs02 = SomeL xs02 +someXs03 :: SomeL Nat +someXs03 = SomeL xs03 + +initL :: forall (k :: Type) (xs :: [k]) (s :: k) (xss :: [k]) + . SnocList xs s xss => L xss -> L xs +initL (_ :^ N) = N +initL (x :^ (y :^ ys)) = x :^ initL (y :^ ys) + +revL1 :: forall (k :: Type) (xs :: [k]) (sx :: [k]) + . ReverseList xs sx => L xs -> L sx +revL1 N = N +revL1 (m :^ ms) = snoc (revL1 ms) m + +revL2 :: forall (k :: Type) (xs :: [k]) (sx :: [k]) + . ReverseList xs sx => L sx -> L xs +revL2 N = N +revL2 (m :^ ms) = snoc (revL2 ms) m + +revL3 :: forall (k :: Type) (xs :: [k]) + . L xs -> L (Reverse xs) +revL3 xs = go xs N + where + go :: forall (ys :: [k]) (sy :: [k]) (zs :: [k]) + . ReverseList ys sy => L ys -> L zs -> L (sy ++ zs) + go N ms = ms + go ((n :: P n) :^ (ns :: L ns)) ms + | Dict <- inferConcat @sy @zs + = go ns (n :^ ms) + + +stripPrefL :: ConcatList as bs asbs => L as -> L asbs -> L bs +stripPrefL N asbs = asbs +stripPrefL (_ :^ as) (_ :^ asbs) = stripPrefL as asbs + + +stripSufL :: ConcatList as bs asbs => L bs -> L asbs -> L as +stripSufL N asbs = asbs +stripSufL bs aasbs@(a :^ asbs) = case cmpL bs aasbs of + SEq -> N + SNe -> a :^ stripSufL bs asbs + +concatL :: ConcatList as bs asbs => L as -> L bs -> L asbs +concatL N bs = bs +concatL (a :^ as) bs = a :^ concatL as bs + + + +goList :: forall as bs asbs + . ConcatList as bs asbs => L as -> L bs -> L asbs -> Property +goList as bs asbs = conjoin + [ conjoin $ map ((show as ===) . show) + [as, stripSufL bs asbs, concatL N as, concatL as N, stripSufL bs (concatL N asbs)] + , conjoin $ map ((show bs ===) . show) + [bs, stripPrefL as asbs, concatL N bs, concatL bs N, stripPrefL as (concatL N asbs)] + , conjoin $ map ((show asbs ===) . show) + [asbs, concatL as bs, concatL N asbs, concatL asbs N, concatL as (concatL N bs)] + , -- sadly, we have to use inferConcat here, because GHC cannot voluntarily + -- try to infer ConcatList from the appearence of Concat TF alone. + -- A plugin would solve this. + case inferConcat @(Reverse bs) @(Reverse as) @_ of + Dict -> show (revL1 asbs) === show (concatL (revL1 bs) (revL1 as)) + ] + + +splitN :: Int -> SomeL k -> (SomeL k, SomeL k) +splitN 0 xs = (SomeL N, xs) +splitN _ (SomeL N) = (SomeL N, SomeL N) +splitN n (SomeL (x :^ xs)) + | (SomeL as, SomeL bs) <- splitN (n-1) (SomeL xs) + = (SomeL (snoc as x), SomeL bs) + + +dropEnd :: Int -> [a] -> [a] +dropEnd n = reverse . drop n . reverse + +runTests :: IO Bool +runTests = isGood <$> quickCheckResult (conjoin tests) + where + isGood :: Result -> Bool + isGood Success {} = True + isGood _ = False + tests :: [Property] + tests = + [ show xs00 === show (revL1 xs00) + , dropEnd 2 (show xs03) === show (initL xs03) + , show xs03 === reverse (show (revL1 xs03)) + , show as === show (stripSufL bs xs03) + , show (snd $ splitN 0 $ SomeL asbs) === drop 0 (show asbs) + , show (snd $ splitN 1 $ SomeL asbs) === drop 2 (show asbs) + , show (snd $ splitN 2 $ SomeL asbs) === drop 4 (show asbs) + , show (snd $ splitN 3 $ SomeL asbs) === drop 6 (show asbs) + , show (snd $ splitN 4 $ SomeL asbs) === drop 8 (show asbs) + , show (snd $ splitN 5 $ SomeL asbs) === drop 10 (show asbs) + , goList as bs asbs + ] + as = initL $ initL xs03 + bs = stripPrefL as xs03 + asbs = concatL as bs diff --git a/test/Numeric/Dimensions/DimTest.hs b/test/Numeric/Dimensions/DimTest.hs --- a/test/Numeric/Dimensions/DimTest.hs +++ b/test/Numeric/Dimensions/DimTest.hs @@ -64,8 +64,8 @@ | a <- max a' b' , b <- min a' b' , xda <- someDimVal a -- this is an unknown (Dim (XN 0)) - , Dx (db :: Dim b) <- someDimVal b - , Just (Dx da) <- constrainDim @_ @(XN b) xda -- here da >= db + , Dx (db@D :: Dim b) <- someDimVal b + , Just (Dx da) <- constrainDim @(XN b) xda -- here da >= db = a - b == dimVal (minusDim da db) prop_minusDim _ _ = False diff --git a/test/Numeric/Dimensions/IdxTest.hs b/test/Numeric/Dimensions/IdxTest.hs --- a/test/Numeric/Dimensions/IdxTest.hs +++ b/test/Numeric/Dimensions/IdxTest.hs @@ -10,7 +10,7 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} -module Numeric.Dimensions.IdxTest (runTests) where +module Numeric.Dimensions.IdxTest where import Control.Arrow import Data.List @@ -45,7 +45,7 @@ prop_idxsFromWords1 ins | (xs, ys) <- minMaxSeq ins , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys - , mIs <- idxsFromWords @Nat @ds xs + , mIs <- idxsFromWords @ds xs = or (zipWith (==) xs ys) || isJust mIs | otherwise = error "Impossible arguments" @@ -55,7 +55,7 @@ prop_idxsFromWords2 ins | (xs, ys) <- minMaxSeq ins , SomeDims (KnownDims :: Dims ds) <- someDimsVal xs - , mIs <- idxsFromWords @Nat @ds ys + , mIs <- idxsFromWords @ds ys = null xs || isNothing mIs | otherwise = error "Impossible arguments" @@ -65,7 +65,7 @@ prop_idxsFromWords3 ins | (xs, ys) <- minMaxSeq ins , SomeDims (ds@KnownDims :: Dims ds) <- someDimsVal ys - , mIs <- idxsFromWords @Nat @ds xs + , mIs <- idxsFromWords @ds xs = Just False /= (go xs ds <$> mIs) | otherwise = error "Impossible arguments" @@ -82,14 +82,14 @@ -- check for Word overflow wouldNotOverflow :: [Word] -> Bool wouldNotOverflow - = and . snd . mapAccumR (\a e -> (a*e, a*e >= a && multLimit > a)) 1 + = and . snd . mapAccumR (\a e -> (a*e, a*e >= a && multLimit > a && multLimit > e)) 1 prop_idxsFromEnum :: [(Word, Word)] -> Bool prop_idxsFromEnum ins | (xs, ys) <- minMaxSeq ins , wouldNotOverflow ys , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys - , Just ids <- idxsFromWords @Nat @ds xs + , Just ids <- idxsFromWords @ds xs = ids == toEnum (fromEnum ids) | otherwise = True @@ -98,7 +98,7 @@ | (xs, ys) <- minMaxSeq ins , wouldNotOverflow ys , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys - , Just ids <- idxsFromWords @Nat @ds xs + , Just ids <- idxsFromWords @ds xs = ids == maxBound || fromEnum (succ ids) == succ (fromEnum ids) | otherwise = True @@ -107,7 +107,7 @@ | (xs, ys) <- minMaxSeq ins , wouldNotOverflow ys , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys - , Just ids <- idxsFromWords @Nat @ds xs + , Just ids <- idxsFromWords @ds xs = ids == minBound || fromEnum (pred ids) == pred (fromEnum ids) | otherwise = True @@ -115,7 +115,7 @@ prop_idxsPredSucc ins | (xs, ys) <- minMaxSeq ins , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys - , Just ids <- idxsFromWords @Nat @ds xs + , Just ids <- idxsFromWords @ds xs = ids == minBound || ids == maxBound || ( succ (pred ids) == ids && pred (succ ids) == ids ) | otherwise = True @@ -126,23 +126,23 @@ , wouldNotOverflow ys , product ys < 100000 , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys - , Just ids <- idxsFromWords @Nat @ds xs + , Just ids <- idxsFromWords @ds xs = [ids..] == map toEnum [fromEnum ids .. fromEnum (maxBound @(Idxs ds))] | otherwise = True prop_idxsEnumFromTo :: [(Word, Word, Word)] -> Bool prop_idxsEnumFromTo ins | (xs, ys, SomeDims (KnownDims :: Dims ds)) <- twoIdxsSeq ins - , Just ids <- idxsFromWords @Nat @ds xs - , Just jds <- idxsFromWords @Nat @ds ys + , Just ids <- idxsFromWords @ds xs + , Just jds <- idxsFromWords @ds ys = [ids..jds] == map toEnum [fromEnum ids .. fromEnum jds] | otherwise = True prop_idxsEnumFromThen :: [(Word, Word, Word)] -> Bool prop_idxsEnumFromThen ins | (xs, ys, SomeDims (KnownDims :: Dims ds)) <- twoIdxsSeq ins - , Just ids <- idxsFromWords @Nat @ds xs - , Just jds <- idxsFromWords @Nat @ds ys + , Just ids <- idxsFromWords @ds xs + , Just jds <- idxsFromWords @ds ys , lim <- if jds >= ids then maxBound else minBound :: Idxs ds = take 1000 [ids, jds ..] == @@ -152,8 +152,8 @@ prop_idxsEnumFromThenTo :: Bool -> [(Word, Word, Word)] -> Bool prop_idxsEnumFromThenTo up ins | (xs, ys, SomeDims (KnownDims :: Dims ds)) <- twoIdxsSeq ins - , Just ids <- idxsFromWords @Nat @ds xs - , Just jds <- idxsFromWords @Nat @ds ys + , Just ids <- idxsFromWords @ds xs + , Just jds <- idxsFromWords @ds ys , lim <- if up then maxBound else minBound :: Idxs ds = take 1000 [ids, jds .. lim] == diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -3,6 +3,7 @@ import Distribution.TestSuite import System.Exit +import qualified Data.Type.ListTest import qualified Numeric.Dimensions.DimTest import qualified Numeric.Dimensions.IdxTest @@ -10,7 +11,8 @@ -- | Collection of tests in detailed-0.9 format tests :: IO [Test] tests = return - [ test "Dim" Numeric.Dimensions.DimTest.runTests + [ test "List" Data.Type.ListTest.runTests + , test "Dim" Numeric.Dimensions.DimTest.runTests , test "Idx" Numeric.Dimensions.IdxTest.runTests ]