[Haskell-cafe] How to convert a list to a vector encoding its
length in its type?
Conor McBride
conor at strictlypositive.org
Fri Aug 21 12:47:22 EDT 2009
Hi
I'm sure it won't be to everyone's taste, but here's what
SHE makes of this problem. SHE lives here
http://personal.cis.strath.ac.uk/~conor/pub/she
> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies,
FlexibleContexts,
> MultiParamTypeClasses, RankNTypes #-}
You need to turn lots of stuff on to support the coding: it
would need much less machinery if this stuff were directly
implemented.
> module Vec where
> import ShePrelude
> data Nat :: * where
> Z :: Nat
> S :: Nat -> Nat
> deriving (SheSingleton)
I'm asking for the generation of the singleton family,
so that I can form pi-types over Nat.
> data Vec :: {Nat} -> * -> * where
> VNil :: Vec {Z} x
> (:>) :: x -> Vec {n} x -> Vec {S n} x
Vectors, in the dependently typed tradition.
> instance Show x => Show (Vec {n} x) where
> show VNil = "VNil"
> show (x :> xs) = show x ++ " :> " ++ show xs
I gather I won't need to roll my own, next version.
> listVec :: [a] -> (pi (n :: Nat). Vec {n} a -> t) -> t
> listVec [] f = f {Z} VNil
> listVec (x : xs) f = listVec xs (\ n ys -> f {S n} (x :> ys))
And that's your gadget: it gives you the length and the
vector.
*Vec> listVec "Broad" (const show)
listVec "Broad" (const show)
"'B' :> 'r' :> 'o' :> 'a' :> 'd' :> VNil"
If you're curious, here's what SHE generates for the above.
{-# OPTIONS_GHC -F -pgmF she #-}
{-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies,
FlexibleContexts,
MultiParamTypeClasses, RankNTypes #-}
module Vec where
import ShePrelude
data Nat :: * where
Z :: Nat
S :: Nat -> Nat
data Vec :: * -> * -> * where
VNil :: Vec (SheTyZ) x
(:>) :: x -> Vec (n) x -> Vec (SheTyS n) x
instance Show x => Show (Vec (n) x) where
show VNil = "VNil"
show (x :> xs) = show x ++ " :> " ++ show xs
listVec :: [a] -> (forall n . SheSingleton ( Nat) n -> Vec (n) a ->
t) -> t
listVec [] f = f (SheWitZ) VNil
listVec (x : xs) f = listVec xs (\ n ys -> f (SheWitS n) (x :> ys))
data SheTyZ = SheTyZ
data SheTyS x1 = SheTyS x1
data SheTyVNil = SheTyVNil
data (:$#$#$#:>) x1 x2 = (:$#$#$#:>) x1 x2
type instance SheSingleton (Nat) = SheSingNat
data SheSingNat :: * -> * where
SheWitZ :: SheSingNat (SheTyZ)
SheWitS :: forall sha0. SheSingleton (Nat ) sha0 -> SheSingNat
(SheTyS sha0)
instance SheChecks (Nat ) (SheTyZ) where sheTypes _ = SheWitZ
instance SheChecks (Nat ) sha0 => SheChecks (Nat ) (SheTyS sha0) where
sheTypes _ =
SheWitS (sheTypes (SheProxy :: SheProxy (Nat ) (sha0)))
All good clean fun
Conor
On 21 Aug 2009, at 17:18, Daniel Peebles wrote:
> I'm pretty sure you're going to need an existential wrapper for your
> fromList function. Something like:
>
> data AnyVector a where
> AnyVector :: Vector a n -> AnyVector a
>
> because otherwise you'll be returning different types from
> intermediate iterations of your fromList function.
>
> I was playing with n-ary functions yesterday too, and came up with the
> following, which doesn't need undecidable instances, if you're
> interested:
>
> 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
>
> (you can also use the Replicate "function" to make type-level n-ary
> vectors and maybe other stuff, who knows)
>
> Hope this helps,
> Dan
>
> On Fri, Aug 21, 2009 at 7:41 AM, Bas van Dijk<v.dijk.bas at gmail.com>
> wrote:
>> Hello,
>>
>> We're working on a Haskell binding to levmar[1] a C implementation of
>> the Levenberg-Marquardt optimization algorithm. The
>> Levenberg-Marquardt algorithm is an iterative technique that finds a
>> local minimum of a function that is expressed as the sum of squares
>> of
>> nonlinear functions. It has become a standard technique for nonlinear
>> least-squares problems. It's for example ideal for curve fitting.
>>
>> The binding is nearly finished and consists of two layers: a low-
>> level
>> layer that directly exports the C bindings and a medium-level layer
>> that wraps the lower-level functions and provides a more Haskell
>> friendly interface.
>>
>> The Medium-Level (ML) layer has a function which is similar to:
>>
>>> levmarML :: (a -> [Double] -> Double)
>>> -> [Double]
>>> -> [(a, Double)]
>>> -> [Double]
>>> levmarML model initParams samples = ...
>>
>> So you give it a model function, an initial guess of the parameters
>> and some input samples. levmarML than tries to find the parameters
>> that best describe the input samples. Of course, the real function
>> has
>> more arguments and return values but this simple version will do for
>> this discussion.
>>
>> Al-dough this medium-level layer is more Haskell friendly than the
>> low-level layer it still has some issues. For example a model
>> function
>> is represented as a function that takes a list of parameters. For
>> example:
>>
>>> \x [p1, p2, p3] -> p1*x^2 + p2*x + p3
>>
>> You have to ensure that the length of the initial guess of parameters
>> is exactly 3. Otherwise you get run-time pattern-match failures.
>>
>> So I would like to create a new High-Level (HL) layer that overcomes
>> this problem.
>>
>> First of all I need the following language extensions:
>>
>>> {-# LANGUAGE EmptyDataDecls #-}
>>> {-# LANGUAGE UndecidableInstances #-}
>>> {-# LANGUAGE TypeFamilies #-}
>>> {-# LANGUAGE GADTs #-}
>>
>> I want to represent the model function as a normal Haskell function.
>> So instead of passing the parameters as a list I want to pass them as
>> arguments:
>>
>>> \x p1 p2 p3 -> p1*x^2 + p2*x + p3
>>
>> Because we would like to be able to use model functions of different
>> arity it means the levmarHL function needs to be polymorphic in the
>> model function:
>>
>>> levmarHL :: (ModelFunc f, Arity f ~ n, Arg f ~ Double)
>>> => (a -> f)
>>> -> Vector Double n
>>> -> [(a, Double)]
>>> -> Vector Double n
>>> levmarHL model initParams samples =
>>> fromList $ levmarML (\x params -> model x $* fromList params)
>>> (toList initParams)
>>> samples
>>
>> You can see that the initial parameters and the result are passed as
>> Vectors that encode their length 'n' in their type. This length must
>> equal the arity of the model function: 'Arity f ~ n'. The arity of
>> the
>> model function and the length of the vectors are represented as type
>> level naturals:
>>
>>> data Z
>>> data S n
>>
>> Lets look at the implementation of ModelFunc:
>>
>>> class ModelFunc f where
>>> type Arg f :: *
>>> type Arity f :: *
>>>
>>> ($*) :: f -> Vector (Arg f) (Arity f) -> Arg f
>>
>> $* is similar to $ but instead of applying a function to a single
>> argument it applies it to a vector of multiple arguments.
>>
>>> instance (ModelFunc f, Arg f ~ b) => ModelFunc (b -> f) where
>>> type Arg (b -> f) = b
>>> type Arity (b -> f) = S (Arity f)
>>>
>>> f $* (x :*: xs) = f x $* xs
>>
>> You can see that we restrict the arguments of module functions to
>> have
>> the same type: 'Arg f ~ b'.
>>
>> This is the base case:
>>
>>> instance ModelFunc Double where
>>> type Arg Double = Double
>>> type Arity Double = Z
>>>
>>> d $* Nil = d
>>
>> We represent Vectors using a GADT:
>>
>>> data Vector a n where
>>> Nil :: Vector a Z
>>> (:*:) :: a -> Vector a n -> Vector a (S n)
>>
>>> infixr :*:
>>
>> Converting a Vector to a list is easy:
>>
>>> toList :: Vector b n -> [b]
>>> toList Nil = []
>>> toList (x :*: xs) = x : toList xs
>>
>> My single question is: how can I convert a list to a Vector???
>>
>>> fromList :: [b] -> Vector b n
>>> fromList = ?
>>
>> regards,
>>
>> Roel and Bas van Dijk
>>
>> [1] http://www.ics.forth.gr/~lourakis/levmar/
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
> _______________________________________________
> 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