work in progress notes for current design

notes.md

@@ -72,4 +72,6 @@ col major of 2x2 rowmajor (2dim)
 
 Array ... rank storage  layout  ... elem
 
-layout =  Lay (ColMajor :#  [n3:@ Colmajor, n2:@ RowMajor] )
+layout =  Lay (ColMajor :#  [n3:@ Colmajor, n2:@ RowMajor] )
+
+Theres currently a somewhat 

numerical-core.cabal

@@ -55,7 +55,7 @@ library
         Numerical.Types.Shape
         Numerical.Types.Nat 
 
-    ghc-options: -O2 -Wall
+    ghc-options: -O2 
     -- Modules included in this library but not exported.
     -- other-modules:       
 
@@ -69,14 +69,16 @@ library
         TypeOperators
         FlexibleInstances
         FlexibleContexts
+        TemplateHaskell 
 
     -- Other library packages from which modules are imported.
-    build-depends:       base >= 4.6 && < 4.8 ,
-                        primitive >= 0.5 && < 0.6,
-                        vector >= 0.10 && < 0.11,
-                        tagged >= 0.7 && < 0.8,
-                        template-haskell >= 2.8.0.0 && < 2.10.0.0,
-                        ghc-prim >= 0.3.0.0 && < 0.5.0.0
+    build-depends:       base >= 4.6 && < 4.9 
+                        ,primitive >= 0.5 && < 0.6
+                        ,vector >= 0.10 && < 0.11
+                        ,tagged >= 0.7 && < 0.8
+                        ,template-haskell >= 2.8.0.0 && < 2.10.0.0
+                        ,ghc-prim >= 0.3.0.0 && < 0.5.0.0
+                         ,singletons >= 0.9.0.0 && < 0.10.0.0
                         -- what version constraints?
 
 

src/Numerical/Types/Array.hs

@@ -22,10 +22,21 @@ or bite the primstate bullet now?
 data family Array world rep lay (view:: Locality) sh elm 
 
 
+{-
+only Row and Column Major have  dense formats that are unique across ALL
+possible ranks, not so simple for others. Make different data instances per formats
+
+
+
+
+
+-}
+--class Array  where
+
 -----------
 -- | for now locality is a closed type, may change going forward
 -- also should it be in a different module like shape or layout?
-data  Locality = Contiguous | Strided 
+
 
 
 {-
@@ -85,7 +96,11 @@ view =
 
 -}
 
-{- what class
+{-
+
+uncheckedReshape :: Array wld rep lay 
+
+
 -}
 
 

src/Numerical/Types/Layout.hs

@@ -11,6 +11,8 @@
 -- do i need flexible instances really?
 {-# LANGUAGE FlexibleInstances #-}
 
+{-# LANGUAGE UndecidableInstances #-}
+
 module Numerical.Types.Layout where
 
 
@@ -31,7 +33,7 @@ make it easy to define new dense array layouts
 
 
 -}
-
+data  Locality = Contiguous | Strided  | InnerContiguous
 
 data PrimLay a  
 data StaticLay a 
@@ -43,6 +45,11 @@ data Row = RowS
 data Col = ColS 
 
 
+--data Elem ls el  where 
+--    Point :: Elem '[] el
+--    (:#) :: a -> Elem ls el -> Elem (a ': ls) el  
+
+
 {-|
     One important invariant about all layouts at all ranks is that for 
     any given ints x < y, that the array index for inr
@@ -60,6 +67,27 @@ data Col = ColS
        toIndex shapedLayout xi <  toIndex  shapedLayout yj
 
 
+this actually relates to the notion of partial ordering over vectors in convex
+geometry!
+
+
+so roughly: we have layouts that are dense
+we have layouts that can be used as tiles (and are dense)
+
+and we have layouts which can can't be tiled, but can have elements which are tiled
+
+So we have
+
+PrimitiveLayouts
+
+Static Layouts
+
+General Layouts (which are a Top level layout over a static layout)
+
+the Layout class tries to abstract over all three cases 
+(NB: this only makes sense when the "rank" for the inner 
+and outer layouts have the same rank!)
+
 -}
 
 
@@ -79,51 +107,58 @@ I really do like how it makes things a teeny bit simpler.. though I may remove t
 -}
 
 
+
+--class SimpleDenseLayout lay (rank :: Nat) where
+--  type SimpleDenseTranpose lay 
+--  toIndexSimpleDense :: Shaped rank Int lay -> Shape rank Int -> Int 
+
+
 class PrimLayout lay (rank :: Nat) where 
     type TranposedPrim lay 
     toIndexPrim :: Shaped rank Int (PrimLay lay) -> Shape rank Int -> Int 
     fromIndexPrim :: Shaped rank Int (PrimLay lay) -> Int -> Shape rank Int 
 
-{-
-primlayouts have a block size of 1
--}
-
-
-class StaticLayout (ls :: [ Sized *]) (rank :: Nat) where
-    type TranposedStatic ls 
-    toIndexStatic :: Shaped rank Int (StaticLay ls) -> Shape rank Int -> Int 
-    fromIndexStatic :: Shaped rank Int (StaticLay ls) -> Int -> Shape rank Int     
-
---instance  StaticLayout [(N3 :@ Row),(N2 :@ Col)]    where 
-
---    deriving (Show, Read, Eq, Ord,Typeable,Data)
-
-class  GenLayout lay (rank :: Nat) where 
-    type TranposedGen lay 
-    toIndexGen :: Shaped rank Int (Lay lay) -> Shape rank Int -> Int
-    fromIndexGen :: Shaped rank Int (Lay lay) -> Int -> Shape rank Int 
-
---- not sure if I need this extra layer here
-class Layout lay (rank :: Nat) where 
-    type Tranposed lay 
-    toIndex :: Shaped rank Int lay -> Shape rank Int -> Int
-    {-# INLINE toIndex #-}
-    fromIndex :: Shaped rank Int lay -> Int -> Shape rank Int 
-    {-# INLINE fromIndex #-}
-
-instance GenLayout l r => Layout (Lay lay) r where
-    type Tranposed (Lay lay) = Lay (TranposedGen lay) 
-    toIndex = toIndexGen
-    {-# INLINE toIndex #-}
-    fromIndex = fromIndexGen
-    {-# INLINE fromIndex #-}
-
-instance StaticLay l r => Layout  (StaticLay l) r where
-    type Tranposed (StaticLay l)=  StaticLay ( TranposedStatic  l)
-    toIndex = toIndexStatic
-    {-# INLINE toIndex #-}
-    fromIndex = fromIndexStatic
-    {-# INLINE fromIndex #-}
+--{-
+--primlayouts have a block size of 1, no tiling, though they may themselves
+--used in forming tiles
+---}
+
+
+--class StaticLayout (ls :: [ Sized *]) (rank :: Nat) where
+--    type TranposedStatic ls 
+--    toIndexStatic :: Shaped rank Int (StaticLay ls) -> Shape rank Int -> Int 
+--    fromIndexStatic :: Shaped rank Int (StaticLay ls) -> Int -> Shape rank Int     
+
+----instance  StaticLayout [(N3 :@ Row),(N2 :@ Col)]    where 
+
+----    deriving (Show, Read, Eq, Ord,Typeable,Data)
+
+--class  GenLayout lay (rank :: Nat) where 
+--    type TranposedGen lay 
+--    toIndexGen :: Shaped rank Int (Lay lay) -> Shape rank Int -> Int
+--    fromIndexGen :: Shaped rank Int (Lay lay) -> Int -> Shape rank Int 
+
+----- not sure if I need this extra layer here
+--class Layout lay (rank :: Nat) where 
+--    type Tranposed lay 
+--    toIndex :: Shaped rank Int lay -> Shape rank Int -> Int
+--    {-# INLINE toIndex #-}
+--    fromIndex :: Shaped rank Int lay -> Int -> Shape rank Int 
+--    {-# INLINE fromIndex #-}
+----the fact that months layer i don't understand these genlayout and static layout instances tells me something
+--instance GenLayout lay rnk => Layout (Lay lay) rnk where
+--    type Tranposed (Lay lay) = Lay (TranposedGen lay) 
+--    toIndex = toIndexGen
+--    {-# INLINE toIndex #-}
+--    fromIndex = fromIndexGen
+--    {-# INLINE fromIndex #-}
+----
+--instance StaticLayout lay rnk => Layout  (StaticLay lay) rnk where
+--    type Tranposed (StaticLay lay)=  StaticLay ( TranposedStatic  lay)
+--    toIndex = toIndexStatic
+--    {-# INLINE toIndex #-}
+--    fromIndex = fromIndexStatic
+--    {-# INLINE fromIndex #-}
 
 
 

src/Numerical/Types/MArray.hs

@@ -6,4 +6,5 @@
 module Numerical.Types.MArray where
 
 
-class MArray mv world rep lay (view:: Locality) sh elem where
+--class MArray mv world rep lay (view:: Locality) sh elem where
+

src/Numerical/Types/Nat.hs

@@ -1,18 +1,16 @@
-{-# LANGUAGE PolyKinds   #-}
-{-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies, TypeOperators,
+             ConstraintKinds, ScopedTypeVariables, RankNTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE DeriveDataTypeable#-}
 {-# LANGUAGE CPP #-}
 
-module Numerical.Types.Nat(Nat(..),nat,N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10)  where
+module Numerical.Types.Nat(Nat(..),nat,N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10
+    ,SNat(..), type (+),plus_id_r,plus_succ_r)  where
 import Data.Typeable
 import Data.Data 
 import Language.Haskell.TH hiding (reify)
+import Data.Type.Equality
 
 data Nat = S !Nat  | Z 
     deriving (Eq,Show,Read,Typeable,Data)    
@@ -23,13 +21,37 @@ deriving instance Typeable 'S
 #endif
 
 
+
+type family n1 + n2 where
+  Z + n2 = n2
+  (S n1') + n2 = S (n1' + n2)
+
+-- singleton for Nat
+data SNat :: Nat -> * where
+  SZero :: SNat Z
+  SSucc :: SNat n -> SNat (S n)
+
+--gcoerce :: (a :~: b) -> ((a ~ b) => r) -> r
+--gcoerce Refl x = x
+--gcoerce = gcastWith
+
+-- inductive proof of right-identity of +
+plus_id_r :: SNat n -> ((n + Z) :~: n)
+plus_id_r SZero = Refl
+plus_id_r (SSucc n) = gcastWith (plus_id_r n) Refl
+
+-- inductive proof of simplification on the rhs of +
+plus_succ_r :: SNat n1 -> Proxy n2 -> ((n1 + (S n2)) :~: (S (n1 + n2)))
+plus_succ_r SZero _ = Refl
+plus_succ_r (SSucc n1) proxy_n2 = gcastWith (plus_succ_r n1 proxy_n2) Refl
+
 -- only use this if you're ok required template haskell
 nat :: Int -> TypeQ
 nat n
     | n >= 0 = localNat n
     | otherwise = error "nat: negative"
     where   localNat 0 =  conT 'Z
-            localNat n = conT 'S `appT` localNat (n-1)
+            localNat m = conT 'S `appT` localNat (m-1)
 
 
 type N0 = Z