[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