Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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
up vote 1 down vote accepted

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?

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.