unsafeCoerce is ugly and I wouldn't count on that working properly. Here's a real solution:
> {-# LANGUAGE GADTs, RankNTypes, TypeFamilies, ScopedTypeVariables, > FlexibleContexts #-} > {-# LANGUAGE FlexibleInstances #-} > module LevMar where > import Data.Maybe (fromJust) Type-level number scaffold: > data Z = Z > newtype S n = S n > class Nat n where > caseNat :: forall r. n -> (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p > -> r) -> r > instance Nat Z where > caseNat _ z _ = z > instance Nat n => Nat (S n) where > caseNat (S n) _ s = s n > induction :: forall p n. Nat n => n -> p Z -> (forall x. Nat x => p x -> p (S > x)) -> p n > induction n z s = caseNat n isZ isS where > isZ :: n ~ Z => p n > isZ = z > isS :: forall x. (n ~ S x, Nat x) => x -> p n > isS x = s (induction x z s) > 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) Sized list type: > data SizedList a n where > Nil :: SizedList a Z > Cons :: a -> SizedList a n -> SizedList a (S n) > infixr 2 `Cons` toList. Your implementation is simpler, but this gives you an idea of how to use "induction" to generate a function that you need. > newtype ToList a n = ToList { unToList :: SizedList a n -> [a] } > toList :: forall a n. Nat n => SizedList a n -> [a] > toList = unToList $ induction (witnessNat :: n) (ToList tl0) (ToList . tlS . > unToList) where > tl0 :: SizedList a Z -> [a] > tl0 Nil = [] > tlS :: forall x. Nat x => (SizedList a x -> [a]) -> SizedList a (S x) -> > [a] > tlS f (Cons x xs) = x : f xs fromList. Here we return a "Maybe" value to represent that the list might not be the right size. > newtype FromList a n = FromList { unFromList :: [a] -> Maybe (SizedList a n) } > fromList :: forall a n. Nat n => [a] -> Maybe (SizedList a n) > fromList = unFromList $ induction (witnessNat :: n) (FromList fl0) (FromList > . flS . unFromList) where > fl0 [] = Just Nil > fl0 _ = Nothing > flS k [] = Nothing > flS k (x:xs) = fmap (Cons x) $ k xs "Model" for your levMar functions > class (Nat (Arity f)) => Model f where > type Arity f > app :: f -> SizedList Double (Arity f) -> Double > instance Model Double where > type Arity Double = Z > app v Nil = v > instance Model f => Model (Double -> f) where > type Arity (Double -> f) = S (Arity f) > app f (Cons v vs) = app (f v) vs And the levmar implementations: > levmarML :: (a -> [Double] -> Double) -> [Double] -> [(a,Double)] -> [Double] > levmarML f inits samples = inits > levmarHL :: (Model f) => > (a -> f) -> SizedList Double (Arity f) -> [(a, Double)] -> SizedList > Double (Arity f) > levmarHL f inits samples = fromJust $ fromList $ > levmarML (\a -> app (f a) . fromJust . fromList) (toList inits) samples We rely on levmarML only calling the passed-in function with a correctly-sized list, and returning a similarily correctly-sized list. That assumption is made explicit with the calls to "fromJust". > testModel :: Double -> Double -> Double -> Double > testModel n x y = x*y - n*n > test = levmarHL testModel (1 `Cons` 2 `Cons` Nil) [(3, 10), (4, 20)] *LevMar> :t test test :: SizedList Double (Arity (Double -> Double -> Double)) *LevMar> toList test [1.0, 2.0] -- ryan On Fri, Aug 21, 2009 at 11:50 AM, Bas van Dijk<v.dijk....@gmail.com> 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 > _______________________________________________ > 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