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

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

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

Ryan Ingram