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?