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

[Daniel Peebles]

I'm pretty sure you're going to need an existential wrapper for your
fromList function. Something like:

data AnyVector a where
  AnyVector :: Vector a n -> AnyVector a

because otherwise you'll be returning different types from
intermediate iterations of your fromList function.

I was playing with n-ary functions yesterday too, and came up with the
following, which doesn't need undecidable instances, if you're
interested:

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

(you can also use the Replicate "function" to make type-level n-ary
vectors and maybe other stuff, who knows)

Hope this helps,
Dan

On Fri, Aug 21, 2009 at 7:41 AM, Bas van Dijk<v.dijk.bas at gmail.com> wrote:
> 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/
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>