<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><font size="5" class="">Hi Frederic,</font></div><div><font size="5" class=""><br class=""></font></div><div><font size="5" class="">Yeh, my explanation is a bit dubious :) </font></div><div><font size="5" class="">What I’m trying to say is:</font></div><div><font size="5" class="">Looking at the type M (n::Nat) </font></div><div><font size="5" class="">If I want an M 2 of Ints say, then I need to write the function with signature</font></div><div><font size="5" class=""><br class=""></font></div><div><font size="5" class=""> f :: M 2 Int</font></div><div><font size="5" class=""> </font></div><div><font size="5" class=""><br class=""></font></div><div><font size="5" class="">If I want a M 3 then I need to explicitly write the function with signature</font></div><div><font size="5" class="">M 3 Int</font></div><div><font size="5" class=""><br class=""></font></div><div><font size="5" class="">and so on for every possible instance that I might want.</font></div><div><font size="5" class=""><br class=""></font></div><div><font size="5" class="">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)</font></div><div><font size="5" class="">In pseudo Haskell</font></div><div><font size="5" class=""><br class=""></font></div><div><font size="5" class="">create :: Int -> [Int] -> M n </font></div><div><font size="5" class="">create size ns = (M ns) :: M size Int</font></div><div><font size="5" class=""><br class=""></font></div><div><font size="5" class="">where </font><span style="font-size: x-large;" class=""> its trying to coerce (M ns) into the type (</span><span style="font-size: x-large;" class="">M size Int) where size is an Int but needs to be a Nat.</span></div><div><span style="font-size: x-large;" class=""><br class=""></span></div><div><font size="5" class="">It’s sort of like parameterising the signature of the function.</font></div><div><font size="5" class=""><br class=""></font></div><div><font size="5" class="">Thanks</font></div><div><font size="5" class=""><br class=""></font></div><div><font size="5" class="">Mike</font></div><div><font size="5" class=""><br class=""></font><blockquote type="cite" class=""><div class="">On 15 Mar 2019, at 11:37, Frederic Cogny <<a href="mailto:frederic.cogny@gmail.com" class="">frederic.cogny@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">I'm not sure I understand your question Mike.<br class="">Are you saying <font face="monospace" class="">createIntM</font> behaves as desired but the data constructor M could let you build a data <font face="monospace" class="">M</font> with the wrong type. for instance <font face="monospace" class="">M [1,2] :: M 1 </font><font face="monospace" class="">Int</font> ?</div><div class=""><div class=""><br class=""></div><div class="">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 <span style="font-family:monospace" class="">createIntM) </span>but where you do not expose the type constructor. so something like<br class=""></div><div class=""><br class=""></div><div class=""><div class=""><font face="monospace" class="">module MyModule</font></div><div class=""><font face="monospace" class=""> ( M -- as opposed to M(..) to not expose the type constructor</font></div><div class=""><font face="monospace" class=""> , createIntM</font></div><div class=""><font face="monospace" class=""> ) where</font></div></div><div class=""><br class=""></div><div class="">Then, outside of MyModule, you can not create an incorrect lentgh annotated list since the only way to build it is through <span style="font-family:monospace" class="">createIntM</span></div><div class=""><span style="font-family:monospace" class=""><br class=""></span></div><div class="">Does that make sense?</div><div class=""><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Mar 14, 2019 at 4:19 PM mike h <<a href="mailto:mike_k_houghton@yahoo.co.uk" class="">mike_k_houghton@yahoo.co.uk</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space" class=""><span style="font-size:20px" class="">Hi,</span><div class=""><span style="font-size:20px" class="">Thanks for the pointers. So I’ve got</span></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class="">data M (n :: Nat) a = M [a] deriving Show<br class=""><br class="">t2 :: M 2 Int<br class="">t2 = M [1,2]<br class=""><br class="">t3 :: M 3 Int<br class="">t3 = M [1,2,3]<br class=""><br class="">fx :: Num a => M n a -> M n a -> M n a<br class="">fx (M xs) (M ys) = M (zipWith (+) xs ys)<br class=""></span></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class="">and having </span></div><div class=""><span class=""><span style="font-size:20px" class="">g = fx t2 t3</span><br class=""></span></div><div class=""><br class=""></div><div class=""><span style="font-size:20px" class="">won’t compile. Which is what I want.</span></div><div class=""><span style="font-size:20px" class="">However…</span></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class="">t2</span><span style="font-size:20px" class=""> </span><span style="font-size:20px" class="">::</span><span style="font-size:20px" class=""> </span><span style="font-size:20px" class="">M</span><span style="font-size:20px" class=""> 2 </span><span style="font-size:20px" class="">Int</span><br style="font-size:20px" class=""><span style="font-size:20px" class="">t2 </span><span style="font-size:20px" class="">=</span><span style="font-size:20px" class=""> </span><span style="font-size:20px" class="">M</span><span style="font-size:20px" class=""> [</span><span style="font-size:20px" class="">1</span><span style="font-size:20px" class="">,</span><span style="font-size:20px" class="">2</span><span style="font-size:20px" class="">]</span></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class="">is ‘hardwired’ to 2 and clearly I could make t2 return a list of any length. </span></div><div class=""><span style="font-size:20px" class="">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. </span></div><div class=""><span style="font-size:20px" class="">In other words if I supply a list, xs, of length n then I wan’t M n xs</span></div><div class=""><span style="font-size:20px" class="">Like this</span></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class=""><span class="">createIntM xs </span><span class="">=</span><span class=""> (</span><span class="">M</span><span class=""> xs) </span><span class="">::</span><span class=""> </span><span class="">M</span><span class=""> (</span><span class="">length</span><span class=""> </span><span class="">xs</span><span class="">) </span><span class="">Int</span></span></div><div class=""><span style="font-size:20px" class=""><span class=""><br class=""></span></span></div><div class=""><span style="font-size:20px" class="">which compile and has type</span></div><div class=""><div class=""><span style="font-size:20px" class="">λ-> :t createIntM </span></div><div class=""><span style="font-size:20px" class="">createIntM :: [Int] -> M (length xs) Int</span></div></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class="">and all Ms created using </span><span style="font-size:20px" class="">createIntM have the same type irrespective of the length of the supplied list.</span></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class="">What’s the type jiggery I need or is this not the right way to go?</span></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class="">Thanks</span></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class="">Mike</span></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><span style="font-size:20px" class=""><br class=""></span></div><div class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On 14 Mar 2019, at 13:12, Frederic Cogny <<a href="mailto:frederic.cogny@gmail.com" target="_blank" class="">frederic.cogny@gmail.com</a>> wrote:</div><br class="m_8211798119830778800Apple-interchange-newline"><div class="">The (experimental) Static module of hmatrix seems (I've used the packaged but not that module) to do exactly that: <a href="http://hackage.haskell.org/package/hmatrix-0.19.0.0/docs/Numeric-LinearAlgebra-Static.html" target="_blank" class="">http://hackage.haskell.org/package/hmatrix-0.19.0.0/docs/Numeric-LinearAlgebra-Static.html</a><div class=""><br class=""><br class=""><br class=""><div class="gmail_quote"><div dir="ltr" class="">On Thu, Mar 14, 2019, 12:37 PM Francesco Ariis <<a href="mailto:fa-ml@ariis.it" target="_blank" class="">fa-ml@ariis.it</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Mike,<br class="">
<br class="">
On Thu, Mar 14, 2019 at 11:10:06AM +0000, mike h wrote:<br class="">
> Multiplication of two matrices is only defined when the the number of columns in the first matrix <br class="">
> equals the number of rows in the second matrix. i.e. c1 == r2<br class="">
> <br class="">
> So when writing the multiplication function I can check that c1 == r2 and do something.<br class="">
> However what I really want to do, if possible, is to have the compiler catch the error. <br class="">
<br class="">
Type-level literals [1] or any kind of similar trickery should help you<br class="">
with having matrices checked at compile-time.<br class="">
<br class="">
[1] <a href="https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/type-level-literals.html" rel="noreferrer" target="_blank" class="">https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/type-level-literals.html</a><br class="">
_______________________________________________<br class="">
Beginners mailing list<br class="">
<a href="mailto:Beginners@haskell.org" target="_blank" class="">Beginners@haskell.org</a><br class="">
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a><br class="">
</blockquote></div></div>-- <br class=""><div dir="ltr" class="m_8211798119830778800gmail_signature" data-smartmail="gmail_signature"><div dir="ltr" class=""><div class=""><font class="">Frederic Cogny<br class=""></font></div><font class=""><font class="">+33 </font><span class="">7 83 12 61 69</span></font><br class=""></div></div>
_______________________________________________<br class="">Beginners mailing list<br class=""><a href="mailto:Beginners@haskell.org" target="_blank" class="">Beginners@haskell.org</a><br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" target="_blank" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a><br class=""></div></blockquote></div><br class=""></div></div></blockquote></div></div></div></div>-- <br class=""><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr" class=""><div class=""><font class="">Frederic Cogny<br class=""></font></div><font class=""><font class="">+33 </font><span class="">7 83 12 61 69</span></font><br class=""></div></div>
</div></blockquote></div><br class=""></body></html>