<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>Hi,<br>
</p>
<p>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><tt>{-# LANGUAGE TypeOperators #-}</tt><tt><br>
</tt><tt>{-# LANGUAGE GADTs #-}</tt><tt><br>
</tt><tt>{-# LANGUAGE DataKinds #-}</tt><tt><br>
</tt><tt>{-# LANGUAGE ScopedTypeVariables #-}</tt><tt><br>
</tt><tt>{-# LANGUAGE KindSignatures #-}</tt><tt><br>
</tt><tt><br>
</tt><tt>import GHC.TypeNats</tt><tt><br>
</tt><tt>import Data.Proxy</tt><tt><br>
</tt><tt><br>
</tt><tt>data M (n :: Nat) a where</tt><tt><br>
</tt><tt> MNil :: M 0 a</tt><tt><br>
</tt><tt> MCons :: a -> M (n-1) a -> M n a</tt><tt><br>
</tt><tt><br>
</tt><tt>infixr 5 `MCons`</tt><tt><br>
</tt><tt><br>
</tt><tt>toList :: M k a -> [a]</tt><tt><br>
</tt><tt>toList MNil = []</tt><tt><br>
</tt><tt>toList (MCons a as) = a:toList as</tt><tt><br>
</tt><tt><br>
</tt><tt>instance (KnownNat n, Show a) => Show (M n a) where</tt><tt><br>
</tt><tt> show xs = mconcat</tt><tt><br>
</tt><tt> [ "M @"</tt><tt><br>
</tt><tt> , show (natVal (Proxy :: Proxy n))</tt><tt><br>
</tt><tt> , " "</tt><tt><br>
</tt><tt> , show (toList xs)</tt><tt><br>
</tt><tt> ]</tt><tt><br>
</tt><tt><br>
</tt><tt>--t2 :: M 2 Integer</tt><tt><br>
</tt><tt>t2 = 1 `MCons` 2 `MCons` MNil</tt><tt><br>
</tt><tt><br>
</tt><tt>--t3 :: M 3 Integer</tt><tt><br>
</tt><tt>t3 = 1 `MCons` 2 `MCons` 3 `MCons` MNil</tt><tt><br>
</tt><tt><br>
</tt><tt>zipM :: (a -> b -> c) -> M n a -> M n b ->
M n c</tt><tt><br>
</tt><tt>zipM _f MNil MNil = MNil</tt><tt><br>
</tt><tt>zipM f (MCons a as) (MCons b bs) = MCons (f a b) (zipM f
as bs) </tt><tt><br>
</tt><tt><br>
</tt><tt>fx :: Num a => M n a -> M n a -> M n a</tt><tt><br>
</tt><tt>fx = zipM (+)</tt><br>
<br>
</p>
<p>Test:</p>
<p><tt>> t2</tt><tt><br>
</tt><tt>M @2 [1,2]</tt><tt><br>
</tt><tt>> fx t2 t2</tt><tt><br>
</tt><tt>M @2 [2,4]</tt><tt><br>
</tt><tt>> fx t2 t3</tt><tt><br>
</tt><tt><br>
</tt><tt><interactive>:38:7: error:</tt><tt><br>
</tt><tt> • Couldn't match type ‘3’ with ‘2’</tt><tt><br>
</tt><tt> Expected type: M 2 Integer</tt><tt><br>
</tt><tt> Actual type: M 3 Integer</tt><br>
</p>
<p><br>
</p>
<p>Cheers,<br>
Sylvain<br>
</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 15/03/2019 13:57, mike h wrote:<br>
</div>
<blockquote type="cite"
cite="mid:542C66B8-2502-4A2D-92C2-7AC382FAAF98@yahoo.co.uk">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<br class="">
<div><font class="" size="5">Hi Frederic,</font></div>
<div><font class="" size="5"><br class="">
</font></div>
<div><font class="" size="5">Yeh, my explanation is a bit dubious
:) </font></div>
<div><font class="" size="5">What I’m trying to say is:</font></div>
<div><font class="" size="5">Looking at the type M (n::Nat) </font></div>
<div><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><font class="" size="5"><br class="">
</font></div>
<div><font class="" size="5"> f :: M 2 Int</font></div>
<div><font class="" size="5"> </font></div>
<div><font class="" size="5"><br class="">
</font></div>
<div><font class="" size="5">If I want a M 3 then I need
to explicitly write the function with signature</font></div>
<div><font class="" size="5">M 3 Int</font></div>
<div><font class="" size="5"><br class="">
</font></div>
<div><font class="" size="5">and so on for every possible instance
that I might want.</font></div>
<div><font class="" size="5"><br class="">
</font></div>
<div><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><font class="" size="5">In pseudo Haskell</font></div>
<div><font class="" size="5"><br class="">
</font></div>
<div><font class="" size="5">create :: Int -> [Int] -> M n </font></div>
<div><font class="" size="5">create size ns = (M ns) :: M size
Int</font></div>
<div><font class="" size="5"><br class="">
</font></div>
<div><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><span style="font-size: x-large;" class=""><br class="">
</span></div>
<div><font class="" size="5">It’s sort of like parameterising the
signature of the function.</font></div>
<div><font class="" size="5"><br class="">
</font></div>
<div><font class="" size="5">Thanks</font></div>
<div><font class="" size="5"><br class="">
</font></div>
<div><font class="" size="5">Mike</font></div>
<div><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>
<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>
</body>
</html>