...

Don't worry, it's just me not liking UndecidableInstances.

Without it, GHC doesn't like the 'Arg f ~ b' constraint

He's probably right. I don't like it either.

What will the type of 'levmarHL' look like using tuples or using your special list-like type?

I guess it would be something like LevMarParamCoolType c => (a -> c -> Double) -> c -> [(a, Double)] -> c

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 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

On Fri, Aug 21, 2009 at 1:03 PM, Jason Dagit wrote:

Even with a type class for our type level numbers I'm at a loss.  I just don't understand how to convert an arbitrary int into an arbitrary but fixed type.  Perhaps someone else on the list knows.  I would like to know, if it's possible, how to do it.

toPeano :: Nat n => Int -> n

The problem is that the parameter, n, is part of the input to toPeano, but you need it to be part of the output. To rephrase slightly, you have toPeano :: forall n. (Nat n) => Int -> n but you need, toPeano :: Int -> exists n. (Nat n) => n which states that toPeano determines the type of its return value. In Haskell, you can encode this with an existential data type, data SomeNat where SomeNat :: (Nat n) => n -> SomeNat toPeano :: Int -> SomeNat or, equivalently, by using a higher-order function. toPeano :: Int -> (forall n. Nat n => n -> t) -> t -- Dave Menendez http://www.eyrie.org/~zednenem/

For some reason I never saw David's reply to my email. On Fri, Aug 21, 2009 at 11:16 AM, Daniel Peebles wrote:

Just to expand on David's higher-order function for the original Vector type, we can do:

data AnyVec a where  AnyVec :: Vec a n -> AnyVec a

listToVec :: [a] -> AnyVec a listToVec = worker AnyVec

worker :: (forall n. Nat n => Vec a n -> t) -> [a] -> t worker f [] = f Nil worker f (x:xs) = worker (f . (Cons x)) xs

and have it behave as you'd expect. Note that in a sense this is "forgetful" of the original length of the list.

Isn't this the case every time you open open up the AnyVector type? The only way you can use the vector's size is when you want to do something that works with all sizes unless you're willing to walk the vector back to Nil? For example, if you started with two equal size vectors, wrap them in an AnyVector, then pass them off to a function that can append them, the type system won't know that you have a vector which is twice the original size.

Dan

On Fri, Aug 21, 2009 at 2:03 PM, David Menendez wrote:

...

On Fri, Aug 21, 2009 at 1:03 PM, Jason Dagit wrote:

...

Even with a type class for our type level numbers I'm at a loss.  I just don't understand how to convert an arbitrary int into an arbitrary but fixed type.  Perhaps someone else on the list knows.  I would like to know, if it's possible, how to do it.

toPeano :: Nat n => Int -> n

The problem is that the parameter, n, is part of the input to toPeano, but you need it to be part of the output. To rephrase slightly, you have

   toPeano :: forall n. (Nat n) =>  Int -> n

but you need,

   toPeano :: Int -> exists n. (Nat n) => n

Yes, that's exactly what I meant by my verbage above :) Guess I should have explicitly used the forall/exists terminology.

...

which states that toPeano determines the type of its return value. In Haskell, you can encode this with an existential data type,

   data SomeNat where SomeNat :: (Nat n) => n -> SomeNat    toPeano :: Int -> SomeNat

Okay, that's what we did with AnyVector. What I don't understand is how you'll actually use this. Once you create SomeNat, the type system no longer remembers which Nat. So to me, you're back where you started.

...

or, equivalently, by using a higher-order function.

   toPeano :: Int -> (forall n. Nat n => n -> t) -> t

This looks a bit more promising. For those unfamiliar with this form, it is the logical "negation" of the previous type. One description is here [1], where it is mentioned that the type of t cannot depend on n. So you could not for example, return Vector a n or do, "toPeano 5 id". I guess you end up writing your program inside out in a sense which is fine, but then how do you address the forgetfulness? Everything has to be inside one scope where you never wrap things in an existential type? Perhaps via the negated existential encoding your last version of toPeano? I have a hard time wrapping my head around it at this point. Jason [1] http://www.ofb.net/~frederik/vectro/draft-r2.pdf

On Fri, Aug 21, 2009 at 2:50 PM, Jason Dagit wrote:

...

On Fri, Aug 21, 2009 at 2:03 PM, David Menendez wrote:

...

The problem is that the parameter, n, is part of the input to toPeano, but you need it to be part of the output. To rephrase slightly, you have

   toPeano :: forall n. (Nat n) =>  Int -> n

but you need,

   toPeano :: Int -> exists n. (Nat n) => n

Yes, that's exactly what I meant by my verbage above :)  Guess I should have explicitly used the forall/exists terminology.

...

...

which states that toPeano determines the type of its return value. In Haskell, you can encode this with an existential data type,

   data SomeNat where SomeNat :: (Nat n) => n -> SomeNat    toPeano :: Int -> SomeNat

Okay, that's what we did with AnyVector.  What I don't understand is how you'll actually use this.  Once you create SomeNat, the type system no longer remembers which Nat.  So to me, you're back where you started.

