[Haskell-cafe] How to convert a list to a vector encoding its length in its type?

[Ryan Ingram]

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
>