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