Cómo calcular el isomorfismo $V \simeq V^{**}$ (en Haskell)?

Question

Dado que existe un isomorfismo canónico entre el espacio vectorial $V$ y su doble espacio dual $V^{**}$ , $\dim V \in \mathbb N \;$ Quiero escribirlo como una función Haskell.

Esta función tendrá un tipo

$$ F : \left( \left(V \to \mathbb K \right) \to \mathbb K \right) \to V $$

¿Es posible?

Answer 1

Pensé un poco más. Sí, hay que ser capaz de señalar una base en $V$ .

Pero eso no implica una cierta estructura de datos --- uno sólo tiene que proporcionar un isomorfismo $V \simeq \mathbb K^n \;$ (preferiblemente como método de clase, junto con $+$ y $\cdot\;$ ). Esto parece ser suficiente para construir tanto $V^*$ y $V \simeq V^{**}\;$ .

Al principio no estaba seguro $\xi : V \simeq \mathbb K^n\;$ permitirá $\eta : V^* \simeq \mathbb K^n\;$ tal que $V^{**} \to V\;$ puede ir como $V^{**} \to \mathbb K^n \to V\;$ . Sin embargo, un experimento revela

$$\left((\eta_x(f), \; \eta_y(f)\right) = \left(f \xi^{-1}(1,0), \; f \xi^{-1}(0,1)\right)$$ $$\eta^{-1}(f_x, f_y) = v \mapsto \left(x \cdot \xi_x(v) + y \cdot \xi_y(v)\right)$$

para construir $V^* \simeq \mathbb K^n\;$ .

Un ejemplo Haskell para $\dim V = 2\;$ caso:

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

class Vector2D v where
  (＋) :: v -> v -> v
  (·)  :: Double -> v -> v
  toArithSpace   :: v -> (Double, Double)
  fromArithSpace :: (Double, Double) -> v

Fundición $V^*\;$ :

type Dual v = v -> Double

instance (Vector2D v) => Vector2D (Dual v) where
  f＋g = \x -> f x + g x
  (·) = \l f -> (\x -> l * f(x))
  toArithSpace f = (f $ fromArithSpace (1,0), f $ fromArithSpace (0,1))
  fromArithSpace (x, y) = \z -> x * (fst $ toArithSpace z) + y * (snd $ toArithSpace z)

y $\tau : V \simeq V^{**}\;$ :

tauF :: Vector2D v => v -> (Dual (Dual v))
tauF x = \f -> f x

tauR :: Vector2D v => (Dual (Dual v)) -> v
tauR x = fromArithSpace (toArithSpace x)

Para demostrar que $\tau$ no depende de $\xi : V \simeq \mathbb K^n \;$ probemos dos $\xi$ :

data Pair  = Pair  Double Double deriving Show
data Pair' = Pair' Double Double deriving Show

instance Vector2D Pair where
  (Pair x1 y1)＋(Pair x2 y2) = Pair (x1+x1) (y1+y1)
  l · (Pair x y) = Pair (l*x) (l*y)
  toArithSpace (Pair x y) = (x+y,x-y)
  fromArithSpace (x, y) = Pair (0.5*(x+y)) (0.5*(x-y))

instance Vector2D Pair' where
  (Pair' x1 y1)＋(Pair' x2 y2) = Pair' (x1+x1) (y1+y1)
  l · (Pair' x y) = Pair' (l*x) (l*y)
  toArithSpace   (Pair' x y) = (x+2*y,4*x-y)
  fromArithSpace (x, y) = Pair' ((x+2*y)/9) ((4*x-y)/9)

*Main> (tauR.tauF) $ Pair 3 7
Pair 3.0 7.0
*Main> (tauR.tauF) $ Pair' 3 7
Pair' 3.0 7.0

¿Será suficiente?