# How to compute isomorphism $V \simeq V^{**}$ (in Haskell)?

Since there is a canonical isomorphism between vector space $V$ and his dual dual space $V^{**}$, $\dim V \in \mathbb N \;$, I want to write it as a Haskell function.

This function is going to have a type of

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

Is it possible at all?

-
The morphism $V^{\star\star}\to V$ is specific to finite dimensional spaces, whereas the morphism $V\to V^{\star\star}$ is not. The latter one is easily definable, the former needs dual basis. What is you data structure for finite dimensional space ? And note that the type is not exactly what you said, since you only consider linear functions. – Lierre Mar 28 '12 at 19:37
I posted a longish answer which I think completely misses the point of your question, and which I deleted; I now think that if you saw it should should try to forget it. – MJD Mar 28 '12 at 20:47
@Lierre yes, the type should take into account the linear structure. Why does the data structure matters? Take it any with defined $+$ and $\cdot$ satisfying vector space axioms. In terms of Haskell's polymorphism F :: (VectorSpaceOverKdimN V, Field K) => ((V -> K) -> K) -> V. – Yrogirg Mar 29 '12 at 4:25
Data structure matters because I doubt you'll be able to define such a map using only the operations for general vector spaces, you definitely need a basis or something equivalent, and formulation will change depending on the data structure. – Lierre Mar 29 '12 at 7:14
Hm, funny coincidence. I've been thinking over and over the issue this morning, and as a result I've decided to read "General Theory of Natural Equivalences" by Eilenberg and MacLane. I'm no good at category theory and I haven't heard much about that work, apart that it actually introduced category theory (mainly for studying natural transformations). And guess what? It starts with a consideration of $V \simeq V^{**} \;$. Though I think I won't get much from that work for the problem in problem, still it was a pleasant surprise. – Yrogirg Mar 29 '12 at 8:14

I thought a bit more. Yes, one need to be able to point a basis in $V$.

But that doesn't imply a certain data structure --- one just need to provide an isomorphism $V \simeq \mathbb K^n \;$ (preferably as a class method, alongside with $+$ and $\cdot\;$). That seems to be enough to construct both $V^*$ and $V \simeq V^{**}\;$.

At first I wasn't sure $\xi : V \simeq \mathbb K^n\;$ will allow for $\eta : V^* \simeq \mathbb K^n\;$, such that $V^{**} \to V\;$ may go as $V^{**} \to \mathbb K^n \to V\;$. However an experiment reveals

$$\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)$$

to be the way to construct $V^* \simeq \mathbb K^n\;$.

A Haskell example for $\dim V = 2\;$ case:

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

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


Casting $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)


and $\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)


To show that $\tau$ does not depend on $\xi : V \simeq \mathbb K^n \;$ lets's test two different $\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


Will that do?

-