Send Beginners mailing list submissions to beginners@haskell.org To subscribe or unsubscribe via the World Wide Web, visit http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners or, via email, send a message with subject or body 'help' to beginners-requ...@haskell.org
You can reach the person managing the list at beginners-ow...@haskell.org When replying, please edit your Subject line so it is more specific than "Re: Contents of Beginners digest..." Today's Topics: 1. Re: Matrix and types (mike h) 2. Re: Matrix and types (Sylvain Henry) ---------------------------------------------------------------------- Message: 1 Date: Fri, 15 Mar 2019 12:57:13 +0000 From: mike h <mike_k_hough...@yahoo.co.uk> To: f...@melix.net Cc: The Haskell-Beginners Mailing List - Discussion of primarily beginner-level topics related to Haskell <beginners@haskell.org> Subject: Re: [Haskell-beginners] Matrix and types Message-ID: <542c66b8-2502-4a2d-92c2-7ac382faa...@yahoo.co.uk> Content-Type: text/plain; charset="utf-8" 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.co...@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_hough...@yahoo.co.uk > <mailto:mike_k_hough...@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.co...@gmail.com >> <mailto:frederic.co...@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...@ariis.it >> <mailto:fa...@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@haskell.org <mailto:Beginners@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@haskell.org <mailto:Beginners@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-0001.html> ------------------------------ Message: 2 Date: Fri, 15 Mar 2019 14:48:06 +0100 From: Sylvain Henry <sylv...@haskus.fr> To: beginners@haskell.org Subject: Re: [Haskell-beginners] Matrix and types Message-ID: <cf5dda23-bd3a-a05c-b353-ce3ee79ad...@haskus.fr> Content-Type: text/plain; charset="utf-8"; Format="flowed" Hi, 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: {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE KindSignatures #-} import GHC.TypeNats import Data.Proxy data M (n :: Nat) a where MNil :: M 0 a MCons :: a -> M (n-1) a -> M n a infixr 5 `MCons` toList :: M k a -> [a] toList MNil = [] toList (MCons a as) = a:toList as instance (KnownNat n, Show a) => Show (M n a) where show xs = mconcat [ "M @" , show (natVal (Proxy :: Proxy n)) , " " , show (toList xs) ] --t2 :: M 2 Integer t2 = 1 `MCons` 2 `MCons` MNil --t3 :: M 3 Integer t3 = 1 `MCons` 2 `MCons` 3 `MCons` MNil zipM :: (a -> b -> c) -> M n a -> M n b -> M n c zipM _f MNil MNil = MNil zipM f (MCons a as) (MCons b bs) = MCons (f a b) (zipM f as bs) fx :: Num a => M n a -> M n a -> M n a fx = zipM (+) Test: > t2 M @2 [1,2] > fx t2 t2 M @2 [2,4] > fx t2 t3 <interactive>:38:7: error: • Couldn't match type ‘3’ with ‘2’ Expected type: M 2 Integer Actual type: M 3 Integer Cheers, Sylvain On 15/03/2019 13:57, mike h wrote: > > 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.co...@gmail.com >> <mailto:frederic.co...@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_hough...@yahoo.co.uk >> <mailto:mike_k_hough...@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 (lengthxs) 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.co...@gmail.com <mailto:frederic.co...@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 >>> >>> >>> >>> >>> On Thu, Mar 14, 2019, 12:37 PM Francesco Ariis <fa...@ariis.it >>> <mailto:fa...@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 >>> _______________________________________________ >>> Beginners mailing list >>> Beginners@haskell.org <mailto:Beginners@haskell.org> >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners >>> >>> -- >>> Frederic Cogny >>> +33 7 83 12 61 69 >>> _______________________________________________ >>> Beginners mailing list >>> Beginners@haskell.org <mailto:Beginners@haskell.org> >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners >> >> -- >> Frederic Cogny >> +33 7 83 12 61 69 > > > _______________________________________________ > Beginners mailing list > Beginners@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://mail.haskell.org/pipermail/beginners/attachments/20190315/f6c93d5a/attachment.html> ------------------------------ Subject: Digest Footer _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners ------------------------------ End of Beginners Digest, Vol 129, Issue 5 *****************************************