[Haskell-cafe] How to convert a list to a vector encoding its
length in its type?
Ryan Ingram
ryani.spam at gmail.com
Mon Aug 24 18:07:58 EDT 2009
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.bas at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
More information about the Haskell-Cafe
mailing list