[Haskell-beginners] Matrix and types

[mike h]

Hi Frederic,

Yeh, my explanation is a bit dubious :) 
What I’m trying to say is:
Looking at the type M (n::Nat) 
If I want an M 2  of Ints say,  then I need to write the function with signature

 f :: M 2 Int
 

If I want a M 3 then I need to explicitly write the function with signature
M 3 Int

and so on for every possible instance that I might want.

What I would like to do is have just one function that is somehow parameterised to create the M tagged with the required value of (n::Nat)
In pseudo Haskell

create :: Int -> [Int] -> M n 
create size ns = (M ns) ::  M size Int

where  its trying to coerce (M ns) into the type (M size Int) where size is an Int but needs to be a Nat.

It’s sort of like parameterising the signature of the function.

Thanks

Mike

> On 15 Mar 2019, at 11:37, Frederic Cogny <frederic.cogny at gmail.com> wrote:
> 
> 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 <mike_k_houghton at yahoo.co.uk <mailto:mike_k_houghton at yahoo.co.uk>> 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 <frederic.cogny at gmail.com <mailto: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 <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

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