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

[Daniel Peebles]

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