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