Send Beginners mailing list submissions to
[email protected]
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
[email protected]
You can reach the person managing the list at
[email protected]
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 <[email protected]>
To: [email protected]
Cc: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Subject: Re: [Haskell-beginners] Matrix and types
Message-ID: <[email protected]>
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 <[email protected]> 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 <[email protected]
> <mailto:[email protected]>> 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 <[email protected]
>> <mailto:[email protected]>> 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 <[email protected]
>> <mailto:[email protected]>> 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
>> [email protected] <mailto:[email protected]>
>> 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
>> [email protected] <mailto:[email protected]>
>> 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 <[email protected]>
To: [email protected]
Subject: Re: [Haskell-beginners] Matrix and types
Message-ID: <[email protected]>
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 <[email protected]
>> <mailto:[email protected]>> 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 <[email protected]
>> <mailto:[email protected]>> 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
>>> <[email protected] <mailto:[email protected]>> 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 <[email protected]
>>> <mailto:[email protected]>> 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
>>> [email protected] <mailto:[email protected]>
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>>>
>>> --
>>> Frederic Cogny
>>> +33 7 83 12 61 69
>>> _______________________________________________
>>> Beginners mailing list
>>> [email protected] <mailto:[email protected]>
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>>
>> --
>> Frederic Cogny
>> +33 7 83 12 61 69
>
>
> _______________________________________________
> Beginners mailing list
> [email protected]
> 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
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 129, Issue 5
*****************************************
