Re: [Haskell-beginners] Matrix and types

I'm not sure I understand your question Mike. Are you saying createIntM behaves as desired but the data constructor M could let you build a data M with the wrong type. for instance M [1,2] :: M 1 Int ? If that is your question, then one way to handle this is to have a separate module where you define the data type and the proper constructor (here M and createIntM) but where you do not expose the type constructor. so something like module MyModule ( M -- as opposed to M(..) to not expose the type constructor , createIntM ) where Then, outside of MyModule, you can not create an incorrect lentgh annotated list since the only way to build it is through createIntM Does that make sense? On Thu, Mar 14, 2019 at 4:19 PM mike h wrote:

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

On Thu, Mar 14, 2019, 12:37 PM Francesco Ariis 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-l... _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

-- Frederic Cogny +33 7 83 12 61 69 _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

-- Frederic Cogny +33 7 83 12 61 69