Thx to Alp for his help

gargantext-graph.cabal

@@ -4,7 +4,7 @@ cabal-version: 1.12
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 2529152eda79b364f7b62e5d9eaf053e8f4e54488749bd83614d515e92c44d26
+-- hash: 0738cfbe36f67275fe7fcd289fd26bddd3727957358ad06543242f719c4f34f1
 
 name:           gargantext-graph
 version:        0.1.0.0
@@ -28,6 +28,7 @@ source-repository head
 library
   exposed-modules:
       Data.Array.Accelerate.Utils
+      Data.Eigen.Coeff
       Graph.BAC.Clustering
       Graph.BAC.Proxemy
       Graph.BAC.ProxemyOptim

src/Data/Eigen/Coeff.hs

+{-| Module  : Data.Eigen.Coeff
+Description : Safe coeff for Eigen Matrix
+Copyright   : (c) CNRS, 2017-Present
+License     : AGPL + CECILL v3
+Maintainer  : team@gargantext.org
+Stability   : experimental
+Portability : POSIX
+
+Author: Alp Mestanogullari (Well Typed)
+
+-}
+
+{-# LANGUAGE DataKinds, GADTs, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications, TypeOperators, TypeFamilies #-}
+
+module Data.Eigen.Coeff (coeffSM, coeffDM)
+  where
+
+import Eigen.Internal (Row(..), Col(..), Elem(..))
+import Data.Maybe (fromMaybe)
+import Data.Proxy
+import Data.Reflection
+import Data.Type.Equality
+import GHC.TypeLits
+import Unsafe.Coerce
+import Eigen.SparseMatrix (SparseMatrix)
+import Eigen.Matrix (Matrix)
+
+import qualified Eigen.SparseMatrix as SMatrix
+import qualified Eigen.Matrix       as DMatrix
+
+data (:<=?) (i :: Nat) (n :: Nat) where
+  IsLTE :: (i <=? n) :~: 'True  -> i :<=? n
+  IsGT  ::                         i :<=? n
+
+isLTE :: (KnownNat i, KnownNat n) => Proxy i -> Proxy n -> i :<=? n
+isLTE pi pn
+  | natVal pi <= natVal pn = IsLTE (unsafeCoerce Refl)
+  | otherwise              = IsGT
+
+reifyNatLT
+  :: forall r n. KnownNat n
+  => Int
+  -> Proxy n
+  -> r -- ^ what to return if the given 'Int' is > n
+  -> (forall i. (KnownNat i, i <= n) => Proxy i -> r)
+     -- ^ what to do if the given 'Int' indeed is <= n
+  -> r
+reifyNatLT i pn r k = reifyNat (fromIntegral i) $ \pi ->
+  case isLTE pi pn of
+    IsLTE Refl -> k pi
+    _          -> r
+
+-- * matrix use case
+
+{-
+-- say we're given those things (origin Eigen lib)
+data Mat (n :: Nat) (m :: Nat) a
+data Row (i :: Nat) = Row
+data Col (j :: Nat) = Col
+coeff
+  :: (KnownNat i, KnownNat j, KnownNat n, KnownNat m, i <= n, j <= m)
+  => Row i -> Col j -> Mat n m a -> a
+coeff = SMatrix.coeff
+-}
+
+-- we can now get:
+
+coeffSM
+  :: forall n m.
+     (KnownNat n, KnownNat m)
+  => Int -> Int -> SparseMatrix n m Double -> Double
+coeffSM x y m = fromMaybe 0 $ coeffSM' x y m
+
+coeffSM'
+  :: forall n m a.
+     (KnownNat n, KnownNat m, Elem a)
+  => Int -> Int -> SparseMatrix n m a -> Maybe a
+coeffSM' i j mat =
+  reifyNatLT i pn Nothing $ \pi ->
+  reifyNatLT j pm Nothing $ \pj ->
+    Just $ SMatrix.coeff (proxyRow pi) (proxyCol pj) mat
+
+  where pn = Proxy @n
+        pm = Proxy @m
+
+coeffDM
+  :: forall n m.
+     (KnownNat n, KnownNat m)
+  => Int -> Int -> Matrix n m Double -> Double
+coeffDM x y m = fromMaybe 0 $ coeffDM' x y m
+
+
+coeffDM'
+  :: forall n m a.
+     (KnownNat n, KnownNat m, Elem a)
+  => Int -> Int -> Matrix n m a -> Maybe a
+coeffDM' i j mat =
+  reifyNatLT i pn Nothing $ \pi ->
+  reifyNatLT j pm Nothing $ \pj ->
+    Just $ DMatrix.coeff (proxyRow pi) (proxyCol pj) mat
+
+  where pn = Proxy @n
+        pm = Proxy @m
+
+
+
+
+-- helpers
+proxyRow :: Proxy i -> Row i
+proxyRow _ = Row
+proxyCol :: Proxy j -> Col j
+proxyCol _ = Col

src/Graph/BAC/ProxemyOptim.hs

@@ -29,12 +29,13 @@ module Graph.BAC.ProxemyOptim
   where
 
 --import Debug.SimpleReflect
+import Data.Eigen.Coeff (coeffSM, coeffDM)
 import Data.IntMap (IntMap)
 import Data.Maybe (isJust)
 import Data.Proxy (Proxy(Proxy))
 import Data.Reflection
 import Eigen.Internal (CTriplet(..), Elem(..), toC, fromC, C(..), natToInt, Row(..), Col(..))
-import Eigen.Matrix (sum, unsafeCoeff)
+import Eigen.Matrix (sum)
 import Eigen.SparseMatrix (SparseMatrix, SparseMatrixXd, (!), toMatrix)
 import GHC.TypeLits (KnownNat, Nat, SomeNat(SomeNat), type(+), natVal, sameNat, someNatVal)
 import Graph.FGL
@@ -80,23 +81,6 @@ withG :: (Show a, Show b)
       -> r
 withG g f = reifyNat (fromIntegral $ length $ nodes g) $ \n -> f (buildFiniteGraph n g)
 
--- ∀ x. P x -> ∃ x. P x
-data T a b where
-  T :: forall n a b. KnownNat n => Proxy n -> FiniteGraph n a b -> T a b
-data Dim (n  :: Nat) = Dim Nat
----------------------------------------------------------------
-getDim :: Graph a b -> Integer
-getDim = undefined
-
-getDim' :: T a b -> Integer
-getDim' (T p _) = natVal p
-
-tab :: Graph a b -> T a b
-tab g = do
-  let Just someNat = someNatVal (fromIntegral $ length $ nodes g)
-  case someNat of
-    SomeNat p -> T p (FiniteGraph g)
-
 ---------------------------------------------------------------
 ---------------------------------------------------------------
 type DenseMatrix      n = DenseMatrix.Matrix n n Double
@@ -200,7 +184,7 @@ matconf True _a _p = panic "MatConf True: TODO but not needed for now"
 
 
 symmetry :: KnownNat n => DenseMatrix n -> DenseMatrix n
-symmetry m = DMatrix.imap (\x y v -> if x < y then v else DMatrix.unsafeCoeff y x m) m
+symmetry m = DMatrix.imap (\x y v -> if x < y then v else coeffDM y x m) m
 
 matmod :: forall n a b. KnownNat n => FiniteGraph n a b -> ModularityMatrix n
 matmod fg = symmetry $ toMatrix modmat
@@ -233,8 +217,7 @@ edges_confluence l fg am tm = SMatrix.toList matconf
     matconf = SMatrix.imap (\x y v -> let am' = SMatrix.add am (SMatrix.fromList [(x,y,-v)])
                                           v'  = doProx l (sparseVectorFromList (Proxy @n) [(1,y,1)]) am'
 
-                                          prox_y_x_length = SMatrix.coeff (Row x) (Col 1) v' -- FIXME
-                                          -- prox_y_x_length = _unsafeCoeff x 1 v'
+                                          prox_y_x_length = coeffSM x 1 v'
                                           prox_y_x_infini = ((VS.!) degs x - 1) / (sumdeg - 2)
 
                                        in (prox_y_x_length - prox_y_x_length)
@@ -297,7 +280,7 @@ make_clust_part :: KnownNat n
                 => SortedEdges
                 -> SimilarityMatrix n
                 -> Clustering Node
-make_clust_part se sm = foldl' (\c (e1,e2,_) -> updateClustering c (\x y -> unsafeCoeff e1 e2 sm') e1 e2)
+make_clust_part se sm = foldl' (\c (e1,e2,_) -> updateClustering c (\x y -> coeffDM e1 e2 sm') e1 e2)
                                (Clustering Dict.empty Dict.empty 0) se
   where
     sm' = case sm of