Hi

I'm sure it won't be to everyone's taste, but here's what
SHE makes of this problem. SHE lives here

http://personal.cis.strath.ac.uk/~conor/pub/she

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts,
>     MultiParamTypeClasses, RankNTypes #-}

You need to turn lots of stuff on to support the coding: it
would need much less machinery if this stuff were directly
implemented.

> module Vec where

> import ShePrelude

> data Nat :: * where
>   Z :: Nat
>   S :: Nat -> Nat
>   deriving (SheSingleton)

I'm asking for the generation of the singleton family,
so that I can form pi-types over Nat.

> data Vec :: {Nat} -> * -> * where
>   VNil :: Vec {Z} x
>   (:>) :: x -> Vec {n} x -> Vec {S n} x

Vectors, in the dependently typed tradition.

> instance Show x => Show (Vec {n} x) where
>   show VNil       = "VNil"
>   show (x :> xs)  = show x ++ " :> " ++ show xs

I gather I won't need to roll my own, next version.

> listVec :: [a] -> (pi (n :: Nat). Vec {n} a -> t) -> t
> listVec []       f = f {Z} VNil
> listVec (x : xs) f = listVec xs (\ n ys -> f {S n} (x :> ys))

And that's your gadget: it gives you the length and the
vector.

*Vec> listVec "Broad" (const show)
listVec "Broad" (const show)
"'B' :> 'r' :> 'o' :> 'a' :> 'd' :> VNil"

If you're curious, here's what SHE generates for the above.

{-# OPTIONS_GHC -F -pgmF she #-}
{-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts,
    MultiParamTypeClasses, RankNTypes #-}

module Vec where

import ShePrelude

data Nat :: * where
  Z :: Nat
  S :: Nat -> Nat

data Vec :: * -> * -> * where
  VNil :: Vec (SheTyZ) x
  (:>) :: x -> Vec (n) x -> Vec (SheTyS n) x

instance Show x => Show (Vec (n) x) where
  show VNil       = "VNil"
  show (x :> xs)  = show x ++ " :> " ++ show xs

listVec :: [a] -> (forall n . SheSingleton ( Nat) n -> Vec (n) a -> t) -> t
listVec [] f = f (SheWitZ) VNil
listVec (x : xs) f = listVec xs (\ n ys -> f (SheWitS n) (x :> ys))

data SheTyZ = SheTyZ
data SheTyS x1 = SheTyS x1
data SheTyVNil = SheTyVNil
data (:$#$#$#:>) x1 x2 = (:$#$#$#:>) x1 x2
type instance SheSingleton (Nat) = SheSingNat
data SheSingNat :: * -> * where
  SheWitZ :: SheSingNat  (SheTyZ)
SheWitS :: forall sha0. SheSingleton (Nat ) sha0 -> SheSingNat (SheTyS sha0)
instance SheChecks (Nat ) (SheTyZ) where sheTypes _ = SheWitZ
instance SheChecks (Nat ) sha0 => SheChecks (Nat ) (SheTyS sha0) where sheTypes _ =
  SheWitS (sheTypes (SheProxy :: SheProxy (Nat ) (sha0)))

All good clean fun

Conor


On 21 Aug 2009, at 17:18, Daniel Peebles wrote:

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....@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to