-- |
-- Module      : Math.VectorSpace.Dual
-- Copyright   : (c) Justus Sagemüller 2020
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 

{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE Rank2Types             #-}
{-# LANGUAGE UnicodeSyntax          #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE KindSignatures         #-}

module Math.VectorSpace.Dual
       ( Dualness(..), Dual, DualityWitness(..), ValidDualness(..)
       , usingAnyDualness, DualnessSingletons(..)
       ) where

import Math.LinearMap.Category.Class
import Data.Kind (Type)


data Dualness = Vector | Functional

type family Dual (dn :: Dualness) where
  Dual Vector = Functional
  Dual Functional = Vector


data DualityWitness (dn :: Dualness) where
  DualityWitness :: (ValidDualness (Dual dn), Dual (Dual dn) ~ dn)
           => DualityWitness dn

data DualnessSingletons (dn :: Dualness) where
  VectorWitness :: DualnessSingletons Vector
  FunctionalWitness :: DualnessSingletons Functional

class ValidDualness (dn :: Dualness) where
  type Space dn v :: Type
  dualityWitness :: DualityWitness dn
  decideDualness :: DualnessSingletons dn
instance ValidDualness 'Vector where
  type 'Vector`Space` v = v
  dualityWitness :: DualityWitness 'Vector
dualityWitness = DualityWitness 'Vector
forall (dn :: Dualness).
(ValidDualness (Dual dn), Dual (Dual dn) ~ dn) =>
DualityWitness dn
DualityWitness
  decideDualness :: DualnessSingletons 'Vector
decideDualness = DualnessSingletons 'Vector
VectorWitness
instance ValidDualness 'Functional where
  type 'Functional`Space` v = DualVector v
  dualityWitness :: DualityWitness 'Functional
dualityWitness = DualityWitness 'Functional
forall (dn :: Dualness).
(ValidDualness (Dual dn), Dual (Dual dn) ~ dn) =>
DualityWitness dn
DualityWitness
  decideDualness :: DualnessSingletons 'Functional
decideDualness = DualnessSingletons 'Functional
FunctionalWitness

usingAnyDualness :: ∀ rc dn . ValidDualness dn
          => (rc 'Vector)
          -> (rc 'Functional)
          -> rc dn
usingAnyDualness :: rc 'Vector -> rc 'Functional -> rc dn
usingAnyDualness rc 'Vector
vecCase rc 'Functional
ftnCase = case ValidDualness dn => DualnessSingletons dn
forall (dn :: Dualness). ValidDualness dn => DualnessSingletons dn
decideDualness @dn of
     DualnessSingletons dn
VectorWitness -> rc dn
rc 'Vector
vecCase
     DualnessSingletons dn
FunctionalWitness -> rc dn
rc 'Functional
ftnCase