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

[Bas van Dijk]

Hello,

We're working on a Haskell binding to levmar[1] a C implementation of
the Levenberg-Marquardt optimization algorithm. The
Levenberg-Marquardt algorithm is an iterative technique that finds a
local minimum of a function that is expressed as the sum of squares of
nonlinear functions. It has become a standard technique for nonlinear
least-squares problems. It's for example ideal for curve fitting.

The binding is nearly finished and consists of two layers: a low-level
layer that directly exports the C bindings and a medium-level layer
that wraps the lower-level functions and provides a more Haskell
friendly interface.

The Medium-Level (ML) layer has a function which is similar to:

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

So you give it a model function, an initial guess of the parameters
and some input samples. levmarML than tries to find the parameters
that best describe the input samples. Of course, the real function has
more arguments and return values but this simple version will do for
this discussion.

Al-dough this medium-level layer is more Haskell friendly than the
low-level layer it still has some issues. For example a model function
is represented as a function that takes a list of parameters. For
example:

> \x [p1, p2, p3] -> p1*x^2 + p2*x + p3

You have to ensure that the length of the initial guess of parameters
is exactly 3. Otherwise you get run-time pattern-match failures.

So I would like to create a new High-Level (HL) layer that overcomes
this problem.

First of all I need the following language extensions:

> {-# LANGUAGE EmptyDataDecls #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE GADTs #-}

I want to represent the model function as a normal Haskell function.
So instead of passing the parameters as a list I want to pass them as
arguments:

> \x p1 p2 p3 -> p1*x^2 + p2*x + p3

Because we would like to be able to use model functions of different
arity it means the levmarHL function needs to be polymorphic in the
model function:

> levmarHL :: (ModelFunc f, Arity f ~ n, Arg f ~ Double)
>          => (a -> f)
>          -> Vector Double n
>          -> [(a, Double)]
>          -> Vector Double n
> levmarHL model initParams samples =
>     fromList $ levmarML (\x params -> model x $* fromList params)
>                         (toList initParams)
>                         samples

You can see that the initial parameters and the result are passed as
Vectors that encode their length 'n' in their type. This length must
equal the arity of the model function: 'Arity f ~ n'. The arity of the
model function and the length of the vectors are represented as type
level naturals:

> data Z
> data S n

Lets look at the implementation of ModelFunc:

> class ModelFunc f where
>     type Arg   f :: *
>     type Arity f :: *
>
>     ($*) :: f -> Vector (Arg f) (Arity f) -> Arg f

$* is similar to $ but instead of applying a function to a single
argument it applies it to a vector of multiple arguments.

> instance (ModelFunc f, Arg f ~ b) => ModelFunc (b -> f) where
>     type Arg   (b -> f) = b
>     type Arity (b -> f) = S (Arity f)
>
>     f $* (x :*: xs) = f x $* xs

You can see that we restrict the arguments of module functions to have
the same type: 'Arg f ~ b'.

This is the base case:

> instance ModelFunc Double where
>     type Arg   Double = Double
>     type Arity Double = Z
>
>     d $* Nil = d

We represent Vectors using a GADT:

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

> infixr :*:

Converting a Vector to a list is easy:

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

My single question is: how can I convert a list to a Vector???

> fromList :: [b] -> Vector b n
> fromList = ?

regards,

Roel and Bas van Dijk

[1] http://www.ics.forth.gr/~lourakis/levmar/