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)
----------------------------------------------------------------------
Message: 1
Date: Fri, 15 Mar 2019 20:44:46 +0000
From: mike h <mike_k_hough...@yahoo.co.uk>
To: 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: <0e90c918-dc68-4d92-af80-44f09cfe1...@yahoo.co.uk>
Content-Type: text/plain; charset="utf-8"
Thanks.
> On 15 Mar 2019, at 13:48, Sylvain Henry <sylv...@haskus.fr> wrote:
>
> 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 (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
>>
>>
>>
>> _______________________________________________
>> 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>
> _______________________________________________
> 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/89b05341/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 6
*****************************************
