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