[Haskell-cafe] How to convert a list to a vector encoding its length in its type?

[Bas van Dijk]

Thanks for all the advice.

I have this so far. Unfortunately I have to use unsafeCoerce:

-------------------------------------------------------------------------
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

module LevMar where

import Unsafe.Coerce

levmarML :: (a -> [Double] -> Double)
         -> [Double]
         -> [(a, Double)]
         -> [Double]
levmarML model initParams samples = initParams

data Z
data S n

data Nat n where
    Zero :: Nat Z
    Succ :: Nat n -> Nat (S n)

data Vector a n where
    Nil   :: Vector a Z
    (:*:) :: a -> Vector a n -> Vector a (S n)

infixr :*:

instance Show a => Show (Vector a n) where
    show Nil = "Nil"
    show (x :*: xs) = show x ++ " :*: " ++ show xs

toList :: Vector b n -> [b]
toList Nil        = []
toList (x :*: xs) = x : toList xs

listVec :: [a] -> (forall n. Vector a n -> t) -> t
listVec []       f = f Nil
listVec (x : xs) f = listVec xs (\ys -> f (x :*: ys))

type family Replicate n (a :: * -> *) b :: *
type instance Replicate (S x) a b = a (Replicate x a b)
type instance Replicate Z a b = b

type Function n a b = Replicate n ((->) a) b

($*) :: Function n a a -> Vector a n -> a
f $* Nil        = f
f $* (x :*: xs) = f x $* xs

levmarHL :: (a -> Function n Double Double)
         -> Vector Double n
         -> [(a, Double)]
         -> Vector Double n
levmarHL model initParams samples =
    listVec (levmarML (\x params -> listVec params $ \v ->
unsafeCoerce (model x) $* v)
                      (toList initParams)
                      samples)
            (unsafeCoerce)
-------------------------------------------------------------------------

regards,

Bas