<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="">Thanks.<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On 15 Mar 2019, at 13:48, Sylvain Henry <<a href="mailto:sylvain@haskus.fr" class="">sylvain@haskus.fr</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
  
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class="">
  
  <div text="#000000" bgcolor="#FFFFFF" class=""><p class="">Hi,<br class="">
    </p><p class="">The problem is that Haskell lists don't carry their length in
      their type hence you cannot enforce their length at compile time.
      But you can define your M this way instead:</p><p class=""><tt class="">{-# LANGUAGE TypeOperators #-}</tt><tt class=""><br class="">
      </tt><tt class="">{-# LANGUAGE GADTs #-}</tt><tt class=""><br class="">
      </tt><tt class="">{-# LANGUAGE DataKinds #-}</tt><tt class=""><br class="">
      </tt><tt class="">{-# LANGUAGE ScopedTypeVariables #-}</tt><tt class=""><br class="">
      </tt><tt class="">{-# LANGUAGE KindSignatures #-}</tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class="">import GHC.TypeNats</tt><tt class=""><br class="">
      </tt><tt class="">import Data.Proxy</tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class="">data M (n :: Nat) a where</tt><tt class=""><br class="">
      </tt><tt class="">   MNil  :: M 0 a</tt><tt class=""><br class="">
      </tt><tt class="">   MCons :: a -> M (n-1) a -> M n a</tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class="">infixr 5 `MCons`</tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class="">toList :: M k a -> [a]</tt><tt class=""><br class="">
      </tt><tt class="">toList MNil         = []</tt><tt class=""><br class="">
      </tt><tt class="">toList (MCons a as) = a:toList as</tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class="">instance (KnownNat n, Show a) => Show (M n a) where</tt><tt class=""><br class="">
      </tt><tt class="">   show xs = mconcat</tt><tt class=""><br class="">
      </tt><tt class="">      [ "M @"</tt><tt class=""><br class="">
      </tt><tt class="">      , show (natVal (Proxy :: Proxy n))</tt><tt class=""><br class="">
      </tt><tt class="">      , " "</tt><tt class=""><br class="">
      </tt><tt class="">      , show (toList xs)</tt><tt class=""><br class="">
      </tt><tt class="">      ]</tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class="">--t2 :: M 2 Integer</tt><tt class=""><br class="">
      </tt><tt class="">t2 = 1 `MCons` 2 `MCons` MNil</tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class="">--t3 :: M 3 Integer</tt><tt class=""><br class="">
      </tt><tt class="">t3 = 1 `MCons` 2 `MCons` 3 `MCons` MNil</tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class="">zipM :: (a -> b -> c) -> M n a -> M n b ->
        M n c</tt><tt class=""><br class="">
      </tt><tt class="">zipM _f MNil         MNil         = MNil</tt><tt class=""><br class="">
      </tt><tt class="">zipM  f (MCons a as) (MCons b bs) = MCons (f a b) (zipM f
        as bs) </tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class="">fx :: Num a => M n a -> M n a -> M n a</tt><tt class=""><br class="">
      </tt><tt class="">fx = zipM (+)</tt><br class="">
      <br class="">
    </p><p class="">Test:</p><p class=""><tt class="">> t2</tt><tt class=""><br class="">
      </tt><tt class="">M @2 [1,2]</tt><tt class=""><br class="">
      </tt><tt class="">> fx t2 t2</tt><tt class=""><br class="">
      </tt><tt class="">M @2 [2,4]</tt><tt class=""><br class="">
      </tt><tt class="">> fx t2 t3</tt><tt class=""><br class="">
      </tt><tt class=""><br class="">
      </tt><tt class=""><interactive>:38:7: error:</tt><tt class=""><br class="">
      </tt><tt class="">    • Couldn't match type ‘3’ with ‘2’</tt><tt class=""><br class="">
      </tt><tt class="">      Expected type: M 2 Integer</tt><tt class=""><br class="">
      </tt><tt class="">        Actual type: M 3 Integer</tt><br class="">
    </p><p class=""><br class="">
    </p><p class="">Cheers,<br class="">
      Sylvain<br class="">
    </p><p class=""><br class="">
    </p>
    <div class="moz-cite-prefix">On 15/03/2019 13:57, mike h wrote:<br class="">
    </div>
    <blockquote type="cite" cite="mid:542C66B8-2502-4A2D-92C2-7AC382FAAF98@yahoo.co.uk" class="">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class="">
      <br class="">
      <div class=""><font class="" size="5">Hi Frederic,</font></div>
      <div class=""><font class="" size="5"><br class="">
        </font></div>
      <div class=""><font class="" size="5">Yeh, my explanation is a bit dubious
          :) </font></div>
      <div class=""><font class="" size="5">What I’m trying to say is:</font></div>
      <div class=""><font class="" size="5">Looking at the type M (n::Nat) </font></div>
      <div class=""><font class="" size="5">If I want an M 2  of Ints say,  then
          I need to write the function with signature</font></div>
      <div class=""><font class="" size="5"><br class="">
        </font></div>
      <div class=""><font class="" size="5"> f :: M 2 Int</font></div>
      <div class=""><font class="" size="5"> </font></div>
      <div class=""><font class="" size="5"><br class="">
        </font></div>
      <div class=""><font class="" size="5">If I want a M 3 then I need
          to explicitly write the function with signature</font></div>
      <div class=""><font class="" size="5">M 3 Int</font></div>
      <div class=""><font class="" size="5"><br class="">
        </font></div>
      <div class=""><font class="" size="5">and so on for every possible instance
          that I might want.</font></div>
      <div class=""><font class="" size="5"><br class="">
        </font></div>
      <div class=""><font class="" size="5">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 class=""><font class="" size="5">In pseudo Haskell</font></div>
      <div class=""><font class="" size="5"><br class="">
        </font></div>
      <div class=""><font class="" size="5">create :: Int -> [Int] -> M n </font></div>
      <div class=""><font class="" size="5">create size ns = (M ns) ::  M size
          Int</font></div>
      <div class=""><font class="" size="5"><br class="">
        </font></div>
      <div class=""><font class="" size="5">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 class=""><span style="font-size: x-large;" class=""><br class="">
        </span></div>
      <div class=""><font class="" size="5">It’s sort of like parameterising the
          signature of the function.</font></div>
      <div class=""><font class="" size="5"><br class="">
        </font></div>
      <div class=""><font class="" size="5">Thanks</font></div>
      <div class=""><font class="" size="5"><br class="">
        </font></div>
      <div class=""><font class="" size="5">Mike</font></div>
      <div class=""><font class="" size="5"><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="" moz-do-not-send="true">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 class="" face="monospace">createIntM</font> behaves
                as desired but the data constructor M could let you
                build a data <font class="" face="monospace">M</font>
                with the wrong type. for instance <font class="" face="monospace">M [1,2] :: M 1 </font><font class="" face="monospace">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 class="" face="monospace">module
                      MyModule</font></div>
                  <div class=""><font class="" face="monospace">  ( M --
                      as opposed to M(..) to not expose the type
                      constructor</font></div>
                  <div class=""><font class="" face="monospace"> 
                      , createIntM</font></div>
                  <div class=""><font class="" face="monospace">  )
                      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="" moz-do-not-send="true">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="" moz-do-not-send="true">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="" moz-do-not-send="true">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="" moz-do-not-send="true">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="" moz-do-not-send="true">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="" moz-do-not-send="true">Beginners@haskell.org</a><br class="">
                                      <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank" class="" moz-do-not-send="true">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="" moz-do-not-send="true">Beginners@haskell.org</a><br class="">
                                <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" target="_blank" class="" moz-do-not-send="true">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="">
      <br class="">
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Beginners mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Beginners@haskell.org">Beginners@haskell.org</a>
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a>
</pre>
    </blockquote>
  </div>

_______________________________________________<br class="">Beginners mailing list<br class=""><a href="mailto:Beginners@haskell.org" class="">Beginners@haskell.org</a><br class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners<br class=""></div></blockquote></div><br class=""></body></html>