[Haskell-beginners] Matrix and types

[mike h]

Hi,
Thanks for the pointers. So I’ve got

data M (n :: Nat) a = M [a] deriving Show

t2 :: M 2 Int
t2  = M [1,2]

t3 :: M 3 Int
t3 = M [1,2,3]

fx :: Num a => M n a -> M n a -> M n a
fx (M xs) (M ys) = M (zipWith (+) xs ys)

and having 
g = fx t2 t3

won’t compile. Which is what I want.
However…

t2 :: M 2 Int
t2  = M [1,2]

is ‘hardwired’ to 2 and clearly I could make t2 return  a list of any length. 
So what I then tried to look at was a general function that would take a list of Int and create the M type using the length of the supplied list. 
In other words if I supply a list, xs, of length n then I wan’t  M n xs
Like this

createIntM xs = (M xs) :: M (length xs) Int

which compile and has type
λ-> :t createIntM 
createIntM :: [Int] -> M (length xs) Int

and all Ms created using createIntM  have the same type irrespective of the length of the supplied list.

What’s the type jiggery I need or is this not the right way to go?

Thanks

Mike




> On 14 Mar 2019, at 13:12, Frederic Cogny <frederic.cogny at gmail.com> wrote:
> 
> The (experimental) Static module of hmatrix seems (I've used the packaged but not that module) to do exactly that: http://hackage.haskell.org/package/hmatrix-0.19.0.0/docs/Numeric-LinearAlgebra-Static.html <http://hackage.haskell.org/package/hmatrix-0.19.0.0/docs/Numeric-LinearAlgebra-Static.html>
> 
> 
> 
> On Thu, Mar 14, 2019, 12:37 PM Francesco Ariis <fa-ml at ariis.it <mailto:fa-ml at ariis.it>> wrote:
> Hello Mike,
> 
> On Thu, Mar 14, 2019 at 11:10:06AM +0000, mike h wrote:
> > Multiplication of two matrices is only defined when the the number of columns in the first matrix 
> > equals the number of rows in the second matrix. i.e. c1 == r2
> > 
> > So when writing the multiplication function I can check that  c1 == r2 and do something.
> > However what I really want to do, if possible, is to have the compiler catch the error. 
> 
> Type-level literals [1] or any kind of similar trickery should help you
> with having matrices checked at compile-time.
> 
> [1] https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/type-level-literals.html <https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/type-level-literals.html>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org <mailto:Beginners at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners <http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners>
> -- 
> Frederic Cogny
> +33 7 83 12 61 69
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20190314/2163ff21/attachment.html>