I'm assuming you want toPeano and fromList to work on any possible input. In that case, the context has to be able to work for any nat type. It's not quite true that the type system doesn't remember the nat: it's bundled inside the data type, along with the class instance. Depending on what operations are available, you can recover the type as specifically as you want. For example, it's perfectly valid to write a function with this type: testLength :: (Nat n) => SomeVector a -> Maybe (Vector a n) which can then be used for distinguishing vectors of different lengths. It's also possible to prove that two vectors have the same (unknown) length and then use that fact elsewhere. data a :==: b where Eq :: a :==: a eqLengths :: Vector a n -> Vector b m -> Maybe (n :==: m) eqLengths Nil Nil = Just Eq eqLengths (_ :*: as) (_ :*: bs) = do Eq <- eqLengths as bs return Eq eqLengths _ _ = Nothing zipVectors :: Vector a n -> Vector b n -> Vector (a,b) n foo v1 v2 = case v1 of SomeVector v'1 -> case v2 of SomeVector v'2 -> case eqLengths v'1 v'2 of Nothing -> error "Something has gone wrong!" Just Eq -> let v3 = zipVectors v'1 v'2 in ...

...

...

or, equivalently, by using a higher-order function.

   toPeano :: Int -> (forall n. Nat n => n -> t) -> t

This looks a bit more promising.

It's an illusion; the two forms are inter-convertible. toPeanoX :: Int -> SomeNat toPeanoK :: Int -> (forall n. (Nat n) => n -> t) -> t toPeanoX n = toPeanoK n SomeNat toPeanoK n k = case toPeanoX n of (SomeNat n) -> k n

I guess you end up writing your program inside out in a sense which is fine, but then how do you address the forgetfulness?

You can't forget something you never knew in the first place. At compile-time, the length of the list isn't known, so it can't be reflected in the type. -- Dave Menendez http://www.eyrie.org/~zednenem/

Hi Bas, I haven't looked at your code too carefully, but unsafeCoerce amounts to proof by violence :) If you want to construct a (much more verbose, probably) "real" proof of your constraints, you might want to refer to Ryan Ingram's email[1] from a few months ago about lightweight dependent(-ish) types in Haskell. Hope this helps, Dan [1] http://www.haskell.org/pipermail/haskell-cafe/2009-June/062690.html On Fri, Aug 21, 2009 at 2:50 PM, Bas van Dijk wrote:

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

On Tue, Aug 25, 2009 at 12:07 AM, Ryan Ingram wrote:

unsafeCoerce is ugly and I wouldn't count on that working properly.

Here's a real solution: ...

Thanks very much! I'm beginning to understand the code. The only thing I don't understand is why you need:

newtype Witness x = Witness { unWitness :: x } witnessNat :: forall n. Nat n => n witnessNat = theWitness where theWitness = unWitness $ induction (undefined `asTypeOf` theWitness) (Witness Z) (Witness . S . unWitness)

I understand that 'witnessNat' is a overloaded value-level generator for Nats. So for example: 'witnessNat :: S (S (S Z))' returns the value: 'S (S (S Z))'. Then you use it in the implementation of 'toList' and 'fromList':

toList = ... induction (witnessNat :: n) ... fromList = ... induction (witnessNat :: n) ...

I guess so that 'induction' will then receive the right 'Nat' _value_. However the following also works:

toList = ... induction (undefined :: n) ... fromList = ... induction (undefined :: n) ...

Indeed, 'witnessNat' itself is implemented this way:

witnessNat = theWitness where theWitness = ... induction (undefined `asTypeOf` theWitness) ...

So the 'n' in 'induction n' is just a "type carrying parameter" i.e. it doesn't need to have a run-time representation. Al dough it looks like that a case analysis on 'n' is made at run-time in:

instance Nat n => Nat (S n) where caseNat (S n) _ s = s n

But I guess that is desugared away because 'S' is implemented as a newtype:

newtype S n = S n

Indeed, when I make an actual datatype of it then 'witnessNat :: S (S (S Z))' will crash with "*** Exception: Prelude.undefined". Again, thanks very much for this! Do you mind if I use this code in the levmar package (soon to be released on hackage)? regards, Bas

Also, be aware that we are testing the edges of what the compiler supports for type families here. I ran into a bug in my initial implementation which I submitted as http://hackage.haskell.org/trac/ghc/ticket/3460 -- ryan

On Tue, Aug 25, 2009 at 6:07 AM, Cristiano Paris wrote:

On Tue, Aug 25, 2009 at 12:07 AM, Ryan Ingram wrote:

...

...

{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, ScopedTypeVariables, FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}

Disturbing... I must admin it: I'll never be a Haskell Guru (tm).

That's funny, I consider GADTs, RankNTypes, and ScopedTypeVariables to be the starting point for real code. They just go at the top of the file without thinking at this point. (Well, sometimes I leave GADTs out) -- ryan

David Menendez wrote:

data SomeNat where SomeNat :: (Nat n) => n -> SomeNat toPeano :: Int -> SomeNat

or, equivalently, by using a higher-order function.

toPeano :: Int -> (forall n. Nat n => n -> t) -> t

Nice! I thought the only way to create them was with a new datatype, but this works too. I guess the nontrivial bit to think of is the introduction of a fresh type (t in this case). Thanks for this insight! Martijn.