content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  -- | This module declares all Shape related functions and data structures, as well as all singleton
  -- -- instances for the Shape data type. This module was highly influenciated by Grenade, a Haskell
  -- -- library for deep learning with dependent types. See: https://github.com/HuwCampbell/grenade
  module TensorSafe.Shape where
  
  import Data.Singletons (Sing, SingI (..))
  import GHC.TypeLits as N
  import TensorSafe.Core (L, R)
  
  --
  -- Shape definition as in Haskell's Grenade library
  --
  
  -- | The current shapes we accept.
  --   at the moment this is just one, two, and three dimensional
  --   Vectors/Matricies.
  --
  --   These are only used with DataKinds, as Kind `Shape`, with Types 'D1, 'D2, 'D3.
  data Shape
    = -- | One dimensional vector
      D1 Nat
    | -- | Two dimensional matrix. Row, Column.
      D2 Nat Nat
    | -- | Three dimensional matrix. Row, Column, Channels.
      D3 Nat Nat Nat
  
  -- | Concrete data structures for a Shape.
  --
  --   All shapes are held in contiguous memory.
  --   3D is held in a matrix (usually row oriented) which has height depth * rows.
  data S (n :: Shape) where
    S1D ::
      (KnownNat len) =>
      R len ->
      S ('D1 len)
    S2D ::
      (KnownNat rows, KnownNat columns) =>
      L rows columns ->
      S ('D2 rows columns)
    S3D ::
      ( KnownNat rows,
        KnownNat columns,
        KnownNat depth,
        KnownNat (rows N.* depth)
      ) =>
      L (rows N.* depth) columns ->
      S ('D3 rows columns depth)
  
  deriving instance Show (S n)
  
  -- Singleton instances.
  -- Check: http://hackage.haskell.org/package/singletons
  --
  -- These could probably be derived with template haskell, but this seems
  -- clear and makes adding the KnownNat constraints simple.
  -- We can also keep our code TH free, which is great.
  data instance Sing (n :: Shape) where
    D1Sing :: KnownNat a => Sing a -> Sing ('D1 a)
    D2Sing :: (KnownNat a, KnownNat b) => Sing a -> Sing b -> Sing ('D2 a b)
    D3Sing :: (KnownNat a, KnownNat b, KnownNat c) => Sing a -> Sing b -> Sing c -> Sing ('D3 a b c)
  
  instance KnownNat a => SingI ('D1 a) where
    sing = D1Sing sing
  
  instance (KnownNat a, KnownNat b) => SingI ('D2 a b) where
    sing = D2Sing sing sing
  
  instance (KnownNat a, KnownNat b, KnownNat c) => SingI ('D3 a b c) where
    sing = D3Sing sing sing sing
  
  -- | Compares two Shapes at kinds level and returns a Bool kind
  type family ShapeEquals (sIn :: Shape) (sOut :: Shape) :: Bool where
    ShapeEquals s s = 'True
    ShapeEquals _ _ = 'False
  
  -- | Same as ShapeEquals, which compares two Shapes at kinds level, but raises a TypeError exception
  -- if the Shapes are not the equal.
  type family ShapeEquals' (sIn :: Shape) (sOut :: Shape) :: Bool where
    ShapeEquals' s s = 'True
    ShapeEquals' s1 s2 =
      TypeError
        ( 'Text "Couldn't match the Shape "
            ':<>: 'ShowType s1
            ':<>: 'Text " with the Shape "
            ':<>: 'ShowType s2
        )
  